Home

T OY - GPD - Universidad Complutense de Madrid

1. 3 3 2 Send More Money smm toy es cierra e oes 3 3 3 N Queens queens toy e soe o Re a a oe ee eS 3 3 4 A Cryptoarithmetic Problem alpha toy lt aoa 3 3 5 Magic Series magicser toy 05 ee ee eee Cooperation of Solvers 4 1 Introduction 20 2 4 84 58 a4 Shave o Skee ba ede dead bh ae a All Biheleney y ac ea ete e ae ee he Ge ale a a es ee 4 1 2 Libraries necessaries for Cooperation oo soa o e 0200 4 2 The Constraint Cooperation Bridge o o eee ee 43 Bindiig os e zeia e A EO a oe e ee ee a AA Propagation s s acs a ce 4 ede a Ne ee ba a ee ee ck ee eas 4 4 1 Propagation from FD toR aaau a a 4 4 2 Propagation from R to FD 2 0 0 0 a ee 4 5 Introductory Programs 4 5 1 Intersection of a discrete grid and a continuous region bothIn toy 4 5 2 Distribution of raw material between suppliers and consumers distrib tion toy lt ss Baw be Kee E ea Gee A 5 Input Output 5 1 Standard Input Output Functions 5 2 Sequencing Input Output Functions 5 3 Do Notation DA Files e ra Gea a a PG Se Oe ae Ee ee 5 4 1 The io file System Module Graphic Input Output 5 5 1 Mutable Variables 5 6 List Comprehensions 5 5 Graphic Input Output 2 2 en Debugging Tools 6 1 Introduction 6 2 Declarative Debugging 6 3 An Example 6 3 1 Starting DDT 6 3 2 Looking for buggy nodes 6 3 3 Strategies Limitations 6 4 6 5 Programming Examples A 1 Logic Programming A 1
2. A gt A gt bool lt O lt real gt real gt bool In fact JOY supports an implicit conversion of values of type int to type real Therefore in absence of user given type declarations the type inference algorithm always assumes the type real for the arguments and results of numeric functions As an exception to this general rule some of the built in arithmetic operations require some arguments of type int see Section 2 8 for details In case that some function definition is ill typed the TOY system raises type error messages and compilation is aborted Otherwise JOY compares the types inferred for defined functions with those declared in the program For each defined function f there are three possible cases e There is no declared type for f or the declared type is equivalent to the inferred type up to a renaming of type variables Then the inferred type is used e There is a declared type which is strictly less general than the inferred type Then a warning to the user is emitted but the declared type is assumed This may prevent a suc cesful type inference for some other defined function For example the following program fragment would cause a type error because the declared type of length requires lists of integers which is not general enough to render the definition of sameLength well typed On the contrary the inferred type of length is general enough to well type sameLength length
3. domain int int int bool subset inset setcomplement int int bool intersect int int int belongs int int bool ENUMERATION FUNCTIONS labeling labelType int bool indomain int bool RELATIONAL CONSTRAINT OPERATORS lt lt gt gt int int bool ARITHMETIC CONSTRAINT OPERATORS amp int gt int gt int ARITHMETIC CONSTRAINTS sum int int gt int bool int bool scalar product int int gt int int bool int bool COMBINATORIAL CONSTRAINTS all_different int bool all different int gt allDiffOptions bool circuit int bool assignment circuit serialized int int bool serialized int int serialOptions bool count int int int int gt bool gt int gt bool element exactly int int int cumulative int gt int gt int int gt bool cumulative int int int int serial0ptions bool PROPOSITIONAL CONSTRAINTS lt gt gt bool bool bool 69 Table 3 3 The Predefined Set of Impure FD Functions REFLECTION FUNCTIONS fdmin fd max fd size fd degree int int d set int fdset fd dom int fdrange fd_neighbors int int fd closure int int
4. do expressions doExpr doj j doDecl ldoDecl doDecl varld lt expr expr Lists list expr E expr expr m7 expr expr Tuples tuple expr m7 expr Intensional Lists intensionalExpr expr qual qual qual varld lt expr pattern expr expr CONSTANTS constant Integer Float Char String Bool 225 BASIC NON TERMINALS Infix operators and constructors op gt funOp consOp funOp opFunld funId consOp opConsId consId Functions and constructors constructor consld l opConsld function gt funld opFunld Identifiers funld identifier consId gt identifier opConsId consOperator opFunld operator typeld gt identifier varld variable 226 Appendix E Type Inference As we have seen in Section 2 2 TOY uses a type inference system based on the Damas Milner polymorphic type system 7 In this appendix we explain the type inference algorithm imple mented in TOY This algorithm performs two main steps first it makes a dependency analysis
5. In fact they can be used in any part of a program but a correct behaviour only is ensured when there is no non deterministic search 125 5 1 Standard Input Output Functions Standard output functions write to the standard output device which is usually the user s terminal The standard output functions provided by TOY are the following e putChar char gt io unit which prints a character e done io unit which does nothing e putStr string gt io unit which prints a string e putStrLn string gt io unit which is similar to putStr except that it prints a newline character after printing the string Standard input functions read input from the standard input device which is usually the user s keyboard The standard input functions provided by TOY are the following e getChar io char which returns the first character read from the standard input e return A gt ioA which is a generalization of done and does not change the world returning a value of type io A e getLine io string which reads a line of text from the standard input 5 2 Sequencing Input Output Functions As in Haskell 16 or Curry 14 the way of combining sequences of input output operations is done by means of the following two binding functions gt gt io A gt io B gt io B gt gt io A gt A gt io B gt io B Supposing that p and q are input output operations then p gt gt q is
6. bool gt bool andL foldr true orL foldr or false orL foldr false orL is stricter but more deterministic than orL any any all A gt bool gt A gt bool any P orL map P any P orL map P any is stricter but more deterministic than any all P andL map P undefined A undefined if false then undefined def X is true if X is finite and totally defined def X _ not_undef X is true if X is not undefined not_undef X X _ nf X is the identity restricted to finite and totally defined values Operationally nf X forces the computation of a normal form for X if it exists 197 hnf X is the identity restricted to not undefined values Operationally hnf X forces the computation of a head normal form for X if it exists hnf X X lt X _ strict F is the restriction of F to finite totally defined arguments It forces the evaluation to nf of the argument before applying F strict F X F Y lt X Y strict F is the restriction of F to not undefined arguments It forces the evaluation to hnf of the argument before applying F strict F X F X lt X _ mapping a function through a list map A gt B gt A gt B map F map F X Xs F X map F Xs hh Function composition B gt C gt A gt B gt A gt C F G X F GX L
7. e Type Declaration range_to_fdset range gt fdset fdset_to_range fdset range e Modes range to fdset fdset_to range in inout e Definition fdset_to range S returns the range equivalent to the input FD set range to _fdset is the inverse function of fdset_to_range e Reifiable Not applied 97 e Example Toy FD gt fdset_to_range interval 0 1 interval 2 3 R range_to_fdset R R gt uni cte 0 1 cte 2 3 S gt interval 0 3 gt Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms fdset_add_element 2 fdset_del_element 2 e Type Declaration fdset_add_element fdset_del_element fdset int fdset e Modes fdset_add element fdset del element in in gt inout e Definition fdset_add element S E and fdset del element S E return the FD set which is the result of adding resp deleting the element E to resp from S e Reifiable Not applied e Example Toy FD gt domain X O 1 S fd_set X SA fdset_add_element S 2 SD fdset_del_element SA O S gt interval 0 1 SA gt interval 0 2 SD gt interval 1 2 X in 0 1 Elapsed time 10 ms sol 1 more solutions y n d a y no Elapsed time O ms fdset_intersection 2 fdset_subtract 2 fdset_union 2 fdset_complement 1 e Type Declaration fdset_intersection fdset_subtract fdset_union fdset
8. RX 1 lt i lt n is created with RX new e Propagation Constraint Afterwards the constraints a lt RX RX lt b 1 lt i lt n are built as mate constraints and submitted to the real solver e Example In next goal a new bridge is created for variable Y 111 Constraint Bridges Created Constraints Created domain X1 Xn ab Xi RX 1 lt i lt n X has no a lt RX RX lt b 1 lt i lt n bridge RX new belongs X a1 an X RX X has no bridge RX min a1 an lt RX new RX lt mazx aj an ti lt te analogously either t is an integer constant or else t lt te For 1 lt i lt 2 Either t is an lt gt gt is a variable Xy integer constant n and tR is n or else t X RX 1SiS2 if ti is a vari is a variable X and tk is RX able X with no bridge RX new ti tg gt lt3 analo X RX 1 lt i lt 3 t is a variable t te gt ie For 1 lt i lt 3 i is gously X with no bridge RX new determined as in the previous case Table 4 1 Propagations from FD to R Toy R FD gt X RX domain 3 X Y 2 5 Y Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms The same goal without propagation is Toy R FD gt X RX domain 3 X Y 2 5 X RX X in 2 5 Y in 2 5 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms
9. Rules Deal Ary Aj Y Chale Xk Ys ifcEe DOC k lt n Q fx X1 Xp Y AO CA Xk Y if fe FS k l lt n fn 1 X1 An 1 Y AO ome A if pere Remarks 1 The real implementation does not need to use different symbols for c p C1 Cn or fo f1 fn resp Instead c f resp is used to represent all of them This can be done since Prolog allows the use of the same constructor with different arities 2 Goals must also be translated to first order syntax in the same way as conditions of program rules are translated that is fol 98 fole1 o fole2 ifo lt lt gt gt 241 3 The first order translation fo determines indeed a way of representing as Prolog terms TOY programs program rules more precisely expressions and goals G 2 Introduction of Suspensions We assume a TOY program P translated to first order syntax consisting of the rules R1 Rn The idea of suspensions is to replace each subexpression in P with the shape of a function call f e1 n by a Prolog term of the form susp f e1 en R S called a suspension where R and S are initially i e at the time of translation new Prolog variables If during execution the computation of a head normal form for f e1 n is required the variable R will be used to get the obtained value and we say that the suspension has been evaluated The argument S in a suspension is a flag to indicate if
10. int gt int length 0 length X Xs 1 length Xs sameLength A gt B gt bool sameLength xs ys length Xs length Ys 29 e There is a declared type which is not unifiable with the inferred type In this case the declared type is wrong The system emits an error message and compilation is aborted For example the following function definition would be rejected as ill typed because the declared type of length is incompatible with the inferred type length A gt bool length 0 length X Xs 1 length Xs 2 7 Operators and Sections As in Haskell and many other programming languages those function symbols used in infiz notation are called operators in TOY For instance the simple expression X 3 uses the primitive multiplication operator In addition to the predefined operators see Section 2 8 TOY users can introduce new operators by means of operator declarations These start with one of the three keywords infixr infixl or infix intended for right associative left associative and non associative respectively followed by the operator s precedence and name For instance in order to declare right associative operators for boolean conjunction and disjunction one could write infixr 40 infixr 30 These declarations inform the parser that must be given higher priority than More generally precedences are positive numbers with bigger values standing for higher priorities
11. X in 0 8 Y in 1 9 Z in 2 10 gt Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms fd_statistics 0O e Type Declaration fd_statistics bool e Modes fd statistics inout e Definition fd_statistics always returns true and displays a summary of the statistics computed by fd_statistics 1 All counters are zeroed e Reifiable Not applied e Example Toy FD gt L X Y Z domain L 1 4 all_different L complete true labeling L fd_statistics Resumptions 9 Entailments 1 Prunings 9 Backtracks 0 102 Constraints created 3 L 1 2 31 X gt 1 Y gt 2 Z gt 3 Elapsed time 10 ms sol 1 more solutions y n d a y n 3 3 Introductory Programs The distribution provides the directory examples cflpfd that contains a number of examples of TOY programs that make use of FD constraints Each one of the programs listed in this section as well as those listed in Section A 7 page 30 are included in that directory The program title is annotated with the corresponding file name with extension toy 3 3 1 The Length of a List haslength toy Recall the definition of the length of a list in Section 2 6 length int gt int length 0 length X Xs 1 length Xs If we pose a goal as the following Toy FD gt length L L SL hy B Elapsed time O ms sol 1 more solutions y n d a y and then we request
12. gt t where tn t are patterns and 7 is the position of the fact in the list A basic fact f tn t must be recognized as valid iff t represents a finite approximation of the result expected for the function call f t according to the intended model of the program see Appendix F For instance if the intended meaning of sort is a list sorting function then the fact sort 2 0 1 0 3 0 gt 3 0 1 0 is not valid since 3 0 1 0 is not a valid approximation of the expected result of sort 2 0 1 0 3 0 The patterns t t can be partial i e they can include the special symbol _ representing an unknown value This is used in place of suspended function calls whose evaluation has not been demanded by the main computation In fact _ corresponds to the undefined value used to formalize declarative semantics in Appendix F Thanks to this symbol questions to the oracle are semantically correct but much simpler than they would be if suspended subexpressions were displayed Let us consider some simple examples based on the list processing functions from Section 2 6 The fact head 1 _ gt 1 is valid because the first element of a list beginning by 1 is indeed 1 The two from 0 gt O _ and from O gt 0 1 _ are also valid because O _ and 0 1 _ are finite approximations of the expected result of from 0 namely the infinite list of all non negative integers On the other hand the fact from 0 gt 0 2 4 _
13. no Elapsed time O ms e Equality and inequality constraints missed during processing of scheduling constraints Fixed e Duplicate solutions with scheduling constraints Fixed e Non ground non FD variables were output as inf sup Fixed 254 H 4 Version 2 2 1 Launched on November 2005 Enhancements e The set of examples has been extended with a new folder examples debug containing examples of buggy programs that can be used for testing the declarative debugger e The computation tree generated by the declarative debugger is now stored in the direc tory javaTree This avoids the creation of auxiliary files in the directory containing the program to be debugged Fixed Bugs e A program as data d c int int f c 3 4 yielded an error during compilation error code 24 Fixed H 5 Version 2 2 0 Launched on August 2005 Enhancements e The system variable TOYDIR is no longer necessary e The answers for a goal are now displayed as two sets the first one representing a substitu tion and the second one a conjunction of constraints For instance a goal as X 5 X Y displays the answer X gt 5 Y 5 meaning that if X is substituted by 5 and Y is any value different from 5 the goal holds However not all finite domain constraints are shown up to now e Totality constraints allowed They can be activated by typing tot and disabled with notot e The declarative debugger handles programs including equality
14. no Elapsed time O ms In the previous example the constraint X lt 2 3 is submitted to the finite domain solver and therefore the value of X is between inf and 2 X in inf 2 a lt RX analogously w r t Table 4 2 a lt RX a gt RX a gt RX e Checking Bridges X RX e Propagation Constraint Afterwards the constraints a lt X is buildt as mate con straints and submitted to the finite domain solver e Example Toy R FD gt X RX 2 3 lt RX X RX RX gt 2 3 X in 3 sup Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms 117 In the previous example the constraint 2 3 lt X is submitted to the finite domain solver and therefore the value of X is between 3 and sup X in 3 sup t tg gt lt3 analogously t t2 gt t3 was explained in section 4 4 t and to can be either constants or else variables but one of this must be a variable so that the propagation is possible e Checking Bridges If t and or tz are variables RX and RY they must have bridges in order to propagate therefore X RX and or RX RY are checked e Creation of Bridges If checking is successful then t3 is a new variable RZ and a bridge Z RZ is building for RZ with Z new e Propagation Constraint Afterwards the constraint X Y gt Z is buildt as mate constraint e Example Toy R FD gt X Xr Y Yr Xr Yr lt 7 X Xr
15. remove A gt A gt A remove Y X Xs if Y X then Xs else X remove Y Xs The execution of the expression gt show_perms abc will show on the screen abc acb bac bca cab cba 141 Chapter 6 Debugging Tools 6 1 Introduction In this chapter we describe the debugging tool DDT which is part of the TOY system As explained in Section 1 1 pg 8 the debugger needs the Java Runtime Environment which is usually part of most operating system distributions and can otherwise be downloaded from http java com Section 6 2 introduces briefly declarative debugging the theoretical basis of our debugger Section 6 3 presents a simple example The limitations of the debugger are discussed in section 6 4 Finally section 6 5 gives some hints about the internals of the tool Some examples of buggy programs are included in the examples debug directory of the distribution 6 2 Declarative Debugging The impact of declarative languages on practical applications is inhibited by many known factors including lack of debugging tools whose construction is recognized as difficult for lazy functional languages As argued in 39 such debuggers are needed and much of interest can be still learned from their construction and use Debugging tools for lazy functional logic languages are even harder to construct A promising approach is declarative debugging which starts from a computation considered incorrect by the user err
16. reverse elements of list member notMember member notMember foldl flip 0 A gt A gt bool any test for membership in list all hh test for non membership 203 concat A gt A concatenate list of lists concat foldr transpose 23 A gt A 4h transpose list of lists transpose foldr auxForTranspose Awhere auxForTranspose Xs Xss zipWith Xs Xss repeat 4A NN is used to remove the first occurrence of each element in the second 7 list from the first list It is a kind of inverse of in the sense that xs ys xs ys for any finite list xs of proper values xs infix 50 A gt A gt A AV foldl del where Ml del Y X Xs del Y if X Y then Xs else X Xs del Y B 2 misc toy FILE miscfd toy A collection of useful FD functions hasLength 2 computes the length of a list irrespective of its mode of usage Whereas a goal as length L 4 length does not terminate when prompting for all solutions hasLength L 4 does hasLength A gt int gt bool hasLength 0 true hasLength X Xs N N gt O hasLength Xs N 1 belongsOrd 2 is a version of belongs 2 that allows its second argument to be an infinite list belongsOrd int gt int gt bool belongsOrd X L belongs X intersectOrdIntLists fdset_to_list fd_set X L intersectOrdIntLi
17. Combinators for currying and uncurrying curry A B gt C gt A gt B gt C curry F X Y F X Y uncurry A gt B gt C gt A B gt C uncurry F X Y F X Y Function iteration iterate A gt A gt A gt A iterate F X Xliterate F F X Functions map and filter map A gt B gt A gt B F X map F Xs map F map F X Xs filter A gt bool gt A gt A filter P J E filter P X Xs if P X then X filter P Xs else filter P Xs One familiar application of functional languages consists in programming generic problem solving schemes as higher order functions In TOY this technique can be naturally combined with non determinism As an example recall the lazy generate and test technique used in Sec tion 2 12 in order to opmitize a permutation sort algorithm In fact all the applications of the lazy generate and test method to different particular problems follow the same scheme and it is easy to program a single generic solution by means of a higher order function findSol This function expects three parameters a generator Generate a tester Test and an input Input and it returns a solution Solution The generator is applied to the input in order to produce 47 candidate solutions and any candidate which passes the tester can be returned as solution As we already know thanks to lazy evaluation partially computed candidates can be r
18. In addition to purely functional computations JOY has also the ability to solve goals see Section 2 13 Goal solving requires to combine lazy evaluation and the computation of bindings and constraints for logic variables A more precise explanation of TOYV s semantics is given in Appendices F and G Next we show some definitions of simple functions related to list processing Note that the symbol is used in JOY to start a comment which is assumed to fill the rest of the current line To write longer comments it is also possible to enclose the commented text between the symbols open comment and close comment Nested comments are allowed List recognizer null A gt bool null true null X Xs false List selectors head A gt A head X Xs X tail A gt A tail X Xs Xs Accessing the Nth element of a list infixl 90 11 A gt int gt A 27 X Xs N if N 0 then X else Xs N 1 List concatenation infixr 50 A gt A gt A Ys Ys X Xs Ys X Xs Ys Flattenning a list of lists into a single list concat A gt A concat concat Xs Xss Xs concat Xss Splitting a list in two parts take int gt A gt A take N Xs if N O then else take N Xs take N take N X Xs X take N 1 Xs drop int gt A gt A drop N Xs
19. L gt X 7 Z Y gt 7 X in 1 10 Z in 1 10 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms exactly 3 e Type Declaration exactly int int gt int bool e Modes exactly inout inout inout inout e Definition exactly X L N returns true if X occurs N times in the list L e Reifiable No 84 e Example The next goal imposes that the two elements of a list have to be equal to 2 Toy FD gt L X Y domain L 1 2 exactly 2 L 2 L gt 2 2 X gt 2 Y gt 2 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms serialized 2 serialized d 3 cumulative 4 cumulative 5 e Type Declaration serialized int int bool serialized int int serial0ptions bool cumulative int int int int bool cumulative int int gt int int serialOptions bool e Modes serialized inout inout inout serialized inout inout inout inout cumulative inout inout inout inout cumulative inout inout inout inout inout e Definition serialized serialized cumulative and cumulative are useful to solve scheduling and placements problems In general serialized S1 Sn D1 Dn serialized S1 Sn
20. N then z else s N P dv P lt P z N md P if P gt N then N else N P md P lt P z LISTS module list imports nat exporting types nat ops Z S exports data list A nil A list A tail list A gt list A head list A gt A list A gt list A gt list A length list A gt nat reverse list A gt list A take nat gt list A gt list A drop nat gt list A gt list A tail and head are only defined for non empty lists body tail N L L head N L N 207 nil L L N L L WN L L length nil z length N L s length L reverse nil nil reverse N L reverse L N nil take z L nil take N nil nil take s N M L M take N L drop zL L drop N nil nil drop s N M L drop NL ORDERED LISTS module ordlist parameters type elt le elt gt elt gt bool imports list exporting types list elt ops nil tail head length exports is_ordered list elt gt bool insertsort list elt gt list elt mergesort list elt gt list elt quicksort list elt gt list elt body local auxiliary operations insert_list list elt gt elt gt list elt insert_list nil M M nil insert_list N OL M if le M N then M N OL else N insert_list OL M merge list elt gt list elt gt list elt merge OL nil OL merge ni
21. The second defining clause for insertion abbreviates the defining rule insertion X Y Ys X Y Ys true lt X X Y Y Ys Ys The permutationSort example also illustrates the use of curried predicates Uncurried pred icates like those in the ancestorO0f example are also allowed More generally programmers are free to choose either curried or uncurried style for each particular function or predicate def inition Curried style is often favoured because partial applications of curried functions can be used to express functional values see Sections 2 1 and 2 14 37 2 12 Non Deterministic Functions Prolog like predicates illustrate a typical feature of logic programming namely the ability to express don t know non determinism For instance the TOY system can solve the goal permutation 1 2 Ys looking for values of Ys that make the goal true The system will compute the two expected answers namely Ys 1 2 and Ys 2 1 via a backtrack ing mechanism More generally don t know non determinism is useful for solving many search problems in a simple although not always efficient way Don t know non determinism in 70 Y can also be achieved by means of non deterministic func tions A function f is called non deterministic iff some function call f t t with fixed already evaluated arguments can return more than one result JOY allows to define non deterministic functions by means of defining rule
22. We define the operational semantics of TOY by means of a translation function 7 Toy Prolog where Toy and Prolog are the sets of TOY programs and Prolog programs respec tively The translation function which constitutes the core of the implementation of TOY is the result of composing three intermediate functions T pcosfo fo where e fo which stands for first order translates source TOY programs which use higher order syntax into TO like programs written in first order syntax e sf which stands for suspended forms introduces suspensions into first order TOY pro grams a technicality useful for achieving sharing in the execution of TOY programs e pc which stands for prolog code generates properly the Prolog clauses which are the final result of the translation The generation of Prolog code is made as to implement a demand driven strategy for lazy narrowing according to the ideas presented in 22 A crucial step for the code generation will be the construction of the definitional trees of all the functions defined in the TOY program We now give the technical details of all the above mentioned functions G 1 First Order Translation of TOY Programs It consists essentially in the three following changes e Enhancing the signature with new constructor symbols for expressing partial applications of constructor or function symbols and adding a new function symbol read apply e Translating all program rules by writi
23. Y in 1 2 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms 15 An exhaustive description of the finite domain solver is carried out in Chapter 3 page 66 nocflpfd Disables finite domain constraints Constraint solvers should only be activated when needed otherwise the system performance would be slightly degraded The solver for syntactical constraints equality and disequality over constructed terms are always enabled 1 5 6 Miscellanea This section collects the commands which do not fit into former sections io_file loads the library IO File which provides functions to handle text files noio_file unloads this library io_graphic loads the library IO Graphic which provides functions for graphical user interfaces noio_graphic unloads this system module prop enables propagation noprop disables propagation statistics lt level gt Sets the level lt level gt of statistics no statistics runtime 0 1 2 runtime and hnf counter 3 3 full statistics statistics Displays the current level of statistics prolog lt goal gt Executes the Prolog goal lt goal gt status Informs about the loaded libraries as follows Toy gt status Libraries CFLPR not loaded CFLPFD not loaded IO File not loaded IO Graphic not loaded version displays the TOY system version number as follows 16 Toy gt version B Sonia 2 3
24. fdset fdset fdset_complement fdset fdset 98 Modes fdset_intersection fdset_subtract fdset_union in in inout fdset_complement in inout Definition fdset_intersection S1 S2 fdset_subtract S1 S2 and fdset_union S1 S2 return the FD set which is the result of S1 N S2 resp S1 S2 and S1 U 2 Finally fdset_complement S is the complement wrt inf sup of the set S Reifiable Not applied Examples Toy FD gt S1 interval 0 4 S2 interval 3 7 fdset_union fdset_intersection S1 S2 fdset_subtract S1 S2 1 S1 gt interval 0 4 S2 gt interval 3 7 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms Toy FD gt fdset_complement interval 0 1 S gt interval inf 1 interval 2 sup gt Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms fdsets_intersection 1 fdsets union 1 Type Declaration fdsets_intersection fdsets union fdset fdset Modes fdsets_intersection fdset_union in inout Definition fdsets_intersection SL and fdsets_union SL return the FD set which is the result of the intersection resp union of each FD set in the list SL Reifiable Not applied Example Toy FD gt SL interval 0 4 interval 3 7 US fdsets_union SL IS fdsets_intersection SL 99 SL gt interval 0 4 interval
25. inf sup int FD SET FUNCTIONS is_fdset empty _fdset fdset bool fdset_parts int int fdset fdset empty_interval int int bool fdset_interval int int fdset fdset_singleton int fdset fdset_min fdset_max fdset_size fdset int list_to_fdset int fdset fdset_to_list fdset int range to_fdset int range fdset to range range gt int fdset_add_element fdset_del_element fdset int fdset fdset_intersection fdset_subtract fdset_union fdset fdset fdset fdset_complement fdset fdset fdsets_intersection fdsets_union fdset fdset fdset_equal fdset_subset fdset_disjoint fdset_intersect fdset fdset bool fdset_member int fdset bool fdset_belongs int int bool STATISTICS FUNCTIONS fd_statistics bool fd_statistics statistics int bool 70 domain int int int bool Modes domain inout gt in gt in gt inout Definition domain L A B returns true if each element in the list L with integers and or FD variables belongs to the interval A B and also constrains each FD variable in L to have values in the integer interval A B It returns false if no element in L belongs to A B Reifiable Yes Examples The next goal returns true and constrains X and Y to have values in the range 1 10 Toy FD gt domain X Y 1 10 1 X in
26. no Elapsed time O ms or Toy R gt X 2 4 X gt 0 4 0 X 2 0 0 0 X gt 0 0 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms Non linear arithmetic constraints like X 4 in this example are suspended by the constraint solver until they become linear because of variable instantiation At the end of the computation the remaining suspended constraints are shown as part of the computed answer although they might be unsatisfiable Another example using the non deterministic function permutationSort from Section 2 12 and the constraints over reals may be the sorting of a list of numbers one of whose elements is unknown In the goal the unknown element is represented as a logic variable X TOY gt permutationSort 3 2 X yes 2 3 xX X gt 3 0 Elapsed time 10 ms more solutions y yes 2 3 X gt 2 0 X lt 3 0 45 Elapsed time O ms more solutions y yes X 2 3 X lt 2 0 Elapsed time O ms Notice that the three computed answers constrain the position and value of X in all possible ways The second way for computing in TOY is to reduce or evaluate expressions as in functional programming languages In order to compute in this mode the user must type the symbol gt followed by the expression e to be evaluated The system will display the value resulting from the evaluation of e more precisely the first possible value in c
27. sched startType gt startType gt startType gt startType gt startType gt startType gt bool sched S1 S52 53 54 S5 56 Tasks t1 3 t5 t6 m1 1 81 2 8 m1 S2 t3 8 m1 S3 t4 6 t3 m2 54 t5 3 t3 m2 85 t6 4 m2 86 schedule Tasks 1 20 labeling ff S1 S2 S3 84 95 S6 where Tasks defines the set of tasks Observe that the problem for a possible scheduling is limited to time window 1 20 by the goal schedule Tasks 1 20 An example of goal solving is given next Toy FD gt sched S1 S2 S3 S4 S5 S6 180 S1 gt gt 1 S2 gt 4 3 gt 12 S4 gt 1 S5 gt 7 s6 gt 10 Elapsed time 31 ms more solutions y n d y S1 gt 1 S2 gt 4 3 gt 12 S4 gt 1 s5 gt 7 S6 gt 11 Elapsed time O ms more solutions y n d y n A 7 5 A Hardware Design Problem A more interesting example comes from the hardware arena In this setting many constrained optimization problems arise in the design of both sequential and combinational circuits as well as the interconnection routing between components Constraint programming has been shown to effectively attack these problems In particular the interconnection routing problem one of the major tasks in the physical design of very large scale integration VLSI circuits have been solved with constraint logic programming 40 For the sake of conciseness and clarity w
28. 4 2 5 9 3 L2 gt 8 7 3 A L3 gt 4 2 2 3 4 3 2 3 I 18 _A _B 20 B in 3 sup _A in 5 sup Elapsed time 31 ms sol 1 more solutions y n d a y n which means that L1 L2 resp constructs L3 by aligning the fragments as the following table indicates 177 LI L3 L2 L3 4 4 8 4 2 2 2 2 71314 5 123 3 3 9 1432 5 23 3 13 In the program code rsm 9 provides the choice of partitioning with either one of the two available enzymes The last three arguments hold the length of the subsequences found so far The function choose_initial 9 chooses the first fragment and the first call to rsm is made with this invariant holding Finally the procedure choose 2 deletes some element from the given list and returns the resultant list Note that the Boolean functions solve 6 rsm 9 and choose_initial 9 have been written in a Prolog like fashion thanks to the syntactic sugaring allowed in our system whereas choose 2 has been written as a function which returns the list resulting from deleting an element of its input list A 7 4 A Scheduling Problem scheduling toy Here we consider the problem of scheduling tasks that require resources to complete and have to fulfill precedence constraints Figure A 3 shows a precedence graph for six tasks which are labelled as i where X stands for the identifier of a task t Y for its time to complete duration and Z for
29. C D X Y 12247 INEA OC PO oe BIN Y lt D circle point gt real gt region circle A B R X Y X A X A Y B Y B lt R R outside region gt region intersect union region gt region gt region outside R P not P lt lt R intersect R1 R2 P P lt lt R1 P lt lt R2 union Ri R2 P P lt lt Ri P lt lt R2 The operator lt lt is defined in order to know whether a point belongs to a region It simply applies the characteristic function to the point Then the characteristic functions for circles given its radius and its center and rectangles given its left lower corner and its right upper corner are defined Finally some operations over regions are defined the outside of a region and the intersection and union of two regions For instance a point P belongs to the intesection of two regions R and R if it belongs to R and operator it belongs to R A simple goal could be Toy R gt 0 5 0 5 lt lt circle 0 0 1 yes Elapsed time O ms more solutions y n d y no 169 Elapsed time O ms asking whether the point 0 5 0 5 belongs to the circle of center 0 0 and radius 1 A more interesting and involved goal can ask for the points X Y belonging to the region between two rectangles 0 0 This area is the intersection between the big rectangle and the outside of the small rectangle Toy R gt X Y lt lt intersect rectangl
30. D1 Dn Options cumulative S1 Sn D1 Dn R1 Rn Limit cumulative S1 Sn D1 Dn R1 Rn Limit Options return true if it is possible to constrain n tasks Ti 1 lt i lt n each with a start time Si and duration Di so that no task overlaps Particularly cumulative constraints also impose a limit to check that given a resource amount Ri for each task the total resource consumption does not exceed the limit Limit at any time Si Di and Ri are integers or domain variables with finite bounds Options is a list of elements of type serialOptions that enables certain options usually dependent on the problem in order to improve the search of the solutions Specifically speaking 85 path_consistency true enables a redundant path consistency algorithm to improve the pruning static_sets true and edge_finder true active the use of redundant algorithms to take advantage of the precedence relations among the tasks decomposition true actives attempts to decompose the constraints each time the search is resumed precedences L provides a list L of precedence constraints where each element in L has the form V1 Va 1 and I is the greatest value to denote a fictitious lifted top element or lift J with I Integers Each element imposes the constraint Sy I lt Sv if J is an integer and Sy lt Sy otherwise e Reifiable No e Examples Toy FD gt cumulative 0 5 8 1 1 2
31. E Sonia e help h Shows the system help about the command interpreter including evaluation and debugging 1 5 7 Defining New Commands In the previous sections we have described the collection of commands provided by TOY This repertory is small simple and enough for accessing the capabilities of the system Nevertheless there are some other commands that are not essential but can allow a more friendly use of TOY The user can define commands for accessing the operating system from the TOY prompt The file toy ini included with the distribution contains such definitions in the form of Prolog facts The user can edit and modify this file For example for defining a new command dir that shows every file in the current directory the file toy ini includes the following Prolog fact command dir 0 1s 1 The first argument is the name of the command dir the second is the number of arguments 0 in this case the third is the list of arguments represented as Prolog variables starting with capital letters that will be used by the command and the last one is the list of strings that must be appended for building the command only one in this case With this definition the command dir will work in the next TOY session Another useful command may be for accessing a text editor For example if the user wants to use the editor emacs the following line must be included in the file toy ini command edit 1 Filel emacs F
32. However TOY also supports another way of defining non deterministic functions namely to use eztra variables in the right hand sides of defining rules Extra vari ables simply means variables that do not occur in the corresponding left hand side TOY allows extra variables both in the right hand sides and in the conditions of defining rules Extra variables behave as logic variables in the logic programming sense they can be introduced in the course of a computation and become bound to different values later on thus giving rise to non determinism For instance the following non deterministic function computes the inverse of another function given as a parameter Al inverse A gt B gt B gt A inverse F Y gt X lt F X Note that inverse F is intended to behave as the inverse of the function given as actual pa rameter for F However due to the condition F X Y it turns out that inverse F Y is de fined only if Y is a finite value returned by some computation of F For instance the goal inverse length 3 Xs has the solution Xs X0 X1 X2 standing for all possible lists whose length is 3 On the other hand the goal inverse repeat Xs X leads to an attempt to solve repeat X Xs and therefore to non termination because the function repeat returns an infinite list Functions whose definition uses extra variables in right hand sides sometimes return results whose types also depend on extra type variables
33. Many other usual and useful but not strictly needed functions can be found in the file misc toy see Appendix B which reproduces in TOY syntax a subset of Haskell s prelude 2 9 Including Programs In many cases you will want to split a program into smaller pieces or simply use some frequent functions which have been previously collected into a given file this is for instance the case of misc toy For this purpose when writing a program in a file lt Filel gt you can use the directive include lt File2 gt whose effect while compiling lt Filel gt is the same as if the content of lt File2 gt were literally included into lt Filel gt For example you can add at any point a line with the text include misc toy to any program you write being careful not to redefine functions already defined in misc toy 34 2 10 Layout Rule In the examples above we have used some implicit rules about indentation Now we are going to define precisely the layout rule which is borrowed from Haskell The use of the layout rule becomes really useful when dealing with nested local definitions Currently TOY does not support nested local definitions but nevertheless the parser is prepared to take adventage of the layout rule whose knowledge is also helpful for understanding some common error messages The basic unit of TOY source code is the section A section begins with an open bracket followed by a sentence and end
34. Opaque decomposition steps can also arise when solving disequalities f e1 em f e where f is a defined function of arity n gt m This is because any solution of e e for any 1 lt i lt m is a solution of the disequality As we have seen those solutions whose computation involves opaque decomposition can be ill typed The current TOY system gives no warning in such cases 2 15 Finite Failure TOY provides the primitive boolean function fails as a direct counterpart to finite failure in Prolog A call of the form fails e returns true if there is not any possible reduction for e and false otherwise For example using the function head introduced in page 27 we have that fails head reduces to true because the function head is not defined for the empty list while fails head 1 2 reduces to false The semantics of failure in functional logic programming has been widely studied in 23 20 24 21 25 19 For the moment TOY incorporates a restricted version of the constructive failure investigated in such works The restriction is similar to that of negation as finite failure in Prolog in order to ensure the correctness of the answers the expression e in a call of the form fails e must not contain variables Despite of this restriction in the use of this function it provides an interesting resource for programming in a wide range of applications As we have seen Section 2 11 TOY allows predicate definition in a Prolog st
35. The next goal returns true and restricts X and Y to have values in the closed integer intervals 2 10 and 1 9 respectively as a consequence of range narrowing Toy FD gt domain X Y 1 10 X gt Y Y lt X X in 2 10 Y in 1 9 77 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms The next goal shows a use of reification Toy FD gt domain X Y 0 1 X gt Y B X gt 1 Y gt 0 B gt true Elapsed time O ms sol 1 more solutions y n d a y B gt false X lt Y X in 0 1 Y in 0 1 Elapsed time O ms sol 2 more solutions y n d a y no Elapsed time O ms 3 2 5 Arithmetic Constraint Operators Arithmetic constraint operators allow to build linear and nonlinear constraints involving prim itive arithmetic functions as addition subtraction multiplication and division It does not make any sense to reify these operators 2 2 tx 2 2 amp 2 e Type Declaration amp int gt int int e Modes amp inout inout inout e Definition 0p A B also written in infix notation as A 0p B where Op amp imposes the constraint A 0p B and returns true if it is entailed e Reifiable Not applied e Remarks Infix notation allowed amp stands for integer modulus e Priorities 78 infixr 90
36. U U 1 1 1 10 U gt cumulative 0 5 8 1 1 2 I gt true Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms Toy FD gt serialized 1 3 1 1 path_consistency true static_sets true edge_finder true decomposition true precedences d 1 2 1ift 2 B gt true Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms 3 2 8 Propositional Constraints Relational constraint functions returning Boolean values can be arranged into propositional Boolean formulae by means of propositional combinators TOY provides the following propo sitional combinators gt J 2 gt J 2 2 e Type Declaration lt gt gt bool bool bool 86 e Modes lt gt gt inout inout inout e Definition P lt gt Q equivalence returns true if P and Q are both true or false P gt Q implication returns true if P is false or Q is true P Q disjunction returns true if at least one of P and Q is true Note that these constraints demand Boolean expressions which may be Boolean con straints or Boolean expressions in general e Priorities infix 15 lt gt gt infix e Reifiable No e Example Toy FD gt X gt 0 Y X in 1 sup Elapsed time O ms sol 1 more solutions y n d a y Y gt true X in inf 0 Elapsed time O
37. __ 1 Queens solver J 4 marks 0 1 2 4 3 1 4 Queens solver ja 4 6 2 4 6 1 3 5 6 Queens solver Je OGR Solution for _ 0 Queens solver OGR Solver 1 lt _ _ 1 Queens solver _ J 0 1 2 4 3 1 4 Queens solver t 4 9 1 3 6 8 2 4 9 7 5 9 Queens solver lt t _ 1 3 5 7 9 11 2 4 6 8 10 11 Queens solver 11 Figure A 6 Pipeline with Client Server Architecture For the sake of easing the presentation we recourse to one dimensional coordinates for rep resenting the Cartesian plane so that given a LX x LY region we identify each coordinate pair X Y X 0 LX 1 Y 0 LY 1 as X Y x LX Assume that for a given identifier 7 coor I X Y so that I X Y LX Piece locations are defined by one dimensional coordinates The idea to specify this problem is to have a finite domain variable R representing the region to be filled A number J in the domain of R means that we have room for placing a unit square at I i e given coor I X Y we can place at I the unit square defined by its borders X Y X Y 1 X 1 Y X 1 Y 1 An absent value J from R means that a unit square is already located at J in the same sens
38. bool bool bool Functions of this type are intended to represent simple circuits which receive three Boolean inputs and return a Boolean output Given the Boolean functions not and and or defined elsewhere we specify three input one output simple circuits as follows i0 behavior i0 12 11 10 10 il behavior ii 12 11 10 11 i2 behavior i2 12 11 10 12 notGate behavior gt behavior notGate B 12 11 IO not B 12 11 10 andGate orGate behavior gt behavior gt behavior andGate B1 B2 12 I1 IO and B1 12 I1 10 B2 12 11 10 orGate B1 B2 12 11 IO or Bi 12 I1 IO B2 12 11 10 Functions 10 i1 and i2 represent inputs to the circuits that is the minimal circuit which just copies one of the inputs to the output In fact this can be thought as a fixed multiplexer selector They are combinatorial modules as depicted in Figure A 4 The function notGate outputs a Boolean value which is the result of applying the NOT gate to the output of a circuit of three inputs In turn functions andGate and orGate output a Boolean value which is the result of applying the AND and OR gates respectively to the outputs of three input circuits see Figure A 4 These functions can be used in a higher order fashion just to generate or match topologies In particular the higher order functions notGate andGate and orGate take behaviors as pa rameters and build new behaviors corresponding to the logical gates NOT A
39. bool schedule TL Start End true lt horizon TL Start End scheduleTasks TL TL horizon task gt int gt int gt bool horizon S E true horizon N D P R S Ts Start End true lt domain S Start End D horizon Ts Start End scheduleTasks task gt task gt bool scheduleTasks TL true scheduleTasks N D P R S Ts TL true lt precedeList N D P R S P TL requireList N D P R S R TL scheduleTasks Ts TL precedeList task gt taskName gt task gt bool precedeList T TL true precedeList T1 TN TNs TL true lt member TN D P R S TL precedes T1 TN D P R S precedeList T1 TNs TL precedes task gt task gt bool precedes Ti T2 true lt STi start Ti DTi duration T1 ST2 start T2 ST1 DT1 lt ST2 requireList task gt resourceName gt task gt bool requireList T TL true requireList T RIRs TL true lt requires T R TL requireList T Rs TL 179 requires task gt resourceName gt task gt bool requires T R true requires N1 D1 P1 R1 S1 R N2 D2 P2 R2 S2 Ts true lt N1 N2 member R R2 noOverlaps N1 Di Pi R1 S1 N2 D2 P2 R2 2 requires N1 D1 P1 R1 S1 R Ts requires T1 R T2 Ts true lt requires T1 R Ts noOverlaps task gt task gt bool noOverlaps Ti T2 true lt precedes Ti T2 noOverlaps Ti T2 true lt
40. complement of subset e Reifiable Yes e Examples Toy FD gt domain X 1 4 domain Y 3 6 subset X Y B gt true subset X Y X in 3 4 Y in 3 6 Elapsed time O ms sol 1 more solutions y n d a y B gt false not subset X Y X in 1 4 Y in 3 6 Elapsed time O ms sol 2 more solutions y n d a y no Elapsed time O ms Toy FD gt domain X 1 4 domain Y 3 6 inset X Y B gt true X in 3 4 Y in 3 6 Elapsed time O ms sol 1 more solutions y n d a y B gt false X in 1 2 Y in 3 6 Elapsed time O ms sol 2 more solutions y n d a y 72 no Elapsed time O ms Toy FD gt domain X 0 1 domain Y 1 4 setcomplement X Y B gt true not subset X Y X in 0 1 Y in 1 4 Elapsed time O ms sol 1 more solutions y n d a y X gt 1 B gt false subset 1 Y Y in 1 4 gt Elapsed time O ms sol 2 more solutions y n d a y no Elapsed time O ms intersect 2 e Type Declaration intersect int int int e Modes intersect inout inout gt inout e Definition intersect A B returns a variable with the intersected domains of A and B e Reifiable Not applied e Example Toy FD gt domain X O 3 domain Y 1 4 intersect X Y X in 0 3 Y in 1 4 Z in 1 3 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms belongs
41. infix right associative infixl 50 infix left associative infixl 90 amp infix left associative e Example The next goal returns true and constrains X Y and Z to have values in the intervals 1 10 1 10 and 1 100 respectively Toy FD gt domain X Y 1 10 X Y H Z X Y Z X in 1 10 Y in 1 10 Z in 1 100 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms 3 2 6 Arithmetic Constraints The following constraints express a relation between a sum or scalar product and a value and use dedicated algorithms that avoid to allocate temporary variables holding intermediate values sum 3 e Type Declaration sum int int int gt bool int bool e Modes sum inout inout inout e Definition sum L Op V is true if the sum of all elements in L is related with V via the relational constraint operator Op i e if Xeer Op V e Reifiable Yes e Note This constraint implements a dedicated algorithm which posts a single sum instead of a sequence of elementary constraints e Example Toy FD gt L X Y Z domain L 1 3 sum L lt 4 L ay 23 as X gt 1 Y gt t 79 Z gt Ls B gt true Elapsed time O ms sol 1 more solutions y n d a y L gt X Y Z B gt false X Y Z gt 4 X in 1 3 Y in 1 3 Z in 1 3 Elapsed time O ms sol 2 more solutions y n d a
42. int bool e Modes indomain inout inout e Definition indomain A assigns a value from the minimum to the maximum in its do main to A which is an integer or a finite domain variable with a bounded domain It always returns true e Reifiable Not applied e Example The evaluation of the next goal assigns to X each value in its domain via backtracking 76 Toy FD gt domain X 1 2 indomain X X gt 1 Elapsed time O ms sol 1 more solutions y n d a y X gt 2 Elapsed time O ms sol 2 more solutions y n d a y no Elapsed time O ms 3 2 4 Relational Constraints Relational constraints include equality and disequality constraints in the form eo e where o Hs lt lt gt gt and e and e are either integers or FD variables or functional expres sions 2 2 lt 2 lt 2 gt 2 t gt 2 e Type Declaration lt lt gt gt int gt int bool e Modes lt H lt gt gt inout inout gt inout e Definition 0p A B also written in infix notation as A 0p B where Op lt lt gt gt returns true if posting the relation A 0p B entails the constraint store It returns false in other case e Reifiable Yes e Remarks Infix notation allowed e Priorities infix 20 infix infix 30 lt lt bp gt infix e Examples
43. y no Elapsed time O ms scalar_product 4 e Type Declaration scalar product int int int int bool int bool e Modes scalar_product inout inout gt inout inout inout e Definition scalar_product L1 L2 Op V is true if the scalar product in the sense of FD constraint solving of the integers in L1 and the integers or FD variables in L2 is related with the value V via the relational constraint operator Op i e if L1 L2 Op V is satisfied with defined as the usual scalar product of integer vectors e Reifiable Yes e Note This constraint implements a dedicated algorithm which posts a single scalar prod uct instead of a sequence of elementary constraints e Example Toy FD gt domain X Y Z 1 10 scalar_product 1 2 3 X Y Z lt 10 B gt true X 2 VH 3 Z lt 10 X in 1 4 Y in 1 2 Z in 1 2 Elapsed time O ms sol 1 more solutions y n d a y B gt false X 2 YH 3H Z gt 10 80 X in 1 10 Y in 1 10 Z in 1 10 Elapsed time 16 ms sol 2 more solutions y n d a y no Elapsed time O ms As expected the expressions constructed from both arithmetic and relational constraints may be non linear 3 2 7 Combinatorial Constraints Combinatorial constraints include well known global constraints that are useful to solve prob lems defined on discrete domains Often these constraints are
44. 1 10 Y in 1 10 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms The next goal shows a use of reification Toy FD gt domain X 0 1 B gt true X in 0 1 Elapsed time O ms sol 1 more solutions y n d a y B gt false X in inf 1 2 sup Elapsed time O ms sol 2 more solutions y n d a y no Elapsed time O ms Observe that in the first solution B gt true X is constrained to have values in the closed integer interval 0 1 whereas in the second solution B gt false X is constrained to have a value different from those Note The possible values for a finite domain variable lies in the interval inf sup where inf and sup denote respectively the functions that return the minimum and maximum integer values that a finite domain variable can take See section 3 2 9 for the definition of these functions 71 subset 2 inset 2 setcomplement 2 e Type Declaration subset inset setcomplement int int bool e Modes subset inset setcomplement inout inout inout e Definition subset A B returns true if the domain of A is a subset of the domain of B It returns false in other case inset A B returns true if A is an element of the FD set of B It returns false in other case setcomplement A B returns true if no value of the domain of A is in the domain of B It returns false in other case setcomplement is the
45. 2 73 e Type Declaration belongs int int bool e Modes belongs inout in inout e Definition belongs A L returns true if the integer or variable domain takes a value in the list L with integers and or FD variables It returns false in other case e Reifiable Yes e Example The next goal shows a use of reification Toy FD gt domain X O 4 belongs X 1 3 B labeling X X gt 1 B gt true Elapsed time O ms sol 1 more solutions y n d a y a X HF 3 B gt true Elapsed time O ms sol 2 more solutions y n d a y X gt 0 B gt false Elapsed time O ms sol 3 more solutions y n d a y X gt 2 B gt false Elapsed time O ms sol 4 more solutions y n d a y X gt 4 B gt false Elapsed time O ms sol 5 more solutions y n d a y no Elapsed time O ms Note labeling is intended to enumerate the possible solutions when propagation alone is not enough to deliver concrete values This enumeration function is covered in the next section 3 2 3 Enumeration Functions Propagation algorithms usually found in constraint solving are incomplete due to efficiency reasons This means that the solving process can terminate without determining whether a 74 constraint store is entailed or not Enumeration constraints allow to reactivate the search for solutions when no more constraint propagation is possible They ask
46. 3 7 US gt interval 0 7 1 IS gt interval 3 4 gt Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms fdset_equal 2 fdset_subset 2 fdset_disjoint 2 fdset_intersect 2 e Type Declaration fdset_equal fdset_subset fdset_disjoint fdset_intersect fdset fdset bool e Modes fdset_equal fdset_subset fdset_disjoint fdset_intersect in gt in gt inout e Definition fdset_equal S1 S2 return true if both S1 and S2 represent the same FD set fdset_subset S1 S2 return true if S1 is a subset of the FD set S2 fdset_disjoint S1 S2 return true if S1 and S2 have no elements in common fdset_intersect S1 S2 return true if S1 and S2 have at least one element in common If the conditions do not hold the functions return otherwise false e Reifiable Not applied e Example Toy FD gt fdset_intersect interval 0 3 interval 3 4 1 B gt true Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms fdset_member 2 fdset_belongs 2 e Type Declaration fdset_member int fdset bool fdset_belongs int int bool e Modes fdset member fdset belongs inout in gt inout 100 e Definition fdset_member X S return true if X is a member of the FD set S fdset_belongs X Y return true if the domain of X is in the domain of Y Otherwise they return false e Reifiable Not applied e Ex
47. A where A is a fresh type variable A otherwise with a fresh type variable A In this case there is some type error in the expression e e The first three cases are quite easy to understand they just consult the stores Notice that the types taken from the context A are renamed with fresh type variables due to the implicit universal quantification of all the type variables occurring in A The fourth case infers a product type for an expression which represents an ordered pair Similar cases should be added for n tuples n gt 2 The most interesting case is the last one dealing with an application e e In order to infer the type of this expression T obtains types for e and e and then tries to unify the type of e with a functional type in such a way that e can be applied to e This is done with the help of a new type variable A and type unification Notice that the substitution 6 obtained from typing e is applied to I and O when typing e but A is untouched The final substitution returned by T is the composition of the three substitutions obtained during the process If some type error has appeared when typing e or e or the the m g u 9 does not exist then a type error in the application e e has been detected In this case T returns a pair consisting of a fresh type variable and the empty type substitution This behaviour supports an error recovering policy since the fresh variable A represents the most g
48. A Map Colouring Problem The code to solve this problem is shown below include cflpfd toy colour int gt bool colour 11 12 13 14 15 16 17 18 19 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 true lt domain 11 12 13 14 15 16 17 18 19 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 1 4 all_different 11 12 a11_different 11 13 all_different 11 14 a11_different I1 15 all_different 12 13 a11_different 12 15 172 all_different all_different all_different all_different all_different all_different all_different all_different all_different all_different all_different all_different all_different all_different all_different all_different all_different all_different all_different all_different all_different labeling ff 12 12 13 13 14 14 15 16 16 I7 I7 I8 I8 I9 I9 I10 I11 I11 I12 I12 I13 Ti 16 a11_different 12 17 I8 all_different 13 14 18 a11_different 13 19 110 all_different I4 15 110 all_different I4 111 112 a11_different I5 16 112 a11_different I5 113 17 a11_different 16 113 114 a11_different I6 115 I8 all_different 17 115 116 all_different I7 117 I9 all_different 18 117 118 all_different I9 110 118 all_different I9 119 120 all_different I10 111 120 all_differ
49. Appendix B 190 This goal is equivalent to the following Toy FD gt take 3 map lazymagic from 7 This simple example gives an idea of the nice features of TOY that combines FD constraint solving management of infinite lists and lazy evaluation curried notation of functions poly morphism HO functions and thus HO constraints composition of functions and a number of other characteristics that increase the potentialities with respect to CLP FD Pipelines pipelines toy Pipelines can be a powerful tool to solve heterogeneous constraint satisfaction problems and these are easily expressed at a high level in 7OY via applying HO constraints and curried notation For example recall the programs Optimal Golomb ruler OGR N queens and client server Then the goal for some natural N map map queens ff map golomb requests N corresponds directly to the scheme shown in Figure A 6 if we redefine the function process of Section A 2 5 as process 1 The solving of this goal as in the preceding example of client server architecture generates N answers in the form of a N elements list A from an initial request initial 4 each element a A i e each answer of the server with i 1 N and a initial i 1 is used to feed the OGR solver with a marks producing a new list S sa gt Say containing N solutions for OGRs with marks a ay Finally each element 0 with ke 1 a belongin
50. As an example consider the following function zipWithAny A gt 4 B zipWithAny zipWithAny X Xs X Y zipWithAny Xs Note that zipWithAny admits a list Xs of any type as parameter The returned result is a list of pairs X Y whose first components X are the elements of Xs and whose second components Y are fresh logic variables which could become bound later on if the call to zipWithAny was part of a bigger computation From the viewpoint of type discipline it is consistent to assume the existence of a common type for the values of the new variables Y More precisely for arbitrary types A and B and for any list Xs A given as actual parameter zipWithAny Xs can return results of type A B provided that the fresh logic variables Y introduced by the computation are bound to values of type B or remain unbound and are assumed to have type B Of course choosing arbitrary bindings for the extra variables Y could lead to an ill typed list of pairs However the TOY system never attempts to produce arbitrary variable bindings More generally whenever a function f FS with principal type f 7 gt lt gt Tn gt T is defined by defining rules with extra variables in the right hand side the type can contain extra type variables and it must be understood in the following way for any choice of the types to be replaced for the type variables occurring in 7 gt gt Tn gt T and for any actual parameter
51. ConsOperator Analogous to an operator but beginning by Table D 1 shows the set of reserved symbols keywords which cannot be used for any other purpose they are deserved to See section 2 In this and following tables if reserved occurs next to a symbol it means that this symbol is reserved for a forthcoming release There is also a set of predefined symbols which can be classified as functions data constructors and data types Table D 2 shows the compatibility of user defined symbols versus predefined symbols This table states for instance that the user can define a new data type symbol even if there is a predefined function or data constructor with the same symbol On the other hand the user cannot define a new function with a name which is already defined for a predefined function or data constructor Tables D 3 D 4 and D 5 summarize the functions data types and data constructors in the plain language The user must be aware of the aforementioned compatibility table when defining new symbols in user programs The predefined symbols in the libraries I O File I O Graphic and Finite Domain Constraints are summarized in the following tables Table D 6 shows the predefined functions for the library 217 ok lt lt gt gt gt gt gt gt abs acos acosh acot acoth asin asinh atan atanh ceiling chr collect collectN conti cont2 cos cosh cot coth div do done dVal dValToString
52. Hh N 0 then X Xs else drop N 1 Xs splitAt int gt A gt A A splitAt N 0 0 splitAt N XIXs if N 0 then XIXs else auxForSplitAt X splitAt N 1 Xs Awhere 200 auxForSplitAt X Xs Ys X Xs Ys takeWhile Hae takeWhile P takeWhile P X Xs takeUntil ae takeUntil P takeUntil P X Xs dropWhile ae dropWhile P dropWhile P X Xs span break Hee span P span P X Xs auxForSpan X Xs Ys break P zipWith zipWith Z Bs zipWith Z AlAs zipWith Z AlAs BlBs zip zip Xs Ys where mkpair mkpair X Y unzip unzip unzip X Y XsYs auxForUnzip X Y Xs Ys until A if A if A if gt bool gt A gt A P X then X takeWhile P Xs else gt bool gt A gt A P X then X else X takeUntil P Xs gt bool gt A gt A P X then dropWhile P Xs else X Xs A gt bool gt A gt A A C 0 if PX then auxForSpan X span P Xs else XIXs X Xs Ys Identical to auxForSplitAt span not P A gt B gt C gt A gt B gt C Z A B zipWith Z As Bs A gt B gt A B zipWith mkpair Xs Ys A gt B gt A B X Y A B gt C A B CE auxForUnzip X Y unzip XsYs X Xs Y Ys A gt bool gt A gt A gt A gt A 201 until P F X if P X then X else until
53. L P lt inLine P L inLine P L Notice that this definition is quite declarative uses the logic of the problem and abstract it does not depend of the concrete represention of lines and points but unfortunately it results again in runtime errors Toy gt intersctPoint 1 1 1 1 1 0 RUNTIME ERROR Variables are not allowed in arithmetical operations no Elapsed time O ms To overcome the problem without the use of constraints we must do some homework to calculate explicitly the coordinates of the intersection intersctPoint A B C A B C B C B C A B A B C A X B Now TOY gt intersctPoint 1 1 1 1 1 0 yes P 0 5 0 5 With the use of constraints arithmetic becomes reversible Toy gt cflpr Toy R gt run regions Toy R gt inLine 2 Y 1 1 1 Y gt 3 Elapsed time O ms sol 1 more solutions y n d a y 61 no Elapsed time O ms Toy R gt intersctPoint 1 1 1 1 1 0 P gt 0 5 0 5 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms Furthermore we can solve goals with several solutions obtaining a constraint as an answer Toy R gt inLine P 1 1 1 P gt A _B _B 1 0 _A Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms Linear constraints are active constraints meaning that their satisfiability is effectively checked
54. Moreover the implicit operation which applies a function to its argument has always greater priority than any infix operator For instance the expression f x 3 is parsed as f x 3 rather than f x 3 Operators may also be used for data constructors In such cases the operator s name must start with the character For instance a datatype for complex numbers can be defined as follows infix 40 data complex real real TOY has two syntactic conventions used to relate the use of operators and ordinary functions e An operator symbol enclosed between brackets becomes a function identifier to be used in prefix notation For instance the two expressions 2 3 and 2 3 are equivalent e An ordinary function identifier enclosed betwenn backward quotes becomes an infix op erator For instance the two expressions mod X 2 and X mod 2 are equivalent 30 TOY also supports the useful notion of section borrowed from languages of the Haskell family For any binary operator 9 71 gt 72 gt T sections are obtained by supplying one of the two missing arguments More precisely assuming given expressions a 71 42 72 one can build the sections a1 T2 gt T and Haz T gt T which stand for the functions waiting for the missing argument For instance 2 is a section of the multiplication operator it behaves as a function which doubles its argument Since JOY does not support A abstraction
55. O Graphic Library Predefined Data Types 219 tkActive tkCanvas tkEntry tkInit tkList tkMessage tkRectangle tkScale tkTextEdit tkAnchor tkBackground tkBottom tkCenter tkCheckButton tkCmd tkExpand tkExpandX tkExpandY tkItems tkLabel tkLeft tkListBox tkMButton tkMenu tkMMenuButton tkMSeparator tkOval tkRef tkRefLabel tkRight tkScrollH tkScrollV tkTcl tkTop tkWidth tkButton tkCol tkHeight tkLine tkMenuButton tkPolygon tkRow tkText Table D 9 I O Graphic Library Predefined Data Constructors gt Hx gt assignment count element exactly fd_global reserved fd_set fd_var fdset_belongs fdset_equal fdset_member fdset_size fdset_to_interval fdsets_intersection init_fd reserved is_fdset minimum reserved serialized sup gt belongs cumulative empty_fdset fd_closure fd_max fd_size fdmaximize reserved fdset_complement fdset_intersect fdset_min fdset_split fdset_to_list fdsets_union inset isin reserved range_to_fdset setcomplement lt amp all_different circuit cumulative empty_interval fd_degree fd_min fd_statistics fdminimize reserved fdset_del_element fdset_intersection fdset_parts fdset_subset fdset_to_range indomain intersect labeling scalar_product subset all_different circuit domain end_fd reserved fd_dom fd_neighbors fd_statistics fdset_add_element fdset_disjoint fdset_ma
56. O ms Toy FD gt fdset_singleton S 1 false no Elapsed time O ms Toy FD gt fdset_singleton interval 0 1 1 1 B gt false Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms fdset_min i fdset_max 1 fdset_size 1 e Type Declaration fdset_min fdset_max fdset_size fdset int e Modes fdset_min fdset_max fdset_size in inout e Definition fdset_min S and fdset_max S returns the lower bound upper bound resp of the FD set S fdset_size S returns the cardinality of the FD set S e Reifiable Not applied e Example Toy FD gt domain X 0 1 S fd_set X Min fdset_min S Max fdset_max S Size fdset_size S S gt interval 0 1 Min gt 0 96 Max gt 1 Size gt 2 X in 0 1 Elapsed time 10 ms sol 1 more solutions y n d a y no Elapsed time O ms list_to_fdset 1 fdset_to_list 1 e Type Declaration list_to_fdset int fdset fdset_to_list fdset int e Modes list_to_fdset fdset_to_list in inout e Definition fdset_to list S returns the list equivalent to the input FD set S list_to fdset is the inverse function of fdset_to_list e Reifiable Not applied e Example Toy FD gt fdset_to_list list_to_fdset 0 1 L gt 0 1 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms range_to_fdset 1 fdset_to_range 1
57. O position and puts the new I O position at the beginning of the following line As an example let us redefine the function copyFile using the operations contained in the system module io_file copyFile io unit copyFile do putStr First File Filel lt getLine putStr Second File File2 lt getLine H1 lt openFile Filel readMode H2 lt openFile File2 writeMode copy_content H1 H2 copy_content handle gt handle gt io unit copy_content H1 H2 do B lt end_of_file H1 if B then closeFile H1 gt gt closeFile H2 else do C lt getCharFile H1 putCharFile H2 C copy_content H1 H2 5 5 Graphic Input Output TOY provides a graphical user interface for application programs similar to that existing in the lazy functional logic language Curry 15 To this end TOY incorporates a system module based on Tcl Tk which provides different functions to create friendly interfaces In order to use the graphic functions it is needed to load the system module io_graphic using the command io_graphic The system module can be unloaded by executing the command noio_graphic The system module io_graphic defines operations allowing the communication between TOY and Tcl Tk by means of a new datatype channel which is implementation dependent The basic functions provided by the system module noio_graphic are the following openWish string gt io channel readWish channel gt io
58. Optimization Functions Optimization problems have been acknowledged as an important field of operations research and have been identified in real life applications as planning scheduling and timetabling to name a few An optimization problem is understood in the context of a set of constraints and a cost function which needs to be maximized or minimized A cost function may represent profit resources or time for instance 7OY provides several optimization functions for real constraints e minimize real gt real The application minimize X returns the minimum for X which represents the cost func tion in the context of the constraints in the real constraint store X is demanded to be in head normal form The evaluation of this application raises an exception if either there are suspended non linear constraints or unboundedness is detected e maximize real gt real The application maximize X is equivalent to the application minimize X The following is an example of using this function Toy R gt 2 X Y lt 16 X 2 Y lt 11 X 3 Y lt 15 Z 30 X 50 Y maximize Z X gt 7 00000000000001 63 Y gt 1 9999999999999956 Z gt 310 00000000000006 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms In this example if minimization is used instead of maximization an exception is raised because of unboundedness Another example shows an optimization problem with infinite values
59. Q AlAs deltaGen D I Fs D Q A As 163 And the accepting function accept automata gt word gt bool accept D I Fs W member deltaGen D I F I W Fs member A gt A gt bool member X false member X Y Ys if X Y then true else member X Ys When recognizing languages with automotatas in practise it is usefull to transictions with labels that represent any character distinct from or any character For example an automata for recognizing the word end could be Here 0 is the initial state 3 is the final state and 4 stands for an error state The label x represents any character and e represents any character except e According to the previous representation this automata would be end delta 0 3 and the transiction function would be expressed as delta 0 e delta 1 n 2 delta 2 d 3 default delta S C 4 Now using failure we can eliminate the construction default and write in TO delta S C delta SC delta S C 4 lt fails delta S C delta 0 e 1 delta 1 n 2 delta 2 d 3 With this automata the call accept end end reduces to true and with an other string produces false as expected Here the use of failure for expressing default rules allows to abreviate definitions we could define 6 for any character But this use is more critical when programming non deterministic automata For example assume the aut
60. Symposium on Functional and Logic Programming pages 170 184 London UK 2001 Springer Verlag Rafael Caballero and Mario Rodriguez Artalejo A declarative debugging system for lazy functional logic programs Electr Notes Theor Comput Sci 64 2002 T H Cormen C E Leiserson and R L Rivest Introduction to algorithms MIT Press Cambridge MA USA 2001 Luis Damas and Robin Milner Principal type schemes for functional programs In POPL 82 Proceedings of the 9th ACM SIGPLAN SIGACT symposium on Principles of program ming languages pages 207 212 New York NY USA 1982 ACM Press S Est vez Martin A Fern ndez T Hortal Gonz lez M Rodr guez Artalejo F S enz P rez and R del Vado V rseda A Proposal for the Cooperation of Solvers in Constraint Functional Logic Programming ENTCS 2007 In Press A J Fern ndez M T Hortal Gonz lez and F S enz P rez Solving combinatorial prob lems with a constraint functional logic language In P Wadler and V Dahl editors 5th In ternational Symposium on Practical Aspects of Declarative Languages PADL 2003 num ber 2562 in LNCS pages 320 338 New Orleans Louisiana USA 2003 Springer Verlag 149 10 11 12 13 14 15 16 17 18 19 20 22 Michael Gelfond and Vladimir Lifschitz The stable model semantics for logic programming In Robert A Kowalski and Kenneth Bowen editors Proceedings of the Fifth Intern
61. TOY allows higher order function definitions We next show all these characteristics by means of examples A 2 1 Arithmetic for Peano Numbers arithmetic toy The next example defines addition and multiplication for Peano natural numbers Datatype for Peano Natural Numbers data nat z s nat Addition and Multiplication for Peano Numbers infixr 40 nat gt nat gt nat X z X X s Y s X Y infixr 50 x nat gt nat gt nat X z Z X s Y s X Y X This TOY program could be considered a Haskell program by ignoring the syntactic differences of upper and lowercase identifiers for variables and constructors We can use this program to compute the value of expressions as in any functional language 155 Toy gt gt s zt s s z Cs s sz Elapsed time O ms The symbol gt indicates to the system that we are going to evaluate an expression In this case we could also have tried the same goal in the shape of a TOY goal Toy gt s z s s z R gt s s s z Elapsed time O ms more solutions y n d y no Elapsed time O ms More noticeable is the skill of TOY in solving goals with logic variables For example the next goal asks for all the decompositions of number 3 as the addition of two numbers X and Y Toy gt X Y s s s z X gt s s s z Y gt z Elapsed time O ms more solutions y n d y X gt s s 2
62. TOY as well all of these possibilities can be encoded by defining a non deterministic predicate However in TOY we can also define a suitable non deterministic function which renders a more expressive solution in this case Next goal shows how the different output lists are computed Toy gt insert 1 2 4 6 X X gt 1d 34 61 Elapsed time O ms more solutions y n d y X gt 124 4 813 Elapsed time O ms more solutions y n d y X gt 124 16 Elapsed time O ms more solutions y n d y gt 2 4 6 11 Elapsed time O ms more solutions y n d y no Elapsed time O ms A 3 2 The Choice Operator choice toy The following operator captures the essence of non deterministic functions It is called the choice operator and selects either of its two arguments infixr 20 A gt A gt A 161 X Y X X Y Y For instance the function insert can be rewritten in the following more appealing way insert A gt A gt A insert X J X insert X YlYs X Y Ys Ylinsert X Ys which yields the same results as above A 3 3 The Inverse Function inverse toy The following is a function that computes the inverse of a given function F Its definition says that X is image of Y through the inverse of F if F X Y Notice that X does not appear at the left hand side of the function inverse A gt B gt B gt A inverse F Y X lt F X For ins
63. X Y Z 0 10 X lt Y Y lt Z fd_closure X L gt _D _E X Ys Z Z7 Y Y gt X X in 0 8 Y in 1 9 Z in 2 10 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms inf sup 0 e Type Declaration inf sup int e Modes inf sup e Definition inf and sup return respectively the minimum and maximum values that a finite domain variable can be assigned to e Reifiable Not applied Example Toy FD gt Min inf Max sup Min gt 33554432 Max gt 33554431 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms 3 2 10 FD Set Functions TOY provides a set of impure functions for managing FD sets during goal solving It does not make any sense to reify FD set functions is _fdset 1 92 e Type Declaration is_fdset int bool e Modes is fdset in inout e Definition is_fdset S returns true if S is a valid FD set Otherwise it returns false e Reifiable Not applied e Example Toy FD gt is_fdset interval 0 1 B1 is_fdset interval 1 0 B2 B1 gt true B2 gt false Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms empty_fdset 1 e Type Declaration empty_fdset int bool e Modes empty_fdset inout inout e Definition empty _fdset S returns true if S is an empty FD set Otherw
64. X3 48789 X4 4657 X6 34539 X7 249912 85698 X1 78219 X5 O 85176 X1 57898 X4 15883 X5 50547 X6 83287 X7 373854 95332 X2 1268 X3 O 87758 X2 19346 X4 70072 X5 44529 X7 740061 10343 X1 11782 X3 36991 X6 O 49149 X1 52871 X2 56728 X4 146074 7132 X3 33576 X5 49530 X6 62089 X7 O 29475 X2 34421 X3 62646 X5 29278 X6 251591 60113 X1 H 76870 X4 15212 X7 22167 29101 X2 5513 X3 21219 X4 O 87059 X1 22128 X5 7276 X6 57308 X7 821228 76706 X1 48614 X6 41906 X7 0 98205 X2 23445 X3 67921 X4 24111 X5 175 labeling Label LD And a goal for this program Toy FD gt equation20 ff L L gt 1 4 6 6 6 3 1 Elapsed time 16 ms more solutions y n d y no Elapsed time 47 ms A 7 3 DNA Sequencing dna toy In this section we show a simplified version of restriction site mapping RSM taken from 17 A DNA sequence is a finite string over the elements A C G T An enzyme partitions a DNA sequence into certain fragments The problem consists of reconstructing the original DNA sequence from the fragments and other information taken from experiments To keep the problem concise we consider a simplification of this problem which only de
65. a new operation that when performed first does p ignoring the value returned and then does q For instance the built in function putStr in Section 5 1 could be defined as follows utStr string gt io unit P 8 putStr done putStr C Cs putChar C gt gt putStr Cs 126 Similarly the built in function putStrLn in Section 5 1 can be defined using gt gt and the function putStr it prints a newline character after printing the string putStrLn string gt io unit putStrLn Cs putStr Cs gt gt putChar n Note that the use of the operator gt gt is only useful when the value returned by the first argument is not needed in the computation more precisely it is not needed by the second argument If the value of the first action should be taken into account by the second action it is necessary to use the more general operator gt gt The combination p gt gt q is an action that when performed first does p returning a value x of type A after this the action q x is executed returning a final value y of type B In fact gt gt can be easily defined in terms of gt gt gt gt io A gt io B gt io B P gt gt Q P gt gt constant Q constant B gt A gt B constant Y X Y As a more practical example the built in function getLine in Section 5 1 can be implemented as follows getLine io string getLine getChar gt gt follows_1 follows_1 char gt
66. a second answer we get no termination This behaviour is due to the fact that there is a pending alternative for the second rule in the definition of length which is a rule that can always be applied provided that its first argument is unbound Observe that the length of the list is not limited to be positive on the right hand side of this rule Finite domain constraints can be applied to impose such a limit Note that this cannot be done without the use of constraints since the function length should allow different modes of usage Then a new definition using constraints is as follows include cflpfd toy hasLength A gt int gt bool hasLength 0 true hasLength X Xs N N gt O hasLength Xs N 1 Now we can submit the following goal and request all the solutions 103 Toy FD gt hasLength L 2 L gt Ay B Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms This definition for hasLength accepts all modes of usage 3 3 2 Send More Money smm toy Below a TOY program for solving the classical arithmetic puzzle send more money is shown Observe that TOY allows to use infix constraint operators such as gt to build the expression X gt Y which is understood as gt X Y The intended meaning of the functions should be clear from their names definitions Tables 3 1 and 3 2 and explanations given in Section 3 2 include cflpfd toy smm int gt label
67. allows to solve disequality conditions without demanding complete evaluation of the expressions e A more formal explanation of strict equality and disequality can be found in Section 2 16 and Appendix F Inequality conditions e1 lt gt e2 with lt gt lt gt work for numbers of type int and real with the obvious arithmetic meaning In addition to their r le in conditions the symbols lt gt lt gt lt gt can be freely used as boolean functions in infix notation Each local definition D must have the form s d where d is an arbitrary expression and s is a linear flat pattern having either the form X variable or c X Xi c being an l ary data constructor Moreover the sequence Dj Dp of local definitions must be such that the following three properties are satisfied 1 For all 1 lt i lt p s and ft tn share no variables 2 For all 1 lt 7 lt j lt mi si and sj share no variables 3 For all 1 lt i lt m 1 lt j lt i s and dj share no variables Intuitively a local condition s d has the effect of matching the pattern s to the value obtained by evaluating the expression d and binding the variables occurring in s accordingly Therefore local definitions can be said to define values for the variables occurring in the patterns 1 Actually transparent patterns See Section 2 14 for an explanation of this technical notion 2More general conditions
68. also called symbolic constraints 2 These constraints implement dedicated algorithms which are more efficient than posting elementary constraints all_different 1 all different 2 e Type Declaration all different int bool all_different int allDiffOptions bool e Modes all different inout inout all_different inout inout inout e Definition all_different L returns true if each finite domain variable with bounded domain in L is constrained to have a value that is unique in the list L and there are no duplicate integers in the list L i e this is equivalent to say that for all X Y L XX Y The extended version all_different L Options allow one more argument which is a list of options This list can take at most one value from the following two groups 1 on value on domains or on range to specify that the constraint has to be woken up respectively when a variable becomes ground when the domain associated to a variable changes or when a bound of the domain in interval form associated to variable changes 2 complete true or complete false to specify if the propagation algorithm to apply is complete or incomplete e Reifiable No e Example 81 Toy FD gt L X Y Z domain L 1 3 all_different L complete true on range L gt X ZII all_different X Y Z complete true on range X in 1 3 Y in 1 3 Z in 1
69. and disequality constraints e Four new non declarative primitives collect collectN once and fails have been included 259 collect e collects in a list all the values obtained when evaluating the expression e For instance a goal as collect 3 4 5 R has one answer R gt 3 4 5 The elements of the list correspond to all the values V computed for the goal e V If e V has no answer then collect e returns collectN n e collects in a list the n first values obtained when evaluating e For instance a goal as collectN 2 3 4 5 R has one answer R gt 3 4 If e cannot be evaluated to n values the primitive fails once e is equivalent to head collectN 1 e fails e returns true if the goal e V fails or false if the goal e V has some answer For instance the goal fails head R has the single answer R gt true In contrast fails head X Xs R has the single answer R gt false e The system can display statistics about the number of head normal forms the system memory or the number of the choice points required by the underlying Prolog program during a certain computation See statistics in the help command displayed by typing help to check all the possibilities Fixed Bugs e The finite domain library was not working properly if no program was compiled after typing cflpfd Fixed e Fixed an error which involved the combination of disequality and equality with r
70. dy 2 317 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms Another example may be Toy gt 1 F F gt 1 ee Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms In this case the normal form 1 is a partial application of the function and it is shown in infix notation See also the next example based on the former one which applies the pattern F the partial application to a list Toy gt 1 F F 2 F gt 1 L gt 1 2 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms After equalities disequalities are shown enclosed between curly brackets The solved form for a disequality is X t where t is a normal form A computation involving disequalities may be Toy gt 1 Xs 1 2 2 f AS Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms If the constraint solver over the real numbers is working see Section 1 5 5 then the computed answer can also contain constraints of this kind that will be showed in the last place The solved form for them is provided by the solver of Sicstus Prolog For example if the constraint solver for real numbers has been activated one can solve goals as 44 Toy R gt X Y Z 3 X Y Z Y gt 1 _C 1 0 X Z 2 0 X _D 1 0 X Elapsed time O ms sol 1 more solutions y n d a y
71. even odd lstEven from and the dependences odd lt even even lt odd even lt lstEven and odd lt IstEven One possible sequence of blocks that satisfies i and ii is even odd lstEven from The functions even and odd are mutually recursive so they must appear in the same block the function lstEven depends on even so the block lstEven must appear after the block that contains even and as the function from does not depend on any other function it constitutes a single block In fact the block from could appear at any position of the sequence The second and main step of the type inference algorithm takes as input the sequence of blocks B Bn resulting from the dependency analysis E 2 Type Inference Algorithm The sequence of blocks B Bn determines the order in which type inference must be per formed The types of the functions belonging to each block B must be inferred simultaneously after having inferred the types of all functions belonging to the preceding blocks B 1 lt i lt j We distinguish two roles for occurrences of function symbols in the defining rules of the program 228 an occurrence can have a definition role or it can have a use role For example the symbol f in the left hand side of a defining rule for f plays a definition role and also every occurrence of f in the right hand side the conditions or the local definitions of the rule since the rule is part of the definition of f The rol
72. file in subsequent computations If Mode is readMode then the file is opened for input This implies that the file Name must exist Otherwise a runtime error will appear If Mode is writeMode then the file is opened for output Here there are two possibilities If the file Name already exists then its content is removed and replaced by the following writings Otherwise the file Name is created Finally if Mode is appendMode then the file Name is opened for output and the current I O position indicating where the next output operation will occur is positioned at the end of the file As for writeMode the file Name may exist or not and the behaviour is similar The execution of the action closeFile Handle closes the text file referenced by Handle whereas the execution of end of file Handle returns true if no further input can be taken from the file referenced by Handle Otherwise it returns false 130 getCharFile Handle reads the character situated in the current I O position of the file refer enced by Handle putCharFile Handle C has a similar behaviour but it writes the character C In both cases the current I O position advances one character Finally putStrFile Handle Cs writes the string Cs from the beginning of the current I O position putting this at the end of the string putStrLnFile Handle Cs does the same but it prints a newline character after printing the string getLineFile Handle reads the rest of the line from the current I
73. further solutions obtaining all possible assignments of pieces in the region even if the region is not completely filled If we want to fill the region we have to ensure that the region is empty A straightforward condition is to test that all the available positions are occupied by pieces that is the cardinality of the region domain is the number of points where pieces cannot be allocated Given the function empty defined as follows empty int gt bool empty R fd_size R spaceX spaceY 1 So we can submit the goal Toy FD gt domain R 0 15 pieces R L empty R This problem can be augmented with other constraints such as the cost of filling the region with particular costs for each piece Finally note that regions to be filled can have any shape and even they have neither been connected nor convex A 7 8 Programmable Search search toy As an example of practical use of the reflection functions here we show a two search strategies First a naive one implemented with the function search naive 1 which selects the variables to be labeled following the ordering of the input list and the values in their domains in ascending order Second one of the most popular labeling strategies often supported by most constraint systems the so called first fail strategy implemented with the function search_ff 1 that selects the variable to be labeled which has the least number of values in its domain and selects the values i
74. io string follows_1 C if C n then return else getLine gt gt follows_2 C follows_2 char gt string gt io string follows_2 C Cs return C Cs As a second practical example here we have a function which reads three characters from the keyboard and prints them on the screen read_3_chars io unit read_3_chars getChar gt gt continue_1 continue_1 char gt io unit continue_1 C1 getChar gt gt continue_2 C1 continue_2 char gt char gt io unit continue_2 C1 C2 getChar gt gt continue_3 C1 C2 continue_3 char gt char gt char gt io unit continue_3 C1 C2 C3 putChar C1 gt gt putChar C2 gt gt putChar C3 127 Note that the definition of the very simple function read_3_chars requires three auxiliary functions In order to facilitate the use of input output we have incorporated the do notation described in next section This facility is available also in Haskell and Curry 5 3 Do Notation Do notation provides a more comfortable syntax for using input output in TOY avoiding the need of auxiliary functions Using the construction do instead of sequences of the operator gt gt leads to a programming style which achieves a declarative specification of I O actions while rendering their intended imperative effects intuitively clear For example the do notation allows to write more intuitive definitions for the functions getLine and read_3_chars in the previous
75. is not valid 6 3 2 Looking for buggy nodes The user can navigate the tree providing information about the state of the nodes by using the menu option Node 144 Node miv Valid i x Non Valid i Unknown Apart from valid and Non valid there are three other possible states e Buggy The user cannot indicate that a node is buggy only the system changes a node state to buggy after checking that it is not valid and all its children are valid We have proved that a buggy node has always an incorrect program rule associated the program rule used to compute the function call represented in the node After finding a buggy node the debugger displays the number of the rule associated and the debugging session ends e Unknown The user doesn t know if the node is valid or not All the nodes are marked as unknown at the beginning e Trusted The function associated to the basic fact in the node can be trusted i e the node is valid and all the nodes corresponding to the same function are also valid Hence changing a node to this state will change all the nodes containing basic facts associated to the same function to trusted as well 6 3 3 Strategies For large trees the process of finding a buggy node can be tiresome In these cases in fact in almost all the cases it is convenient to use a fixed strategy DDT provides two of such strategies the top down and the divide and query The top down strategy behaves essentially like
76. it The monadic style ensures that in any step of a computation there is a unique version of the world Output operations have type io unit because they yield an uninteresting value of type unit a predefined type which contains one single value Input operations which yield a value of some interesting type T unit have type io 7 The two monadic binding functions used to sequence input output operations are gt gt and gt gt which will be carefully described in Section 5 2 As an alternative to writing combinations of gt gt TOY offers the possibility of using the do notation whose description can be found in Section 5 3 In addition to the standard input output TO provides also text files see Section 5 4 and a declarative Graphical User Interface GUI which has been developed following the ideas presented in 15 More concretely the graphic input output has been implemented by means of a GUI system module based on Tcl Tk 30 see Section 5 5 Finally in Section 5 6 we describe list comprehensions a powerful notation to write expres sions of type list which is available also in Haskell and some other functional logic languages List comprehensions are a useful device for computing several solutions while avoiding non deterministic search in a context where monadic I O is needed For this reason they have been added to TOY during the development of the monadic I O facilities although they are also useful for other purposes
77. mean to order the three lists removing the elements that are duplicate in the lists that is to say merge3 U VW UaV aW where the operation a 2 is defined as follows JaV V Ual U X Xs a Y Y s X Xs a Ys X X Xs a Y Y s X Xs a Y Ys X lt Y X Xs a Y Y s Y X Xs a Ys X gt Y and finally to add the element 1 as initial element A schematic picture is shown in Figure A 1 A solution is shown below where merge2 defines the operator a include misc toy merge3 int gt int gt int gt int merge3 U V W merge2 merge2 U V W 158 2 4 6 map 2 ja PEPEN map 3 ja 5 10 15 a map 5 je 1 2 3 4 5 l Figure A 1 Hamming Codes merge2 int gt int gt int merge2 V V merge2 U U merge2 X Xs X Ys merge2 X Xs YIYs merge2 X Xs YIYs X merge2 Xs Ys X merge2 Xs YIYs lt X lt Y Y merge2 X Xs Ys lt X gt Y hamming int hamming 1 merge3 map 2 hamming map 3 hamming map 4 hamming The next goal computes the 12 first Hamming numbers Toy FD gt gt take 12 hamming 1 2 3 4 6 8 9 12 16 18 24 27 Elapsed time 47 ms A 2 5 Process Network Client Server Interaction clientserver toy Processes can be considered as functions consuming data i e arguments and producing values for other functions Proce
78. ment propagation rules relying on the available bridges are used for building a mate constraints which are submitted to the mate solver think of R as the mate of FD and viceversa Propa gation enables each of the two solvers to take advantage of the computations performed by the other In order to maximize the opportunities for propagation the goal solving procedure has been enhanced with operations to create bridges whenever possible according to certain rules listed in Tables 4 1 and 4 2 These tables use the notation t t2 t3 in order to illustrate the process flattering of goal solving procedure For example the goal RX 2 lt 3 is flattered to constraints RX 2 Z and Z lt 3 where Z is a new variable When constraints are totaly flatted then they are submitted to solver and in this moment take place propagation it is explained in 8 4 4 1 Propagation from FD to R In order to propagate a constraint from FD to R we follow two steps First is checked if each variable has its corresponding bridge if the variable has not bridge then a bridge is created using a new real variable From FD to R always is possible to create bridges since all integer value is a real value Afterwards new real constraints are building and submitted to real solver Constraints that support propagation from FD to R are listed in Table 4 1 and explained below domain X1 Xn ab e Creation of Bridges If X has no bridge then X
79. ms sol 2 more solutions y n d a y no Elapsed time O ms 3 2 9 Reflection Functions TOY provides a set of impure functions called reflection functions that allow to both recover information about variable domains and to manage FD sets during goal solving It does not make any sense to reify reflection functions fd_var 1 e Type Declaration fd var int bool e Modes fd var inout inout e Definition fd_var V returns true if Vis an unbound FD variable in the constraint store 87 e Reifiable Not applied e Example Toy FD gt domain X O 1 fd_var X BX fd_var Y BY fd_var 1 Bl X 1 fd_var X BX1 X gt 1 BX gt true BY gt false B1 gt false BX1 gt false Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms Note In particular this example shows the impure behaviour of this reflection function since the meaning of fd_var X depends on its location in the goal expression fd_min 1 fd_max 1 e Type Declaration fdmin fdmax int gt int e Modes fd min fdmax inout inout e Definition fdmin V and fd_max V return the smallest greatest value in the current domain of V e Reifiable Not applied e Example Toy FD gt domain X 0 10 Min fd_min X Max fd_max X Min gt 0 Max gt 10 X in 0 10 Elapsed time O ms sol 1 more solutions y n d a y no
80. n gt 0 where a logic variable F is acting as a function Let us speak of goals with higher order logic variables to describe this situation Some binding for the higher order logic variable F must be computed in order to solve such goals This can happen in two ways 49 1 Generated bindings some previous goal solving step binds variable F before coming to the computation of F ej en This was the case in the family relationships example above 2 Guessed bindings no previous goal solving step has bound F Then in order to continue the computation of F e e TOY guesses some pattern of the form h X1 Xm with fresh logic variables X as binding for F In fact the system uses backtracking to try all possible bindings of this form In each case the computation continues and may lead to different solutions of the goal Generated bindings of higher order logic variables are unproblematic Guessed bindings on the other hand can give rise to ill typed solutions For instance solving the well typed goal map F true X Y false requires to guess a binding for the higher order logic variable F One possibility is 1 which leads to an ill typed solution because the principal type of is incompatible with the type that must be assumed for F in order to well type the goal In general guessed bindings of higher order variables can produce ill typed solutions because the current TOY system does not check type con
81. o tupleType PATTERNS m less than the arity of the function m less or equal than the arity of the constructor pattern function simplePat simplePat constructor simplePat simplePat simplePat Patterns that can appear in the lhs of a function rule fPat nPlusk asPattern simplePat Simple patterns simplePat varld constructor function constant listPat tuplePat pattern SS 223 Lists of patterns listPat pattern E pattern pattern rm pattern pattern Tuples of patterns tuplePat pattern gt pattern n k patterns nPlusk varld Integer as patterns asPattern varld Q simplePat EXPRESSIONS expr simpleExpr appExpr Simple expressions simpleExpr doExpr list tuple intensionalExpr aExpr Applications appExpr aExpr expr expr op expr Argument expressions expressions that can be applied to some arguments aExpr aAtom section Jexpr 224 Appliable atoms aAtom varld constructor function Left and right sections NS section simpleExpr funOp funOp simpleExpr SS
82. of appendices include programming examples predefined functions and library modules and some technical specifications concerning the syntax and semantics of the language TOY has been designed by the Declarative Programming Group at the Universidad Complutense de Madrid following previous experiences with the design of declarative languages The finite domain library has been developed in cooperation with Antonio Fern ndez Leiva from the Uni versity of M laga In addition to the authors of the report many people have contributed to the development of the system We would like to acknowledge the work of Mercedes Abeng zar Carneros Juan Carlos Gonzalez Moreno Javier Leach Albert Narciso Marti Oliet Juan M Molina Bravo Ernesto Pimentel S nchez Maria del Mar Rold n Garc a and Jos J Ruz Ortiz Chapter 1 Getting Started 1 1 Supported Platforms and System Requirements The current version TOY works on most operating systems which are the ones supported by SICStus Prolog 36 This Prolog system version 3 8 4 or higher is required whenever you want to use JOY from a Prolog interpreter as will be described in the next section Any way you can also use the binary distributions which do not require any installed Prolog sys tem In this case JOY has been tested to work on the following operating systems Windows 98 NT ME 2000 XP 2003 Linux and Solaris In addition some features of Toy need additional software Feature Re
83. of solutions together in an structure like a list Prolog provides several predicates for this issue like findall Using failure we can obtain all the results of the evaluation of any expression but in fact TOY facilitates the work by providing a number of primitives for such issues The first one is collect e that returns the list of possible values for the expression e For example for the program of graphs introduced above we can evaluate Toy gt collect next a L gt b c Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms This is the list of the nodes adjacent to the node a as expected For the Nim s game we can evaluate 53 Toy gt collect winMove 2 2 2 L gt 0 2 2 2 0 2 122 0117 Elapsed time 78 ms sol 1 more solutions y n d a y no Elapsed time O ms Toy gt collect winMove 2 2 L gt 11 7 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms The first goal provides the list of states lists that represent the possible winning moves from the state 2 2 2 while the second one shows that there is no possible winning movement from 2 2 this means that there is not any possible movement that guaranties our victory of course the other player can make a wrong movement like 0 2 in such a way that we will win Another primitive is collectN M e that returns a list with the first M results for the expression e For exam
84. rules are indeed deterministic A goal such as ancestor0f alan P can be solved by the TOY system The expected answers will be computed by backtracking They are P paul zs rose P john mary Maybe the most paradigmatic example of non deterministic function is the non deterministic choice from two given values This choice operator can be programmed in TOY as follows infixr 20 Ao ADA X Y gt X X Y gt Y The choice operator allows a more succint presentation of other non deterministic functions For instance an alternative definition of the ancestorOf function can be written as ancestorOf X gt parentOf X ancestor0f parentOf X or also as follows taking advantage of a ocal definition to avoid repeated computations of parents ancestorOf X gt Y ancestorOf Y where Y parentOf X A well known problem solving method involving non determinism is generate and test which works by generating candidates and testing wether they are actual solutions for the problem at hand Programming generate and test in Prolog style leads often to very expensive algorithms because candidates are totally computed before testing A typical example of this situation is the Prolog like permutation sort algorithm shown in Section 2 11 above TOY allows to express a lazy generate and test method where the generator is a non deterministic function rather than a predicate Candidates returned by the gener
85. showed that TOY is fairly efficient as in general behaves closely to SICStus Despite this is not surprisingly as it is implemented on top of SICStus we think that it is important to show that the wrapping of SICStus by TOY does not increase significantly the computation time Moreover in the same paper we showed that TOY is about two and five times faster and even much more in scalable problems than another CF LP FD implementation 26 which is said to be efficient in its Web page http redstar cs pdx edu pakcs 3 1 2 Modes and Bidirectionality Each N arity predefined constraint and constraint related function is listed with its correspond ing modes for arguments and results as function modes where modes is a comma separated list of modes of the form mode0 gt model gt modeN where function has arity N mode 0 lt i lt N is the mode for the th argument modeN is the mode for the result and modei can be e A basic mode in An in mode demands a ground expression inout An inout mode accepts any expression e A constructed mode basic mode Demands a list of elements each one of basic mode basic model basic modeN Demands an N tuple of elements in which the i th element is of basic modei Arguments of predefined functions and constraints with finite types are not demanded and can otherwise be produced For example the second argument of the arithmetic constraint
86. sum stands for a relational constraint operator If it is not provided by the user the system produces all the possible operators The mode for sum is listed as sum in gt inout gt in Some other functions can have several usage modes 3 1 3 Loading the FD Constraint Library TOY does not incorporate automatically FD constraints and thus it is necessary to load the FD extension in order to perform constraint solving This is done with the command cflpfd See also Section 1 5 5 in page 15 for an introductory system session 67 3 2 FD Constraints and Functions In this section TOY constraints and constraint related functions are listed and explained Several of them are reifiable i e a reified constraint represents its entailment in the constraint store with a Boolean variable In general constraints in reified form allow their fulfillment to be reflected back in a variable For example B X Y gt Z constrains B to true as soon as the disequation is known to be true and to false as soon as the disequation is known to be false On the other hand constraining B to true imposes the disequation and constraining B to false imposes its negation Incidentally in CLP FD languages the Boolean values false and true usually correspond to the numerical values 0 and 1 respectively 3 2 1 Predefined Data Types In TOY we have defined a set of predefined datatypes that are used to define the constraints Table 3 1 shows t
87. takes the form e d1 d2 gt qa where e is any TOY expression whose type is the type of the elements of the comprehension list and q 1 lt i lt n is a qualifier that is either e a generator of the form X lt xs where X is a fresh variable of type 7 for some type 7 and xs is an expression of type 7 or e a condiition given as a boolean expression b or e a condition given as a goal G In this case G is treated as a boolean expression i e if the evaluation of G true succeeds then G returns true if the evaluation of G false succeeds then G returns false otherwise the evaluation of the comprenhension list fails As an example given the two partial functions fi 1 g3 1 f 2 2 g4 the comprehension list X X lt 1 2 Y lt 3 4 f g Y can be evaluated to the list 1 2 Note that if we would change the generator X lt 1 2 by the new one X lt 1 2 3 then the evaluation of the comprehension list would fail In fact for any element y of 3 4 neither f 3 g y true nor f 3 g y false succeeds because f 3 is not defined As in functional languages generators must occur before those boolean conditions using the generated variable and as near as possible to them in order to increase the efficiency Comprehension lists are understood as a shorthand for computations involving conditional ex pressions and the functions map and concat defined in Sections
88. the refined type assumption lstEven nat bool The second rule for 1stEven rule does not supply additional information and does not produce any error The updated context after processing the second block is then A Ao U even nat bool odd nat bool lstEven nat bool Finally for the last block from the inferred type from nat nat is the same as the declared one and type inference ends up with the following context A Ao U even nat gt bool odd nat bool lstEven nat bool from nat nat TOY stores this final context A in order to perform type checking of the different goals proposed by the user in an interactive session As explained in Section 2 13 goals are sequences of conditions Therefore type checking of goals can be performed by following the innermost loop of the type inference algorithm using an empty I environment and with no modification of the context A 233 Appendix F Declarative Semantics The semantics of programs written in a declarative programming language can be explained in terms of logical deduction This so called declarative semantics allows to separate what programs do the logical meaning from how it is done the complex operational execution model In this appendix we present the core ideas of TOY s declarative semantics More technical details can be found in 11 for first order programs and in 13 for the higher order case F 1
89. the right hand side and or the conditions As in lazy functional languages sharing improves efficiency Moreover sharing in 7OY is needed for correctness as shown by the previous example Sharing implements so called call time choice semantics of non deterministic functions Intuitively this semantics means the following given any function call of the form f e en where the actual parameter expressions e may involve non determinism the evaluation proceeds by first computing some possible value v for each es and then invoking f with actual parameters v Note that the values v are not computed eagerly rather the evaluation of the actual parameters e is delayed until needed and the eventually obtained values v are shared A more formal description of call time choice can be found in Appendix F and in 11 From a practical viewpoint JOY users must be aware of call time choice since it affects the set of possible solutions in the case of non deterministic computations For instance given the TOY definitions coin int coin gt O coin gt 1 40 double int gt int double X X X the goal double coin R has two possible solutions namely R O and R 2 These correspond to the two possible call time choices of a value v for coin before invoking double v Sometimes call time choice gives rise to more subtle behaviours as illustrated next Consider the TOY definitions coins int coins gt coin co
90. the textual debugger presented in the previous section The process starts with a computation tree whose root is considered non valid Then the children of the root are examined looking for some non valid child If such child is found the debugging continues examining its corresponding subtree Otherwise all the children are valid and the root of the tree is pointed out as buggy finishing the debugging The next display shows the starting point of the a debugging session using the top down strategy where the user has marked the second node as non valid and the last two nodes as trusted 145 DDT tree xml File Node Tree Select Strategy Information Help xX root fromX gt X sucX _ map times suc z X suc X _ gt L zI_ tail L z _ gt 212 head z _ gt z valid 0 NonValid 1 Unknown 9 TTrusted 0 s Buggy 0 Total 10 See TT Basic Facts Y fromX gt X sucX _ O map times suc z X suc X _ gt L z _ tail L z _ gt Z _ O head z _ gt z O Notice that after each subsequent step the selected subtree has a smaller size and an invalid root until a buggy node is eventually reached As in the top down strategy the divide and query strategy starts with a computation tree whose root is not valid The idea is to choose a node N such that the number of nodes inside and outside of the subtree rooted by N are the same Although such node called the center of the
91. tkSetValue tkShowCoords tkShowErrors tkslabels tkTerminateWish tkUpdate tkVoid writeVar writeVarl writeWish Table D 7 I O Graphic Library Predefined Functions I O File Note that the data type and data constructors needed for these functions are already defined in the plain language predefinitions Tables D 7 D 8 and D 9 show respectively the predefined symbols for functions data types and data constructors for the library I O Graphic Finally tables D 10 D 11 and D 12 show respectively the predefined symbols for functions data types and data constructors for the library Finite Domain Constraints Observe that the library Real Constraints does not introduce new symbols and arithmetic operators from the plain language are otherwise reused for building constraints D 2 Grammar This section describes TOY syntax Terminals are shown enclosed in square boxes like this Curly brackets represent the choice of one among several elements separated by com mas Square brackets enclose optional elements while rounded brackets are used for grouping The postfix operator represents the repetition of tokens of some syntactic category zero or more times while represents the repetition one or more times Syntactic categories of tokens are written in italic letters see lexicon above tkConfItem tkWidget tkConfCollection tkRefType tkCanvasItem tkMenultem tau Table D 8 I
92. tree does not exist in most of the cases the system looks for the node that better approximates the condition Then the user is queried about the validity of the basic fact labeling this node If the node is non valid its subtree will be considered at the next step If it is valid then its subtree is deleted from the tree and debugging continues The process ends when the subtree considered has been reduced to a single non valid node Is easy to observe that as in the top down strategy the number of nodes in the tree T considered is reduced after each step and that nonvalid root T holds and that the strategy will find some buggy node The divide and query requires a number of questions that proportional in average to the logg n where n is the number of nodes of the tree and must usually preferred to the top down strategy In our example after four questions the system finds a buggy node pointing at the second rule of function times as invalid 146 DDT tree xml File Node Tree Select Strategy Information Help x times suc z suc times z suc X oy Buggy Node Found Node times suc z suc X gt z Program rule times 2 Valid 0 Unknown 1 Basic Fact T times z suc X gt z 0 Since these strategies modify the structure of the tree DDT includes options to save and load computation trees see the options of the menu File The files are stored in XML format These options can be
93. 1 Y gt s z Elapsed time O ms more solutions y n d y X gt s z Y gt s s z Elapsed time O ms more solutions y n d y X gt gt z Y gt s s s z Elapsed time O ms more solutions y n d y no Elapsed time O ms Thus even this purely functional program can be used in a functional logic way by allowing variables in the goals and returning several different answers if they exist A 2 2 Infinite Lists inflists toy The following example takes advantage of lazy computations in TOY to represent infinite structures in the same way as in Haskell 156 An infinite list of consecutive integers from int gt int from N N from N 1 The first N elements in a list take int gt A gt A take N take N X Xs if N gt O then X take N 1 Xs else An expression of the form from N represents an infinite list of consecutive numbers starting at number N while take N L returns the first N elements of list L Therefore we can evaluate a purely functional expression of shape Toy gt gt take 3 from 0 0 1 2 Elapsed time O ms showing the first three elements of the infinite list on numbers starting at 0 Thus the infinite list is only evaluated up to the needed point A 2 3 Prime Numbers primes toy In TOY higher order functions are also allowed as Haskell does Therefore typical higher order functions like map fold filter et
94. 1 Peano Numbers peano toy A 1 2 Paths in a Graph paths toy Functional Programming A 2 1 Arithmetic for Peano Numbers arithmetic toy A 2 2 Infinite Lists inflists toy A 2 3 Prime Numbers primes toy A 2 4 Hamming Codes hamming toy A 2 5 Process Network Client Server Interaction clientserver Functional Logic Programming A 3 1 Inserting an Element in a List insert toy A 3 2 The Choice Operator choice toy A 3 3 The Inverse Function inverse toy Programming with Failure A 4 1 Default Rules automata toy A 4 2 A Propositional Tautology Generator tautology toy Programming with Equality and Disequality Constraints A 5 1 The Cardinal of a List cardinal toy Programming with Real Constraints A 6 1 Defining Regions of the Plane regions toy Programming with Finite Domain Constraints A 7 1 A Colouring Problem colour toy A 7 2 Linear Equations eq10 toy and eq20 toy A 2 Functional Programming 00 2000 A 3 Functional Logic Programming AA Programming with Failure o A 5 Programming with Equality and Disequality Constraints A 6 Programming with Real Constraints A 7 Programming with Finite Domain Constraints A 7 3 DNA Sequencing dna toy 2 2 0 eee ee ee eee A 7 4 A Scheduling Problem scheduling toy o A 7 5 A Hardware Design Problem o e e A 7 6 Golomb Rulers An Optimi
95. 2 14 and 2 6 More concretely the precise meaning of a comprehension list is given by the following translation rules e b q if b then e q else where b is a boolean expression or a goal e X lt L q concat map f_x Xs wheref_x X e q e e e As an example consider again the comprehesion list 3We are assuming that the file misc toy containing the function odd has been previously included 139 X X X lt 1 2 3 4 5 6 7 8 9 10 odd X The translation of this comprehension list by applying the translation rules is the following X X X lt 1 2 3 4 5 6 7 8 9 10 odd X concat map fx 1 2 3 4 5 6 7 8 9 10 where fx X X X odd X Since fx i i i odd iJ 1 lt i lt 10 then fx i i i if odd i fx i otherwise Hence X X X lt 1 2 3 4 5 6 7 8 9 10 odd X concat 1 1 3 3 5 5 C 7 7 01 9 9 1 9 25 49 81 Differently to functional programming the conditions occurring in a comprehension list named guards in Haskell may contain variables not generated previously Similarly in a comprehension list e Q e may contain variables not occurring in Q In both cases the non generated variables aree treated as logic variables depending on the computational context they can become bound to some pattern or stay free For instance for generating a list containing 5 pairwise distinct variables w
96. 20 0 64234 X2 O 68550 X1 61944 X4 84391 X3 X2 44247 42253 X4 x X1 21103 X1 55679 65337 X3 27886 X2 92964 81310 X4 77527 X2 X4 45581 31716 279091 88963 X5 76391 X6 O 76132 X2 71860 X3 22770 480923 48224 X1 82817 X7 519878 94198 X2 87234 X3 37498 X4 O 71583 X1 25728 X5 25495 X6 70023 361921 78693 X1 38592 X5 38478 X6 O 94129 X2 43188 X3 82528 X4 69025 labeling Label LD The next goal uses the first fail labeling strategy Toy FD gt equation10 ff L L gt 2 6 0 By 4 9 3 9 4 Elapsed time 32 ms more solutions y n d y no Elapsed time 15 ms X6 X5 70582 X5 97932 X5 X3 X4 44550 X6 96552 X6 67707 73597 68211 X7 33054 X7 X7 X6 98038 X7 X4 38835 X7 X5 78587 X6 X7 X7 Another version considers 20 linear equations with the same number of finite domain variables and related domains include cflpfd toy equation20 labelingType gt int gt bool equation20 Label LD true lt 174 LD X1 X2 X3 X4 X5 X6 X7 domain LD O 10 876370 16105 X1 6704 X3 68610 X6 0 62397 X2 43340 X4 95100 X5 58
97. 3 Elapsed time 15 ms sol 1 more solutions y n d a y no Elapsed time O ms assignment 2 e Type Declaration assignment int int bool e Modes assignment inout inout gt inout e Definition assignment L1 L2 is a function applied over two lists of domain variables with length n where each variable takes a value in 1 which is unique for that list Then it returns true if for all i j 1 n and X L1 Y L2 then X j if and only if Y 7 e Reifiable No e Example The next goal returns true and constrains X Y and Z to be 3 1 and 2 respectively Toy FD gt domain X Y Z 1 3 assignment X Y Z 2 3 D X gt 3 Y gt 1 Z gt 2 D gt 1 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms circuit 1 circuit 2 82 Type Declaration circuit int bool circuit int int bool Modes circuit inout inout circuit inout inout inout Definition circuit L1 and circuit L1 L2 return true if the values in L1 form a Hamiltonian circuit This constraint can be thought of as constraining n nodes in a graph to form a Hamiltonian circuit where the nodes are numbered from 1 to n and the circuit starts in node 1 visits each node and returns to the origin L1 and L2 are lists of FD variables or integers of length n where the t
98. 301 X7 533909 96722 X5 0 51637 X1 67761 X2 95951 X3 3834 X4 59190 X6 15280 X7 915683 34121 X2 33488 X7 O 1671 X1 10763 X3 80609 X4 42532 X5 93520 X6 129768 11119 X2 38875 X4 14413 X5 29234 X6 0 71202 X1 73017 X3 72370 X7 752447 58412 X2 0 8874 X1 73947 X3 H 17147 X4 62335 X5 16005 X6 8632 X7 90614 18810 X3 48219 X4 79785 X7 O 85268 X1 54180 X2 6013 X5 78169 X6 1198280 45086 X1 4578 X3 0 51830 X2 96120 X4 21231 X5 97919 X6 65651 X7 18465 64919 X1 59624 X4 H 75542 X5 47935 X7 O 80460 X2 90840 X3 25145 X6 O 43525 X2 92298 X3 58630 X4 92590 X5 1503588 43277 X1 9372 X6 60227 X7 O 47385 X2 97715 X3 69028 X5 76212 X6 1244857 16835 X1 12640 X4 81102 X7 O 31227 X2 93951 X3 73889 X4 81526 X5 68026 X7 1410723 60301 X1 72702 X6 O 94016 X1 35961 X3 66597 X4 25334 82071 X2 30705 X5 44404 X6 38304 X7 O 84750 X2 21239 X4 81675 X5 277271 67456 X1 51553 X3 99395 X6 H 4254 X7 O 29958 X2 57308
99. 31 2 9 Including Programs 34 2 10 Layout Rule ca ss ca denena du dat ee a a a do 35 2 11 Predicate Definitions o oaoa a ee 35 2 12 Non Deterministic Functions ee 38 2 13 Goals and Computed Answers 0 ee ee 42 2 14 Higher Order Programming xx e era ee Re ee oe 46 2 15 Finite Failure 2 ee 51 2 16 Constraints i 6 eda a og aw BO ee i ee Oe dd 54 2 16 1 Syntactical Equality and Disequality Constraints 2 16 2 Arithmetical Constraints over Real Numbers 3 Constraints over Finite Domains dul Introduction vu psoe ae oaea ee A OR PO a ee ee ee Qld EXCEDEN sos ea Aas Sa PR ee ed a ee ate eo ee eee e 3 1 2 Modes and Bidirectionality 0 20 0000 4 3 1 3 Loading the FD Constraint Library 2 04 3 2 FD Constraints and Functions e 3 2 1 Predefined Data Types 2 2 0 2 2 000002 eee eee 3 2 2 Membership Constraints 2 0 0 2 ee 3 2 3 Enumeration Functions e 3 2 4 Relational Constraints a 3 2 5 Arithmetic Constraint Operators 0 0000022 eae 3 2 6 Arithmetic Constraints 2 20000 eee eee 3 2 7 Combinatorial Constraimts e 3 2 8 Propositional Constraints e 3 2 9 Reflection Functions ee 3 2 10 FD Set Functions a 3 2 11 Statistics Functions 2 2 e 3 3 Introductory Programs 3 3 1 The Length of a List haslength toy
100. 994 T Klove Bounds and construction for for difference triangle sets IEEE Transactions on Information Theory 35 879 886 July 1989 Francisco J L amp 243 pez Fraguas and Jaime S amp 225 nchez Hern amp 225 ndez A proof theoretic approach to failure in functional logic programming Theory Pract Log Program 4 2 41 74 2004 Francisco Javier L amp 243 pez Fraguas and Jaime S amp 225 nchez Hern amp 225 ndez Prov ing failure in functional logic programs In CL 00 Proceedings of the First International Conference on Computational Logic pages 179 193 London UK 2000 Springer Verlag Francisco Javier L amp 243 pez Fraguas and Jaime S amp 225 nchez Hern amp 225 ndez Nar rowing failure in functional logic programming In FLOPS 02 Proceedings of the 6th International Symposium on Functional and Logic Programming pages 212 227 London UK 2002 Springer Verlag Rita Loogen Francisco Javier Lopez Fraguas and Mario Rodriguez Artalejo A demand driven computation strategy for lazy narrowing In PLILP pages 184 200 1993 150 23 F J L pez Fraguas and J S nchez Hern ndez TOY A multiparadigm declarative system 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 In P Narendran and M Rusinowitch editors 10th International Conference on Rewriting Techniques and Applications number 1631 in LNCS pages 244 247 Trento Italy 1999 Springer Verlag Francisco Javi
101. Changes below e wakeoptions See Section Changes below e options See Section Changes below e newOptions See Section Changes below Changes e fd_statistics and fd_statistics have interchanged their role in order to adhere to the convention that the prime indicates that options can be used The type of fd_statistics has changed to statistics gt int e substract in misc toy becomes subtract e wakeoptions becomes wakeOptions e options becomes al1DiffOptions e nevOptions becomes serial0ptions Fixed Bugs e The command type did not work on expressions Fixed e User defined commands as described in section 1 5 5 of User Manual for version 2 2 2 did not work Fixed e sum and scalar_product were not correctly implemented giving rise to type error excep tions Fixed e fd_statistics delivered duplicate solutions Fixed e nocflpfd did not completely unload the library CFLPFD Fixed e The libraries IO File and IO Graphic could not be unloaded Fixed e When first loading the libraries IO File and IO Graphic and depending on the previous state of the system their functions were not available at command prompt until a program were compiled Fixed e The data type ioMode was documented as data ioMode read write append 251 but the actual declaration is data ioMode readMode writeMode appendMode H 3 Version 2 2 2 Launched on March 2006 Enhancements e Dynamic cut optimization It can be activated using the c
102. Elapsed time O ms fd_size 1 88 e Type Declaration fd_size int int e Modes fd size inout inout e Definition fd_size V returns the cardinality of the domain of V e Reifiable Not applied e Example Toy FD gt domain X 0 10 Card fd_size X Card gt 11 X in 0 210 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms fd_set 1 e Type Declaration fd_ set int gt fdset e Modes fd_ set inout inout e Definition fd_set V returns the FD set denoting the internal representation of the current domain of V e Reifiable Not applied e Examples Toy FD gt domain X 0 10 X 5 FDSet fd_set X FDSet gt interval 0 4 interval 6 10 gt X in 0 4 6 10 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms Toy FD gt domain X 0 1 P fd_set P X interval 1 1 X 89 X gt 1 P gt fd_set Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms fd_dom 1 e Type Declaration fddom int fdrange e Modes fd_ dom inout inout e Definition fd_dom V returns a constant range denoting the current domain of V e Reifiable Not applied e Example Toy FD gt domain X 0 10 X 5 Dom fd_dom X Dom gt uni cte 0 4 cte 6 10 X in 0 4 6 10 Elapsed time O
103. For instance an attempt of finding the intersection of two concrete parallel lines fails Toy R gt intersctPoint 1 1 1 1 1 0 no Elapsed time O ms However nonlinear constraints are passive and their satisfiability is not checked For instance an attempt of finding the intersection of two generic parallel lines does not fail but returns a hard to read non linear constraint as answer which is in fact unsatisfiable Toy R gt intersctPoint A B 1 A B 0 P gt _C _D 1 0 _F G A 04 _F 0 0 _D B _E 0 0 _H _C A 0 0 _G _D B 0 0 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms The previous examples use only as arithmetical constraint The system supports also lt lt gt gt The use of some of them is illustrated in Section A 6 1 62 Ak lt abs acos acosh acot acoth asin asinh atan atanh cos cosh cot coth exp ln log max min sin sinh sqrt tan tanh wminus Table 2 3 Real Constraint Operators and Functions ceiling div floor gcd mod round toReal trunc Table 2 4 Real Constraint Operators and Functions unmanaged by the Solver Table 2 3 summarizes the real constraint operators which are sent to the real solver Other arithmetical functions cannot be managed by this solver as shown in Table 2 4 Recall that nonlinear constraints are delayed until they become linear due to variable instatiation
104. Motivation Declarative semantics originated in the field of pure logic programming where programs are given as sets of definite Horn clauses In this setting the logical meaning of a program P can be modelled as the set of atomic facts p ti tn which can be derived from P in the logical calculus HL for Horn Logic consisting of one single inference rule qilti 1 gt timo 1 lt i lt k Pia ss bal IF p ti tn lt qi tis atin timi TEP Geller hey mia is an instance of some clause in P HL is a very simple inference system which reflects the logical reading of a program clause as a universally quantified implication Atomic facts play a key r le here because program clauses behave as definitions of predicates In the case of a multiparadigm declarative language like TOY program clauses are replaced by defining rules for functions which are lazy and possibly non deterministic as we have seen in Chapter 2 Therefore a declarative semantics for TOY must rely on some suitable generalization of atomic facts Following 13 we consider atomic facts of the form ft tn t whose intended meaning is t represents one of the possible approximations of the result returned by a call to the n ary function f provided that t1 t represent finite approximations of f s arguments More precisely in any atomic fact fti tn gt t f FS must be a defined function symbol of arity n and t t must be patt
105. ND and OR For instance the multiplexer depicted in Figure A 5 can be represented by the following pattern orGate andGate iO notGate i2 andGate il i2 This first class citizen higher order pattern can be used for many purposes For instance it can be compared to another pattern or it can be applied to actual values for its inputs in order to compute the circuit output So with the previous pattern the goal Toy FD gt P orGate andGate iO notGate i2 andGate il i2 P true false true 182 Input 0 Input 1 Input 2 Module Module Module ee E Not Gate And Gate Or Gate Module Module Module B1 B1 4 JOP B2 B2 Figure A 4 Basic Modules 10 i0 0 A il aoe it Di i2 gt i2 Symbol Sum of products equivalence Figure A 5 Two Input Multiplexer Circuit is evaluated to true and produces the substitution 0 false The rules that define the behavior can be used to generate circuits which can be restricted to satisfy some conditions If we use the standard arithmetics we could define the following set of rules for computing or limiting the power dissipation power behavior gt int power i0 0 power il 0 power i2 0 power notGate C notGatePower power C power andGate C1 C2 andGatePower power C1 power C2 power orGate C1 C2 orGatePower power C1 powe
106. O H RX RY RY gt RYO H RY RX lt RYO RXO RY RX lt RYO RXO bothIn region gt grid gt dPoint gt bool bothIn Region Grid X Y X RX YH RY isIn Region RX RY isIn Grid X Y labeling X Y We build an isosceles triangles from a given upper vertex RX RYo and a given height H The three vertices are RXo RYo RXo H RYy H RXo H RYo H and the region inside the triangle is enclosed by the lines RY RYp H RY RX RY RXo and RY RX RYy RXo and characterized by the conjuntion of the three linear inequalities 119 RY gt RYy H RY RX lt RY RXo and RY RX lt RYo RXo This explains the real arithmetic constraints in the triangle predicate As an example of goal solving for this program we consider three goals computing the intersec tion of this fixed square grid with three different triangular regions e Toy R FD gt bothIn triangle 2 5 3 0 5 square 4 X Y no Elapsed time O ms 0 5 Figure 4 3 No solutions This goal fails e Toy R FD gt bothIn triangle 2 2 5 1 square 4 X Y X gt 2 Y gt 2 Elapsed time 15 ms sol 1 more solutions y n d a y no Elapsed time O ms 1 Figure 4 4 One solution This goal computes one solution for X Y corresponding to the point 2 2 e Toy R FD gt bothIn triangle 2 2 5 2 square 4 X Y X gt 1 Y gt 1 Elapsed time 16 ms sol 1 more solutions y
107. P F F X until A gt bool gt A gt A gt A gt A until P F takeUntil P iterate F Standard combinators Ah Ah hh const A gt B gt A const K X K id A gt A id X X non deterministic choice A gt A gt A X _ X _ Y Y curry A B gt C gt A gt B gt C curry F A B F A B uncurry A gt B gt C gt A B gt C uncurry F A B FAB fst A B gt A fst X Y X snd A B gt B snd X Y Y fst3 A B C gt A fst3 X Y Z X snd3 A B C gt B snd3 Y X Z X thd3 A B C gt C thd3 Y Z X X subtract real gt real gt real subtract flip even odd int gt bool 202 even X odd not 1cm int lcm X Y X mod 2 even gt int gt int if X 0 Y 0 then 0 else abs X div gcd X Y Y Ahhh head head X _ last last last X _ Y Xs tail tail _ Xs init X X Y Xs init init nub nub nub X Xs length length length _ Xs size size reverse reverse Standard list processing functions hh hh hh hh hh hh A gt A X A gt A X last Y Xs A gt A Xs A gt A Xlinit Y Xs A gt A remove duplicates from list X nub filter X Xs A gt int 0 1 length Xs A gt int length nub A gt A
108. St tkSetValue Display 0 Ch else do Acu lt readVar St writeVar 0 op snd Acu fst Acu C St op int gt string gt int gt int op N N op N N op N N x op N N div Note that the mutable variable is created in the function calculator with an initial value 0 id where id is the identity function This variable is passed as argument to be used by those functions which require to manipulate the state On the other hand we have also used a reference to the display tkRef Display which is also passed as argument in order to allow to modify it The third argument of function button_pressed is the label of the pressed button Finally the execution of the expression gt calculator generates the following window whose behaviour is the expected one a ea PAE EA ganea goH epe 5 6 List Comprehensions TOY in common with some other functional logic languages like Haskell and Curry provides a powerfull list notation called list comprehensions This notation allows to define lists in a compact way describing the properties which must satisfy the elements of a list instead of enumerating its elements Here is an example X X X lt 1 2 3 4 5 6 7 8 9 10 odd X 138 The evaluation of the above comprehension list returns the list 1 9 25 49 81 as result i e it returns the list of squares of odd numbers in the range 1 to 10 Formally a list comprehension
109. TOY A Multiparadigm Declarative Language Version 2 3 Rafael Caballero Jaime S nchez Eds Document Version 1 0 Purificaci n Arenas S nchez Antonio J Fern ndez Leiva Ana Gil Luezas Francisco J L pez Fraguas Mario Rodr guez Artalejo Fernando S enz P rez Universidad Complutense de Madrid December 2006 Contents Preface 6 1 Getting Started 8 1 1 Supported Platforms and System Requirements a aooo 8 1 2 Downloading and Running TOY 2 ee 8 13 First Steps m TOV pr eae ea lk ae ee ee te a e a E 9 1 4 Compiling and Loading Programs 000000 ee eee 10 1b Commands ior s dree hoe BY ete ee aa Se BY et ee 12 LOL Syntax toe Be Soe ea Be ee a ee ee a a a 12 1 5 2 Interaction with the Operating System 2 0200 13 1 5 3 Compiling and Loading Programs 0224 13 1 5 4 Information about Programs 0 0000 eee eee 14 1 5 5 Commands for Constraint Solvers o e e 2 ee 15 1 5 6 Miscellanea sa s rerea naa a ee 16 1 5 7 Defining New Commands aoaaa e 17 2 The Language 18 2 1 Expressions suss por m Bonk a i piia ee ee e a ek A ke ee es 18 22 Types fuses Bk a eee p hak Say PERSE ae K ae Are a 19 2 3 Datatype Definitions aoaaa a a 21 2 4 Predefined Types 23 2 5 Type Synonyms e 2x0 0 e Ve ee RR ee De pa e ee 24 2 6 Function Definitions a 26 2 7 Operators and Sections a 30 2 8 Primitive and Predefined Functions a
110. Y Yr _E _F _F lt 7 0 Yr _F Xr X Y _E _E in inf 7 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms Previous goal matches _F with RZ and _E with Z 4 5 Introductory Programs The directory examples cooperation provides by distribution contains examples of TOY pro grams that make use of FD and R constraints bridges constraints and cooperation between solvers The program title is annotated with the corresponding file name 4 5 1 Intersection of a discrete grid and a continuous region bothIn toy We consider a generic program written in JOY which solves the problem of searching for a 2D point lying in the intersection of a discrete grid and a continuous region 118 RXo RY0 RXo H RY 0 H t Figure 4 1 Discrete grid and a continuous region Figure 4 2 Possible intersections Sizes of square grid and triangular region is parametric Both grids and regions are represented as Boolean functions They can be passed as parameters because our programming framework supports higher order programming features type dPoint int int type cPoint real real type setOf A A gt bool isIn setOf A gt A gt bool isIn Set Element Set Element type grid setOf dPoint square int gt grid square N X Y domain X Y ON type region setOf cPoint triangle cPoint gt real gt region triangle RXO RY
111. a b and d in its three first arguments respectively The output represents the possibilities to construct d from the fragments taken from a and b include cflpfd toy solve int gt int gt int gt int gt int gt int gt bool solve A B D AFIMA BF MB DF MD 176 choose_initial A B D AF BF DF A2 B2 D2 rsm A2 B2 D2 AF BF DF MA MB MD rsm int gt int gt int gt int gt int gt int gt int gt int gt int gt bool rsm J LenA LenB LenD J true rsm A B D LenA LenB LenA Ai MA MB Dk MD LenA lt LenB Dk lt LenB LenA Ai gt Dk choose Ai A A2 choose Dk D D2 NLenA LenA Ai NLenD LenA Dk rsm A2 B D2 NLenA LenB NLenD MA MB MD rsm A B D LenA LenB LenB MA Bj MB DkIMD LenB lt LenA Dk lt LenA LenB Bj gt Dk choose Dk D D2 choose Bj B B2 NLenB LenB Bj NLenD LenB Dk rsm A B2 D2 LenA NLenB NLenD MA MB MD choose_initial int gt int gt int gt int gt int gt int gt int gt int gt int gt bool choose_initial A B D AF BF DF A2 B2 D2 choose AF A A2 choose BF B B2 choose DF D D2 choose int gt int gt int choose X choose Ai AilA2 A2 choose Ai A1 A2 A Ailchoose Ai A2 A For instance one goal for this program could be Toy FD gt solve 3 2 4 5 9 7 8 3 2 3 4 2 2 3 4 L1 L2 L3 L1 gt
112. a defining rule is f I Tp TD Ty gt T f tietan r lt Ci Cm where Di Dp Such a definition is understood to introduce a defined function f FS of arity n For each defining rule the left hand side f ti tn must be linear i e it cannot include repeated variables The formal parameters t must be patterns The right hand side r can be any expression built from variables built in operations data constructors and functions occurring in the program C are conditions and D are local definitions more details about them will be explained below Often a defining rule needs no conditions in which case the symbol lt can be omitted Similarly the reserved word where can be omitted if there are no local definitions For the moment we assume that each condition must have the form e1 lt gt e2 for some lt gt lt gt lt gt es and e gt being expressions Conditions of the form b true can be abbreviated as b Strict equality conditions ey e2 are solved by evaluating the two expressions es and ez to a common finite value represented by a pattern while disequality conditions e ez are solved by evaluating es and ez to conflicting values In the case of expressions e whose evaluation yields an infinite value e g an infinite list a strict equality never holds and the attempt to solve it can lead to a non terminating computation On the other hand lazy evaluation explained below
113. all n gt 0 belong to the declarative semantics of any TOY program which includes the definition of from This example shows that partial patterns are essential to model the semantics of lazy functions whose returned results can be potentially infinite Atomic facts in the sense of pure logic programming can be represented in the form plti tn true By convention this may be abbreviated as p t1 tn For instance the declarative semantics of the Prolog like TOY program presented in Section 2 11 includes among others the atomic fact ancestorOf alice john The declarative semantics we are aiming at is also able to reflect non determinism As an example recall the non deterministic nullary functions coins rcoins int defined in Section 2 12 Their declarative semantics contains the following atomic facts coins gt 0 L coins gt 1 L coins gt 0 0 1 coins gt 0 1 1 coins gt 1 0 1 coins 1 1 1 rcoins gt 0 1 coins gt 0 0 1l rcoins gt 1 L rcoins gt 1 1 L but not rcoins gt 0 1 L neither rcoins gt 1 0 L This reflects the behavioural difference between coins and rcoins which was intended in their respective definitions Recall the informal discussion on call time choice semantics of non deterministic functions in Section 2 12 Formally the declarative semantics of a TOY program P is modelled as the set of all the atomic facts f ty tn t which can be de
114. als with the length of the fragments instead of the fragments themselves Consider the use of two enzymes The first enzyme partitions the DNA sequence into A Ay and the second into B Byz A simultaneous use of the two enzymes also produces a partition into D Dx which corresponds to the combination of the previous two partitions that is Vi Jj Ap As Dy Dy A Vi Aj By B Dy D and conversely Vj Si Dy D A A V Dy D By B where A A denotes the sequence of fragments A to A and denotes syntactic equality Let a b and d resp denote the length of A B and D resp Let a denote the subsequence a1 j 1 lt i lt N and similarly for bj and di The problem is stated as follows given the multisets a a anv b bi by and d di dy construct the sequences ay a1 ay by bi by and dx dj dx The algorithm to solve this problem generates d1 d2 in order and extends the partitions for a and b using the following invariant property which can be obtained from the problem definition above Hither e dy is aligned with a that is dj dy aj aj Or e dy is aligned with bj but not with a for simplicity we assume we never have all three partitions aligned except at the beginning and at the end that is dy dp aj aj The following Boolean function solve 6 takes three input lists representing
115. alse true true false false false true true true false true Outi Dut2 Dut3 Dut4 Outd5 Out Out7 Outs Then to generate a NOR circuit with maxArea maxPower maxCost and maxDelay equal 6 we could submit the following goal domain A P C D O 6 genCir A P C D B S switchingFunction B true false false false false false false false An example of generating a NOR circuit is shown next Toy FD gt F true false false false false false false falsel genCircuit 6 6 6 6 F CIRCUIT F gt true false false false false false false false CIRCUIT gt notGate orGate iO orGate il i2 A in 5 B in 5 C in 5 D in 5 Elapsed time 5312 ms 6 6 6 6 sol 1 more solutions y n d a y F gt true false false false false false false false CIRCUIT gt notGate orGate iO orGate i2 i1 _A in 5 6 _B in 5 6 _C in 5 6 _D in 5 6 Elapsed time 32 ms sol 2 more solutions y n d a y up to 24 solutions A B _C _D A B _C _D The solutions shown above to the problem are included in the distribution A 7 6 Golomb Rulers An Optimization Problem golomb toy A Golomb ruler is a class of undirected graphs that unlike usual rulers measures more discrete lengths than the number of marks it carries Its particularity is that on any given ruler all differences between pairs of mar
116. also used to restore a previous version of the debugging session if the user realizes after some steps that she or he made a mistake when providing information about the validity of the nodes a situation that often arises The theoretical results presented in 4 5 ensure that if debugging starts with an erroneous answer and the user answers the questions correctly then the debugger eventually locates in the program an incorrect function rule as cause of the error Note however that each debugging session locates only one program error Other incorrect program rules can still remain and further debugging session can be required 6 4 Limitations The main limitations of our current debugging tool are e Missing answers Whenever finitely many answers are computed for a certain goal fol lowed by a no more answers indication and the user expects some other answer which is not covered by the computed ones one speaks of missing answers Finitely failing goals with expected solutions are an important subcase of goals with missing answers Declar ative diagnosis of missing answers should detect a function whose set of defining rules in the given program is incomplete Currently our debugger can diagnose wrong answers but not missing answers e Constraints Programs and goals in TOY can use different kinds of constraints as con ditions see sections 2 6 and 2 16 Currently the debugger supports strict equality and 147 disequality constra
117. ample Toy FD gt domain X 4 4 domain Y 0 1 fdset_belongs X Y X gt 0 B gt true Y in0 1 Elapsed time O ms sol 1 more solutions y n d a y X gt 1 B gt true Y in 0 1 Elapsed time O ms sol 2 more solutions y n d a y B gt false X in 4 4 Y in 0 1 Elapsed time O ms sol 3 more solutions y n d a y no Elapsed time O ms 3 2 11 Statistics Functions TOY provides a set of impure functions that allow to to display execution statistics about constrained FD variables and their associated domains during goal solving fd_statistics 1 e Type Declaration fd_statistics statistics int e Modes fd statistics inout gt inout e Definition fd_statistics Key returns a value V if either V unifies with the number of constraints created for Key constraints or V unifies with the number of times that a constraint is resumed and Key resumptions 101 a dis entailment was detected by a constraint and Key entailments a domain was pruned and Key prunings a backtracking was executed because a domain becomes empty and Key backtracks Each value for Key stands for a counter which is zeroed whenever it is accessed by fd_statistics e Reifiable Not applied e Example Toy FD gt domain X Y Z 0 10 X lt Y Y lt Z fd_statistics prunings V gt 12 Z Y Y gt X
118. and fdset_size 1 Also when there is just one variable X it reactivates the search process by dividing its domain by the value fd_min X The search toy file contains several modified example programs to be solved with the labeling strategies search naive 1 and search ff 1 195 Appendix B A Miscellanea of Functions This chapter presents the contents of the two files misc toy and miscfd toy which include use ful functions and type declarations for programming and can be found in the directory include of the distribution B 1 misc toy FILE misc toy A collection of useful functions and type declarations many of them taken from Haskell s prelude type alias for strings type string char infixl 90 nth element selector infixr 90 function composition infixr 50 concatenation of lists infixr 40 non deterministic choice infixr 40 and parallel and sequential conjunction infixr 30 or X parallel and sequential disjunction asx boolean functions and or bool gt bool gt bool not bool gt bool Parallel and false and _ false and false false true and true true 196 Parallel or true or _ true or true true false or false false Sequential and false _ false true X X Sequential or true X true false V X X Negation not true false not false true andL orL orL
119. and myPairOf A are treated as different although they bear equivalent information A very useful example of synonym is the type for character strings defined as follows type string char The previous definition is currently not predefined in TOY It is left to the user s choice to include it in any program if desired In any case JOY supports a special syntax for lists of characters which can be written as a text enclosed in double quotation marks For instance the following are three different representations of the same string Hello World 2H 267421 220 5 YAA 9 et AA A 2 A 7A e 1 1 0 2 W 2 0 Yr 1 d4d 1 M In particular the empty string can be written either as oras Unitary strings consisting of a single character must not be confused with that character For instance a string is not the same as a char As a last example we define a type synonym person along with three auxiliary types type person name address age type name string type address string type age int Note that persons with negative age will not give rise to a type error because person is treated as a shorthand for string string int 25 2 6 Function Definitions A function definition in TOY consists of an optional type declaration and one or more defining rules which are possibly conditional rewrite rules with optional local definitions The schematic form of such
120. ar S occursNot X susp E R S Skel Res Res1 occursNot X R Skel Res Res1 propagate X Cin Cin propagate X T Terms Cin Cout notEqual X T Cin Cout1 propagate X Terms Cout1 Cout continueBind Cin Cin continueBind X Y Res Cin Cout equal X Y Cin Cout1 continueBind Res Cout1 Cout extractCtr X extractCtr Y Terms Ctrs X Ctrs Terms X Y extractCtr Y CY Ctrs X Y CY Ctrs1 CX extractCtr Ctrs X Ctrs1 CX Clauses for Solving Disequalities NotEqualpc notEqual X Y Cin Cout hnf X HX Cin Cout1 hnf Y HY Cout1 Cout2 notEqualHnf HX HY Cout2 Cout notEqualHnf X Y Cin Cout var X notEqualVar X Y Cin Cout notEqualHnf Y X Cin Cout var X notEqualVar X Y Cin Cout 244 notEqualHnf c X1 Xn 0 Y 1 Y mm Cin Cin ifc d notEqualHnf c X1 Xn c Y1 Yn Cin Cout notEqual X Y1 Cin Cout don t know nondeterminism notEqual X Y Cin Cout notEqualVar X Y Cin Cout var Y X Y addCtr X Y Cin Cout1 addCtr Y X Cout1 Cout notEqualVar X Y Cin Cout occursNot X Y ShY Res contNotEqual X Y ShY Res Cin Cout notEqualVar X Y Cin Cin The occur check failed then X Y is valid contNotEqual X _ ShY Cin Cout No residual Y was a cterm l addCtr X ShY Cin Cout contNotEqual X c X1 Xn Cin Cout hnf X d Yi Ym Cin Cout don t know nondeterminism hnf X c Y1 Yn Cin Cout1 n
121. ase that e includes some non deterministic function If this value happens to be infinite the evaluation will continue until the user interrupts it by pressing the Ctrl C key or the available memory is exhausted When computing in this mode it is expected that e includes no logic variables Otherwise the system s behaviour is unpredictable although no error message will occur Three simple examples of TOY computations in evaluation mode are shown below Toy gt gt 3 6 2 12 Elapsed time O ms Toy gt gt 1 2 3 4 1 2 3 4 Elapsed time O ms Toy gt gt 0 1 0 Elapsed time O ms In the third example the expression is non deterministic and the first possible value is computed In order to compute more possible values a user should work in gaal solving mode with a goal of the form 0 1 2 14 Higher Order Programming TOY supports higher order programming in the style of Haskell and other functional languages except that A abstractions are not allowed The syntax for function defining rules see Section 46 2 6 does not preclude the possibility of functions being passed as arguments or returned as results In previous sections we have already met some higher order functions such as twice in Sections 2 1 and 2 2 and inverse in Section 2 12 Some other typical examples are shown below Composition operator infixr 90 B gt C gt A gt B gt A gt C F G X F GX
122. at in some cases the code depends on the signature having different but similar clauses for different constructor or function symbols Whenever we write c of f in the clauses below it indicates that a different clause must be considered for each constructor 242 symbol c DC or function symbol f FS The actual code might be more compact by using metapredicates to recognize and decompose the structure of expressions G 3 1 Clauses for Goal Solving Solve A goal or constraint takes the form e1e ene where lt can be or As answer for a goal the system produces a collection of constraints in solved form Solved forms for equality constraints can be handled as substitutions and the system indeed does it Substitutions are managed by means of Prolog unification and therefore there is no need of explicit management of substitutions in the Prolog code Things are different for the case of disequality constraints which are explicitly managed in the code by means of a disequality constraint store with the form of a list X t1 tn Y 51 5m representing the collection of constraints in solved form X AX t1 X 4 tn Y 1 Y Sm This constraint store must be consistently kept and taken into account throughout the computation This is why many Prolog procedures below have two arguments Cin Cout containing the constraint store as it is before and after the procedure acts These are the top leve
123. ational Conference on Logic Programming pages 1070 1080 Cambridge Massachusetts 1988 The MIT Press J C Gonz lez Moreno Maria Teresa Hortal Gonz lez Francisco Javier L pez Fraguas and Mario Rodr guez Artalejo An approach to declarative programming based on a rewrit ing logic Journal of Logic Programming 40 1 47 87 1999 J C Gonz lez Moreno Programaci n L gica de Orden Superior con Combinadores PhD thesis Universidad Complutense de Madrid July 1994 In Spanish Juan Carlos Gonz lez Moreno Maria Teresa Hortal Gonz lez and Mario Rodr guez Artalejo Polymorphic types in functional logic programming Journal of Functional and Logic Programming 2001 1 2001 M Hanus Curry An Integrated Functional Logic Language Version 0 7 1 June 2000 Available at http www informatik uni kiel de curry report html Michael Hanus A functional logic programming approach to graphical user interfaces Lecture Notes in Computer Science 1753 47 2000 Paul Hudak Simon L Peyton Jones Philip Wadler Brian Boutel Jon Fairbairn Joseph H Fasel Mar a M Guzm n Kevin Hammond John Hughes Thomas Johnsson Richard B Kieburtz Rishiyur S Nikhil Will Partain and John Peterson Report on the programming language haskell a non strict purely functional language SIGPLAN Notices 27 5 R1 R164 1992 J Jaffar and M Maher Constraint logic programming a survey The Journal of Logic Programming 19 20 503 581 1
124. ator are passed as arguments to the tester Since candidates are evaluated lazily they can be rejected without being totally computed and a greater efficiency can be achieved A lazy generate and test version of the permutation sort algorithm is shown below 39 permutationSort real gt real permutationSort Xs checkIsSorted permutation Xs checkIsSorted real gt real checkIsSorted Ys Ys lt isSorted Ys isSorted real gt bool isSorted true isSorted X true isSorted X Y Zs X lt Y isSorted Y Zs permutation 23 A gt A permutation gt permutation X Xs gt insert X permutation Xs insert A gt A gt A insert X gt X insert X Y Ys gt X Y Ys Ylinsert X Ys Here the non deterministic function permutation acts as generator while checkIsSorted is the tester When sorting a list Xs by means of this program the variable Ys acting as formal parameter in the left hand side of the tester gets bound to the different permutations of Xs returned by the generator Therefore it is essential for the correctness of the algorithm that the two occurrences of Ys in the right hand side and in the condition of the defining rule of checkIsSorted share the value passed as actual parameter for Ys More generally the TOY system supports sharing for the values of all variables which occur in the left hand sides of defining rules and have multiple occurrences in
125. b html 2004 Sicstus manual SiCStus Prolog user s manual release 34 8 By the Intelligent Systems Laboratory Swedish Institute of Computer Science 1999 P Van Hentenryck Constraint satisfaction in logic programming The MIT Press Cam bridge MA 1989 Ton Vullinghs Daniel Tuinman and Wolfram Schulte Lightweight GUIs for functional programming In PLILP pages 341 356 1995 151 39 Philip Wadler Why no one uses functional languages SIGPLAN Not 33 8 23 27 1998 40 N F Zhou Channel Routing with Constraint Logic Programming and Delay In 9th In ternational Conference on Industrial Applications of Artificial Intelligence pages 217 231 Gordon and Breach Science Publishers 1996 152 Appendix A Programming Examples In this chapter we show some of the main feaures of TO First we will discuss a few examples that are closest to the logic programming paradigm and functional programming paradigms sections A 1 and A 2 respectively but enriched with some specific functional logic flavour We consider the pure fragment of Prolog and Haskell as representatives of the purely logical and lazy functional programming styles respectively Next we present the use of failure The last three sections present programming with constraints over different domains constructor terms reals and finite domains The distribution provides the directory examples that contains a number of examples of T OY programs included the
126. belongs X a an e Creation of Bridges If X has no bridge then X RX is created with RX new 112 e Propagation Constraint Afterwards the constraints min a1 dn lt RX RX lt maz a1 dn are buildt as mate constraints and submitted to the real solver e Example Toy R FD gt belongs X 1 5 3 X _B _B lt 5 0 _B gt 1 0 X in 1 3 5 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms The same goal without propagation is Toy R FD gt belongs X 1 5 3 X inti S 5 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms t lt t2 analogously lt gt gt t and tg can be either integer constants or else a integer variables e Creation of Bridges If t and or t2 are variables X and or Y and they have no bridges then X RX and or Y RY are created with RX and or RY new e Propagation Constraint Afterwards the constraint t lt tk is buildt as mate con straint and submitted to the real solver where t and or t are either the same constant that t and or ta or else they are the variables RX and or RY e Example Toy R FD gt X RX X lt 5 X RX RX lt 5 0 X in inf 4 Elapsed time O ms sol 1 more solutions y n d a y 113 no Elapsed time O ms Toy R FD gt X RX 5 lt X X RX RX gt 5 0 X in 6 sup Elapsed time O ms sol 1 more solution
127. button butHello text Hello World command puts h writeWish Ch button butExit text Exit command puts e writeWish Ch pack butHello butExit side left runHelloWorld Ch runHelloWorld channel gt io unit runHelloWorld Ch do Str lt readWish Ch if Str e then do putStrLn Goodbye closeWish Ch else do putStrLn Hello World runHelloWorld Ch Note that the buttons have associated the Tcl Tk command puts String The execution of this command writes in the communication channel the string String This string is used to detect 132 which button has been clicked on The auxiliary recursive function runHelloWorld executes the corresponding action in each case depending on the read string Thus when clicking the button Exit the message Goodbye is written in the standard output of TOY and the window is closed and when clicking on the other button writes Hello World and the execution of the program continues in the same way Finally the form of the window generated by the program is the following Hello World A It is important to point out that the four basic operations previously presented allow to program with graphic I O by using purely Tcl Tk commands However the system module io_graphic incorporates also new datatypes and functions avoiding the writing of Tcl Tk commands and facilitating the programming As in the functional logic language Curry 14 graphic I O is specified
128. by means of the datatype tkwidget A whose definition is the following data tkWidget A tkButton channel gt A tkConfItem A A simple press button tkCanvas tkConfItem A For drawing lines circles etc tkCheckButton tkConfItem A A botton that holds a state of either on or of tkEntry tkConfItem A A text entry field tkLabel tkConfItem A A simple label tkListBox tkConfItem A A box containing a list of options tkMessage tkConfItem A A multi line text widget tkMenuButton tkConfItem A A button which when pressed offers a selection of choices tkScale int int tkConfItem A Resizes the widget when moving the slider tkScrollV tkRefType tkConfItem A Adds vertical scrollbars to windows or canvases tkScrollH tkRefType tkConfItem A Adds horizontal scrollbars to windows or canvases tkTextEdit tkConfItem A A sophisticated multi line text widget that can also display other widgets such as buttons tkRow tkConfCollection tkWidget A Y A row of widgets tkCol tkConfCollection tkWidget A A column of widgets In fact the polymorphic type tkWidget A is only used for the instance io unit However we have preferred to use a polymorphic type in sight to future improvements 2In fact the rest of definitions referring to Tcl Tk are an adaptation of an existing graphic I O Curry library to TOY syntax 133 A GUI can be either a simple widget or a collection
129. c can be defined The next example defines the infinite list of prime numbers using an algorithm based on the sieve of Erathostenes It uses the higher order function filter in order to remove numbers that can be divided by any of previous members of the list Function type declarations are not mandatory in TOY and are not included here Observe also the alternative semantics for defining functions e g gt instead of In addition lists use the constructor symbol 2 primes gt sieve from 2 sieve X Xs gt X filter notDiv X sieve Xs notDiv X Y gt mod Y X gt 0 from N gt N from N 1 filter P O gt El filter P X Xs gt if PX then X filter P Xs else filter P Xs 157 take N D gt take N X Xs gt if N gt 0 then X take N 1 Xs else Next goal computes the list of the first ten prime numbers Toy gt gt take 10 primes 2 3 5 7 11 13 17 19 23 29 Elapsed time 16 ms A 2 4 Hamming Codes hamming toy Let H be the smallest subset of N satisfying the following axioms e IEH e Vr x E H amp 22 32 5 EH The problem consists of obtaining the ordered sequence of elements in H that is to say 1 2 3 4 5 6 8 9 10 12 15 Let h denotes the list of elements in H Then the numbers i e codes of Hammings can be obtained by mixing conveniently the following infinite lists map 2 h map 3 h map 5 h By the expression mixing conveniently we
130. constraints provide many benefits like more reversibility reusability and independence of control Something similar happens in the functional logic programming setting Consider for instance the following boolean function to determine if a given point in the plane represented by its two coordinates lies in a given straight line represented by the three coefficients of its equation type point real real type line real real real inLine point gt line gt bool inLine X Y A B C A X Bx Y C 0 We nevertheless discourage the use of nocflpr at least if efficiency is required since this command inhibits the use of constraint solver within TO but is not able to deactivate it for the Sicstus session running underground This implies a strong penalty in efficiency 60 Even without constraints this works fine as a functional program We can evaluate ground expressions like inLine 1 2 1 1 1 orinLine 1 0 1 1 1 to obtain true and false respectively But an attempt of solving a goal with variables results in a runtime error Toy gt inLine 2 Y 1 1 1 RUNTIME ERROR Variables are not allowed in arithmetical operations no Elapsed time O ms instead of obtaining the logical answer Y 3 This makes programs less reversible abstract and reusable For instance to calculate the intersection point of two lines we cannot use the following definition despite its logical soundness intersctPoint L
131. cumulated substitution and constraint store 9 An alternative branch for the the computation at x1 is Goal Substitution Constraint store daxY daa dXX d c Z c b x XA 0 Y d X X d c Z c b X cY d X X d c Z c b X cY Y a X c Z X c b X cY Y faa eZ f 6 2Z lt 6b XwcZ Y a Z Y cZ cb Xu cz a cZ cb XweZ Vf a 2 f Y Z XweZ Y I uA fa Y b Y X cbh Z eb Y a X cb Z b Y a Y b Strict Equality and Disequality Functions As we have discussed before for practical purposes one needs not only the possibility of using the constraints and in conditions of rules but also a two valued equality function for which the system overloades the symbol We also mentioned that can be defined in the language by means of the rules X Y X Y true lt X false lt X Y Dually there is also a two valued function which could be defined as X Y true lt X Y X Y false lt X The system cleans up the final store to eliminate irrelevant disquequalities not involving directly or indirectly the goal variables 59 These definitions of are semantically correct but not very efficient As an example con sider the evaluation of 0 1 99 0 1 99 100 where is the equality function this always can be known by the context With the code above the system tries first the first rule attempting then to solve th
132. current defining rule The three stores have the same structure a set of annotations of the form s T meaning that 7 is the type of the symbol s The symbols s belong to different syntactic categories depending on the store where they occur In A they can be data constructors or defined function symbols from previously processed blocks In I they must be defined function symbols from the current block and in O they must be variables from the current program rule Moreover the type variables occurring in A have an implicit universal quantification For these reason whenever a type assumption s 7 is taken form I the type variables occurring in 7 can be renamed and eventually become bound to other types if this is needed for subsequent type inferences Initially the context A contains the principal types for the constructor symbols of predefined data types such as true false the principal types for predefined functions such as numeric functions div equality and disequality functions and some others as if _ then _ else _ and the principal types for constructor symbols of user defined data types these types are directly obtained from the definition of data types For example for the previous program the initial context has the form A true bool false bool A B B B zero nat suc nat nat where he type variables A and B have an implic
133. d Answers As we said already in Section F 1 CRWL semantics provides no direct information about com puted answers Nevertheless CRWL can be used to specify the logical correctness of compu tations More precisely assume a substitution o of patterns for variables computed by the TOY system as answer for a goal G which consists of strict equality conditions using a program P Correctness of o means that P ForwL Go i e P Forw vo for each strict equality y in G This correctness criterion can be used as a basis to prove soundness and completeness of formally specified goal solving mechanisms see 11 13 The case of goals including other kinds of conditions can be treated analogously with the extensions of CRWL mentioned in Section F 5 237 F 4 Models In the pure logic programming field declarative semantics also includes models A model of a logic program P is any interpretation of the predicate symbols over a certain domain so that all the clauses in P become true when interpreted as universally quantified implications In particular models whose domain is the set of all the data terms see Section 2 1 are called open Herbrand models such models can be represented as sets of atomic facts closed under arbitrary substitutions of data terms for variables A well known result of logic programming theory says that the set Mp p ti tn P Fax p ti tn ie the set of all the atomic facts that can be derived from P in Hor
134. des as a boolean function safe X X is not connected with d there is no path from X to d In order to define this function we would have to use a deterministic functional style changing the representation of graphs and rewriting the full program But using failure the definition is direct safe X fails path X d According to this definition safe c reduces to true while for the rest of nodes it reduces to false Failure may also be used for programming two person finite games in an easy and elegant way following the idea of 10 in logic programming Assume such a game in which players make a move in turn until it is not possible to continue At this stage the player that cannot move losses so the winner is the one that makes the last movement We assume that it is defined the function move State that produces in a non deterministic way a new state from the given State using a legal movement We are interested in a function winMove State that provides a winning movement from State that is a movement that eventually bring us to the victory with independence of the movements of the adversary This is easy to express using failure file nim toy in the examples directory of the distribution winMove State State lt State move State fails winMove State This simple function provides a way for winning the game whenever it is possible The idea is to find a legal movement State such that the other player fai
135. dition and multiplication of natural numbers in Peano notation However the second rule for times is incorrect A user might detect an error symptom when asking for solutions of the following goal intended to compute in Y the second element of the infinite list N X N X 1 Nx X 2 TOY gt head tail map times N from X yes N z Y z more solutions y n d y y yes suc Z z more solutions y n d y d The first computed answer is correct if N is z then the second element of the list will be zero in fact the list will be an infinite list of zeros But the second answer is wrong if N is suc z then the second element of the list should be suc X not z Therefore the user answers d to the question more solutions y n d y and the debugging process starts After some previous work explained briefly in Section 6 5 the debugger displays 143 DDT tree xml DER File Node Tree Select Strategy Information Help X root fromX gt X sucX _ map times suc z X suc X _ gt L zl_ tail L z _ gt z _ head z _ gt z Y Valid 0 X NonValid 1 Unknown 9 T Trusted 0 s Buggy Total 10 The complete tree can be examined by choosing the option Tree Expand Tree The root of the tree corresponds to the initial goal and is not displayed The children nodes correspond to the function calls occurred at the patent The nodes contain basic facts of the form fin
136. e 0 0 4 4 outside rectangle 1 1 3 3 Y gt 3 0 Y lt 4 0 X gt 1 0 X lt 3 0 Elapsed time O ms more solutions y n d y X gt 1 0 X lt 3 0 Y gt 0 0 Y lt i 0 Elapsed time 16 ms more solutions y n d y X gt 3 0 X lt 4 0 Y gt 0 0 Y lt 4 0 Elapsed time O ms more solutions y n d y Y gt 0 0 Y lt 4 0 X gt 0 0 X lt 1 0 Elapsed time O ms more solutions y n d y no Elapsed time O ms 170 The answers are given in terms of arithmetic constraints for the coordinates of the point X Y The union of the areas rectangles given by the four solutions constitute the intersection of the two rectangles 171 A 7 Programming with Finite Domain Constraints In order to compile real constraint programs in TOY the user must first activate the constraint solver over finite domains by means of the command cflpfd In addition it must contain the directive include cflpfd toy as the file cflpfd toy contains the definitions of data types constraints and functions related to finite domains A 7 1 A Colouring Problem colour toy We want to solve the classical map colouring problem Consider the simple map shown in Figure A 2 To solve this problem we have to specify that some countries have different colors by using the constraint all_different L 16 17 18 19 15 20 14 21 12 25 24 23 22 Figure A 2
137. e TF y for all p C THEN f ti tn gt t Z for every pattern t such that Z E r gt t Using this notion of model it can be shown that Mp f ti tn gt t P Forw fti tn gt t i e the set of all the atomic facts that can be derived from P in CRWL is an open Herbrand model of P and even the least open Herbrand model w r t set inclusion This is a nice generalization of the classical results known for pure logic programs Models are a useful tool for various purposes including program analysis verification and de bugging In particular the foundations of TOYV s declarative debugger rely on the comparison between the least open Herbrand model Mp and another open Herbrand model Z which plays the role of the intended model of P The observation of some wrong computed answer g for some goal G indicates that Mp Z T Since Mp is the least open Herbrand model of P it follows 238 that Z is not a model of M Therefore some program rule instance must be false in Z As explained in Chapter 6 the debugger locates such a wrong rogram rule instance by searching a computation tree In fact the computation tree represents the FC inference steps in a CRWL derivation which proves P ForwzL Go All the other CRWL inferences can be ignored by the debugger since they are program independent and cannot cause logical errors See 4 5 for more details F 5 Extensions The presentation of CRWL in Section F 2 and 11 13 is li
138. e action readFile respectively writeFile opens a file and that such a file remains opened as far as the end of the evaluation of the expression in which it is involved On the other hand TOY forbids to open a file previously opened independently of the mode This is the reason why the system closes a file as soon as it detects that a readFile or writeFile operation has finished This remark must be taken into account in the rest of this section 5 4 1 The io file System Module By loading the system module io_file using the command io_file TO provides new functions to handle text files This system module can be unloaded by executing the command noio_file The system module io_file defines operations to read from and write to files represented by values of a new datatype handle which is implementation dependent More precisely io_file provides a dataype ioMode and a collection of I O operations as shown below data ioMode readMode writeMode appendMode openFile path gt ioMode gt io handle closeFile handle gt io unit end_of_file handle gt io bool getCharFile handle gt io char putCharFile handle gt char gt io unit putStrFile handle gt string gt io unit putStrLnFile handle gt string gt io unit getLineFile handle gt io string The execution of the action openFile Name Mode opens the file named Name in the mode estab lished by Mode and yields a handle to manage the
139. e as before Therefore we type type region location int Pieces located in the plane can be represented by a list of pairs piece location Each element in this list can be computed by a function returning the name of the piece its function symbol and its location whose type definition is type piece region gt location location We can define an infinite list generator of such pairs with indeterministic choice of pieces as pieces region gt piece pieces Region Piece Location pieces Region lt choose_piece Piece Piece Region Location pieces Region Note that this function definition embodies lazy evaluation higher order applications and con straint solving choose_piece returns the function symbols for pieces and is defined as 192 choose_piece region gt location choose_piece squarel choose_piece rectanglelx2 The application of a piece to a region returns possible locations pruning the region by constraint solving For domain pruning each piece application drops the values it occupies from the region domain so that no other piece can be placed in the same location For instance the definition of a unit square is squarel region gt location squarel R L lt domain L fd_min R fd_max R inbounds L 1 1 free LR R L The first condition restricts the domain of the location L of the unit square to that of the region Next a condition tests whether t
140. e can execute the following allowed goal Y X lt 1 2 3 4 5 and the computed answer is _C D Es F G As a second example suppose the following function definition p int gt bool p 1 true p 2 true p 3 false Then the allowed goal X p X L has the following three solutions 140 X 1 X 2 X 3 L 1 L 2 L However note that the goal X II X lt 1 2 3 p X has as unique solution L 1 2 This is because we have generated previously the domain of the function p using the comprehension list as a picker of solutions for p To conclude with this section we remark that comprehension lists provide a solution to the problem of programming monadic I O in the context of a search for multiple solutions Since the monadic I O operations are not guaranteed to work correctly within non deterministic com putations the idea is to use a comprehension list to obtain all the desired solutions within one single deterministic computation As a concrte example we show a function that computes all the permutations of a character string writing each one of them in a different line include misc toy show_perms string gt io unit show_perms L putListStr perms L putListStr string gt io unit putListStr An putListStr S Ss putStrLn S gt gt putListStr Ss perms A gt A perms perms L YIYs Y lt L Ys lt perms remove Y L
141. e constraint 0 1 99 0 1 99 100 After 100 decompositions we reach the constraint 100 which fails Then the second rule is tried which requires to redo all the decompositions to reach finally the constraint 100 which succeeds Things are not done in this way in the system Instead the evaluation of an equality proceeds as long as possible without branching between the positive and the negative case In the example above the decompositions are done until the evaluation of 100 is reached Since 100 evaluates to false this is the value of the initial equality Inequality Functions Similarly to the case of and each of the constraint symbols lt lt gt gt is overloaded to represent also a boolean function according to the following definitions X lt Y true lt X lt Y X lt Y false lt X gt Y and similarly for the rest 2 16 2 Arithmetical Constraints over Real Numbers As explained in Section 1 5 5 TOY includes the possibility of activating deactivating resp a linear constraint solver by means of the command cflpr nocflpr resp 1 The interest of arithmetical constraints is known in the logic programming field since the ap pearance of CLP R the first constraint logic programming language In contrast to the very ad hoc Prolog treatment of arithmetic constraints give a clear logical status to real numbers From the point of view of programming
142. e focus on a constraint combinational hardware problem at the logical level but adding constraints about the physical factors the circuit has to meet This problem will show some of the nice features of TOY for specifying issues such as behavior topology and physical factors Our problem can be stated as follows Given a set of gates and modules a switching function and the problem parameters maximum circuit area power dissipation cost and delay dynamic behavior the problem consists of finding possible topologies based on the given gates and modules so that a switching function and constraint physical factors are met In order to have a manageable example we restrict ourselves to the logical gates NOT AND and OR We also consider circuits with three inputs and one output and the physical factors aforementioned We suppose also the following problem parameters Gate Area Power Cost Delay NOT 1 1 1 1 AND 2 2 1 1 OR 2 2 2 2 In the sequel we will introduce the problem by first considering the features TOY offers for specifying logical circuits what are its weaknesses and how they can effectively be solved with the integration of constraints in TOY FD 181 FLP Simple Circuits circuit toy With this example we show the FLP approach that can be followed for specifying the problem stated above We use patterns to provide an intensional representation of functions The alias behavior is used for representing the type bool
143. e of a symbol g in a defining rule of f depends on the blocks of the program if f and g are both in the same block then g plays a definition role while if they belong to different blocks then g has a use role Intuitively in the first case as f and g are mutually dependent the definition of any of them is also part of the definition of the other and as a consequence the type of any of them depends on the type of the other In the second case if the rule of f contains the symbol g but both functions appear in different blocks then the type of g must be fixed before inferring the type for f In this case the occurrence of g corresponds to a use of this function These ideas suggest the way in which the algorithm works The inference is done sequentially block by block from the first to the last one While inferring types for functions of a block any type information about those functions extracted from definitions is added to the type information of those functions in order to refine the information obtained previously When a block is completely processed the types inferred for its functions are fixed for the next blocks in which those functions can appear with a use role The algorithm uses a context A which stores fixed type information obtained from previously processsed blocks an environment IT which stores temporary type information for functions in the current block and an environment O which stores type information for variables in the
144. e syntax of TOY expressions described in Appendix D supports some additional features including numerals if then else conditional expressions and infix operators see Section 2 7 However abstractions are not supported Otherwise TOY syntax is quite similar to Haskell 16 syntax although some predefined symbols and conventions are different Most notably Haskell reserves identi fiers starting with an uppercase letter for types and data constructors while variable identifiers must start with a lowercase letter In 7OY identifiers starting with an uppercase letter are reserved for variables as said before while identifiers for types and data constructors must start with a lowercase letter Two important subclasses of expressions are data terms defined as t X ti tn cti tn ce DC and patterns defined as ti X ti ta cti tm ce DC 0 lt m lt n fti tm f EFS 0 lt m lt n Data terms in TOY correspond to the notion of pattern in typical functional languages such as Haskell Patterns in TOY are more general For instance assume a program with functions times twice FS defined as follows times X Y X Y twice F X F F X Then we can build the pattern twice times 2 which is not a data term neither a pattern in a Haskell like language More generally patterns of the form f t tm J E FS 0 lt m lt _n are not data terms they are called functional patterns or also higher order patterns becau
145. eal num bers For example after loading the library CLP R by typing cflpr a goal as X 1 X 2 was throwing an exception e Fixed an error that occurred when combining disequality and equality constraints of com posed terms For example X 1 1 X 2 2 was throwing an exception H 6 Version 2 1 0 Launched on May 2005 Enhancements e Finite Domain Constraints e Enhanced Declarative Debugging e Multiplatform Support including Windows UNIX and Linux e Executables for Windows 98 and later and SunOS54 H 7 Version 2 0 Launched on February 2002 Undocummented 256 Appendix I Known Bugs e The concurrent execution of several Toy interpreter sessions is not guaranteed to work properly when loading and downloading libraries e O arity tuples are not allowed e You can compile and load a program with FD constraints without loading the library CFLP FD but the correct implementation of primitive FD constraints and functions is not available So before running a CFLP FD program load this library by means of the command cflpfd e If CFLP FD is loaded and a program is compiled and run without the directive include cflpfd toy then the definitions of the FD constraint and functions are lost e When Ctrl C is pressed the stand alone TOY application exits 257
146. ed to Definitional Trees For each function symbol f FS a set of Prolog clauses is generated which is responsible of computing head normal forms for calls to f of the form f e en At the top level the Prolog code for f FS defines a Prolog predicate f with three more arguments than the original function f one for the computed head normal form H two more for the initial and final states Cin Cout of the disequality constraints store Thus the top level clause for f has the shape F E En H Cin Cout The complete code for f called here prolog f is extracted from the definitional tree of f and is defined as prolog f prolog f dt f where the auxiliary function prolog 2 takes a definitional tree and a function symbol possibly different to the function of the definitional tree returning as value a set of Prolog clauses as defined below e prolog f 3 gt case X of c dti Cm dtm 9 In the actual implementation the predicate is named f in order to avoid conflicts between user defined predicates coming from the Prolog translation of a TOY program and built in predicates or predicates belonging to the Prolog translator itself 247 leto X HX in g s H Cin Cout hnf X HX Cin Cout1 g 50 H Cout1 Cout U prolog dty g U prolog dtm 9 where g is a new function symbol e prolog f s gt or dt dtm 9 g 5 H Cin Cout gi
147. efined in the function runHelloWor1d is automated by the built in function runWidget string gt tkWidget io unit gt io unit Thus the evaluation of the expression gt runWidget Hello World win_hello has the same effect as the evaluation of gt hello_world2 runWidget Title Widget runs the widget Widget in a new window with title Title The evaluation of such expression generates an event oriented loop which terminates when closing the window In our example at hand there are two possible events the exit button is pressed or the hello world button is pressed whose associated handlers are the defined functions eventExit and eventHello respectively Note that the function eventExit invokes the built in function tkExit channel gt io unit which closes the window The function eventHello is not recursive because the execution loop is done by the function runWidget In general to program with function runWidget requires to define the layout of the GUI in our example at hand function win_hello and the functions defining the event handlers in our example at hand functions eventExit eventHello The built in functions which facilitate the programming of the event handlers are the following e tkVoid channel gt io unit the void event handler e tkExit channel gt io unit the event handler for closing a window e tkGetValue tkRefType gt channel gt io string gets the value a string of the tex
148. efinitions to obtain the values of locally defined variables Thus the comma in the condition part can be read as conjunction Conjunctions of constraints are also called constraints At the top level a TOY computation consist in solving a goal where goals are also constraints To check the satisfiability of constraints requires a process of constraint solving which is some how independent of narrowing although cooperates with narrowing when constraints involve subexpressions f e1 n Constraint solving may produce one of the following results e A failure if the constraint was unsatisfiable As for the case of failure during narrowing failure of constraint solving is silent and simply forces backtracking Only in case of failure of the whole computation the user is noticed of that e A constraint in solved form i e a constraint in some kind of simplified format ensuring its satisfiability As a matter of fact a single constraint can be transformed into a family a solved forms the original constraint would be equivalent to the disjunction of such family Disjuncts correspond to independent branches of the computation to be tried in sequence in case of bactracking This happens for instance for the goal X 0 1 Y for which a first solution X 1 is obtained If after being asked the user wants to see more solutions a second one Y 0 is shown e A suspended constraint for which the constraint solver is not powerf
149. ejected by the tester The TOY definitions realizing this algorithm are as follows findSol Input gt Solution gt Solution gt bool gt Input gt Solution findSol Generate Test Input gt check Test Generate Input check Solution gt bool gt Solution gt Solution check Test Solution gt Solution lt Test Solution An alternative definition of the function permutationSort as a particular instance of the generic function findSol is now possible permutationSort real gt real permutationSort findSol permutation isSorted where permutation and isSorted are defined as in Section 2 12 The TOY language also supports higher order predicates These are just higher order func tions which return a boolean result TOY users can program higher order predicates using the clausal notation explained in Section 2 11 For instance the following higher order predicate is a relational version of the map function mapRel A gt B gt bool gt A gt B gt bool mapRel R Ml true mapRel R X Xs Y Ys R X Y mapRel Xs Ys In relational logic programming languages such as A Prolog 28 user defined functions are not available Therefore mapRel must be used instead of map In a multiparadigm language there is more room for choice Often functions behave better than predicates if there is some need to compute with potentially infinite structures where lazy evaluation is helpful For ins
150. else evalfd reserved exp fails flip floor gcd getChar getConstraintStore getLine if_then if_then_else ln log max min mod once ord putChar putStr putStrLn readFile readFileContents return round selectWhereVariableXi sin sinh sqrt tan tanh toReal trunc uminus writeFile Table D 3 Plain Language Predefined Functions O Tis m7 7 bool atomicConstraint channel char constraint cTree handle int io T ioMode pVal real varmut Table D 4 Plain Language Predefined Data Types appendMode atomicConstraint channel char constraint cTreeNode cTreeVoid false io pValApp pValBottom pValChar pValNum pValVar readMode stream true varmut writeMode Table D 5 Plain Language Predefined Data Constructors 218 contint openFile closeFile getLineFile contin2 putCharFile end_of_file putstrFile getCharFile putStrLnFil e Table D 6 I O File Library Predefined Functions aux auxl aux2 aux3 aux4 checkWishConsistency closeWish escape_tcl forkWish getNumber getString initSchedule intTostr newVar newVarl newVar2 openWish readVar readWish runWidget runWidgetInit runWidgetPassive setlistelems setmenuelems strToint tk2tcl tkAddCanvas tkcitem tkcitems2tcl tkConf2tcl tkConfCollection2tcl tkConfig tkConfs2handler tkConfs2tcl tkExit tkFocus tkGetValue tkGetVar tkGetVarMsg tkGetVarValue tkLabel2Refname tkmain2tcl tkMenu2handler tkMenu2tcl tkParselnt tkRef2Label tkRef2Wtype tkRefname2Label tks2tcl tkSchedule tkSelectEvent
151. eneral type for an expression the error is not propagated moreover the substitution guarantees that the stores are not be affected 230 BUILD THE INITIAL CONTEXT A FOR I 1 TO N DO LET I BE THE SET OF ANNOTATIONS f Af FOR EACH f Bi FOR EACH DEFINING RULE R l e 4 CD oF f Bi DO LET O BE THE SET OF X Ax FOR EACH X var R LET Tt A T O Ti 01 T 0 16 901 LET Te A T O Te 0e T O Te OB IF THERE EXISTS A M G U 6 OF 7 0 AND Te THEN T 0 T9 00 FOR EACH CONDITION OR LOCAL DEFINITION e 9e IN CD DO LET Te Ar 2 arde T 9 The Obe LET T e A T O Ten Aer 7 0 Ther OB IF THERE EXISTS A M G U 0 OF Ter AND Te THEN T 0 T6 06 ELSE ERROR IN e Oe ELSE ERROR IN RULE R FOR EACH f B DO Ir f HAS A USER DEFINED TYPE Tf THEN Let T f A P 0 74 1 IF THERE EXISTS O SUCH THAT Tf TO THEN De lay aa Ue are ELSE ERROR IN INFERRED DECLARED TYPES FOR f A lt AUTL Table E 1 Inference Algorithm 231 by the error The real implementation as a collateral effect produces an error message with appropriate information for the user Using the function T we can now present a type inference algorithm which starts with the sequence of blocks B1 Bn resulting from the dependency analysis of a program The algorithm is shown in Table E 1 using the notation a c for assignment In order to simplify the presentation we ass
152. ent I10 121 112 all_different I11 121 122 a11_different I11 123 113 all_different 112 123 124 all_different 113 124 125 a11_different 113 114 12 13 14 15 16 17 18 19 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 Toy FD gt colour L Below we show an example of constraint solving with two different solution to this problem L gt dy 232 31 38 1 2 3 ty 2 3 24 La By By Ls Sy By ds Se Se A Elapsed time O ms more solutions y n d y L gt 1 2 3 2 3 1 3 1 2 1 3 1 2 3 2 1 2 3 1 3 2 1 23 31 Elapsed time O ms more solutions y n d y Up to all the possible solutions A 7 2 Linear Equations eq10 toy and eq20 toy This classical problem solves a set of 10 linear equations with seven finite domain variables ranging in the interval 0 10 include cflpfd toy 173 equationi0 labelingType gt int gt bool equationi0 Label LD true lt LD X1 X2 X3 X4 X5 X6 X7 domain LD O 10 O 98527 X1 34588 X2 5872 X3 59422 X5 65159 X7 1547604 30704 X4 29649 X6 O 98957 X2 83634 X3 69966 X4 62038 X5 37164 X6 85413 X7 1823553 93989 X1 900032 10949 X1 77761 X2 67052 X5 0 80197 X3 O 73947 X1 1164380 96253 O 13057 X3 1185471 60152 1394152 669
153. er L pez Fraguas and Jaime S nchez Hern ndez Functional logic program ming with failure A set oriented view In LPAR pages 455 469 2001 Francisco Javier L pez Fraguas and Jaime S nchez Hern ndez Failure and equality in functional logic programming Electr Notes Theor Comput Sci 86 3 2003 M Hanus editor Pakcs 1 4 0 user manual The Portland Aachen Kiel Curry System Available from http www informatik uni kiel de pakcs 2002 K Marriot and P J Stuckey Programming with constraints The MIT Press Cambridge Massachusetts 1998 Gopalan Nadathur and Dale Miller An overview of lambda prolog In ICLP SLP pages 810 827 1988 Lee Naish A declarative debugging scheme Journal of Functional and Logic Programming 1997 3 1997 John K Ousterhout Tcl and the Tk Toolkit Addison Wesley 1994 S P Peyton Jones The Implementation of Functional Programming Languages Prentice Hall Englewood Cliffs N J 1987 J S nchez Hern ndez TOY Un lenguaje l gico funcional con restricciones Research work Universidad Complutense de Madrid 1998 In Spanish J S nchez Hern ndez Implementing constructive failure in functional logic programming In Jornadas de Programaci n y Lenguajes PROLE pages 127 136 2005 J B Shearer Some new optimum golomb rulers IEEE Transactions on Information Theory 36 183 184 January 1990 J B Shearer Golomb ruler table www research ibm com people s shearer grta
154. er as described in the previous sections When the debugger ends the original program P is again loaded into memory The first two points are performed automatically as soon as the user answers d to the question more solutions y n d y and can take some time depending on the size of the original program The last point cor responds to the interaction with the user If she is able to answer all questions correctly an incorrect program rule will be diagnosed Otherwise the debugging process will abort 148 Bibliography 1 Sergio Antoy Rachid Echahed and Michael Hanus A Needed Narrowing Strategy In Conference Record of POPL 94 21ST ACM SIGPLAN SIGACT Symposium on Principles of Programming Languages Portland Oregon pages 268 279 New York NY 1994 N Beldiceanu Global constraints as graph properties on a structured network of elementary constraints of the same type In Rina Dechter editor 6th International Conference on Principles and Practice of Constraint Programming CP 97 number 1894 in LNCS pages 52 66 Singapore 2000 Springer Verlag R Bird Introduction to Functional Programming using Haskell second edition Prentice Hall Series in Computer Science 1998 Rafael Caballero Francisco Javier L amp 243 pez Fraguas and Mario Rodr amp 237 guez Artalejo Theoretical foundations for the declarative debugging of lazy functional logic programs In FLOPS 01 Proceedings of the 5th International
155. eral case Consider a function h of the form ht oe C h tn gt en lt Cn default h tny1 gt enti Cn 1 The construction default is not supported in TOY for the moment but we can translate this function into hX gt hX h X enw1 lt fails h X true Cny1 Pt gt 1 C htn gt en C Notice that with this translation the default rule covers the case of a failure of the previous rules even in the case that failure does not come from pattern matching Default rules can be usefull a variety of situations As an example we consider the case of finite automata A finite automata can be defined as a 5 tuple of the form M K s F 6 where K is a set of states X is an alphabet s is the initial state F C K is the set of final states and 6 K x Y K is the transiction function In order to represent automatas in a program we can assume some simplifications the states are integer values X is the standard set of characters a word is a string list of characters Then we can define in TOY type state int type symbol char type word string type automata state gt symbol gt state delta function state initial state state final states Now we can define a generalized transiction function deltaGen to process words by applying 6 repeteadly until consume the input symbols deltaGen automata gt state gt word gt state deltaGen D I Fs Q TJ Q deltaGen D I Fs
156. erations listToStree list elt gt stree elt listToStree nil empty listToStree N L insert listToStree L N inorder_st stree elt gt list elt inorder_st empty nil inorder_st T inorder_st left T root T inorder_st right T lt T empty Note There is no way to reuse the inorder traversal from bintree_traversals because parameter types do not match main operation stree_sort L inorder_st listToStree L stree_sort only works for lists with no repetitions because all elements in a search tree are different DICTIONARY AS SEARCH TREE module dictionary parameters type key type contents kle keq key gt key gt bool default contents combine contents gt contents gt contents parbody ple peq key contents gt key contents gt bool ple k1 c1 k2 c2 kle ki k2 peq k1 c1 k2 c2 keq ki k2 imports searchtree type elt to key contents op le to ple op eq to peq renaming type stree key contents to dict key contents 213 exporting types dict key contents ops empty exports find dict key contents gt key gt bool insertcont dict key contents gt key gt contents gt dict key contents deletekey dict key contents gt key gt dict key contents lookup dict key contents gt key gt contents body find D K is_in D K default insertcont D K C if C default then insert D K C el
157. erns with abstract syntax 234 t L X Tte cti tm cE DC 0 sin lt a fti tm J EFS 0 lt m lt n This syntax is almost the same as the one already introduced in Section 2 1 except that the special symbol 1 read bottom is now allowed to occur in patterns The symbol L represents an undefined value A pattern t is called total if there is no occurrence of L in t and partial otherwise Partial patterns can be understood as a representation of partially known values where the occurrences of 1 stand for the unknown parts Therefore the result of replacing some or all occurrences of L in a given pattern is a more defined pattern More precisely the notation t E 1 read t approximates t or t is more defined than t indicates a partial order between patterns which holds iff t can be obtained from t by replacing some or all occurrences of by other patterns This partial order is called the semantic ordering between patterns For instance using the list constructor and integer constants viewed as nullary constructors we can build the infinite list of patterns which is increasing w r t E LOC O 1LC O 1 1 6 O0 1 2 1C The patterns in this sequence represent more and more defined approximations of the infinite list of all non negative integers which is the expected result of the function call from O re member the definition of from given in Section 2 6 Therefore the atomic facts from 0 gt O 1 n 1 for
158. ever if we enable propagation with the command prop then is possible to obtain a solution This goal returns ten answers only two are shown Toy R FD gt CR 9 D1 distribution D1 D2 D3 CDi CD2 CD3 CD Ri R2 R3 CR1 CR2 CR3 gt 0 D2 gt 9 D3 gt 0 CD1 gt 3 CD2 gt 11 CD3 gt 0 CD gt 14 Ri gt 0 R2 gt 0 R3 gt 0 CR1 gt 0 CR2 gt 2 CR3 gt 3 CR gt 5 C gt 17 999999999999996 Elapsed time 16 ms sol 1 more solutions y n d a y D1 gt 9 D2 gt 0 D3 gt 0 CD1 gt 12 123 CD2 gt 2 CD3 gt 0 CD gt 14 Ri gt 0 R2 gt 0 R3 gt 0 CR1 gt 0 CR2 gt 2 CR3 gt 3 CR gt 5 C gt 17 999999999999996 Elapsed time O ms sol 2 more solutions y n d a y n 124 Chapter 5 Input Output TOY provides a monadic I O approach similar to that used in the purely functional language Haskell 16 3 To this end I O operations can only be used in deterministic computations I O actions are expected to transform the outside world and to yield a value of some type A upon termination Therefore they are represented as values of the special type io A which in fact can be understood as a type synonym data io A world gt A world The type world is as an abstract dataype whose representation is implementation dependent Therefore the outer world is not accessible directly and only I O operations can modify
159. ferent kinds of trees can be represented by means of suitable recursive datatypes For instance binary trees storing information of type A at their leaves can be defined as follows data leafTree A leaf A node leafTree A leafTree A 22 Mutually recursive datatype definitions are also possible They can be presented in any textual order The mutually recursive types even and odd defined below correspond to even and odd natural numbers data even evenZero evenSuc odd data odd oddSuc even Note that oddSuc evenZero odd suc zero nat 1 int are treated as different values belonging to different types in JOY More generally different datatypes are always disjoint and different from predefined types 2 4 Predefined Types Predefined types in TOY include e bool defined as data bool true false e int the type of single precision integers e real the type of single precision floating point numbers e char the type of characters which must be written by enclosing them in single quotes like e g 2a Q 9 or Some values of this type are control characters rather than visible signs These are written in a special way as follows Toy character meaning AV backslash JAS quote ES double quote a new line ea carriage return eg horizontal tabulator a vertical tabulator E form feed Na alarm b backspace Pod delete e escape e A the recursive datatype of
160. ferred one then the declared type is plced in I and the system emits a warning If the declared type is not an instance of the inferred one then the system signals an error pointing to the inconsistency between the declared and inferred types Finally before processing the next block the algorithm updates the context A by adding all the type annotations in I to it At the end the context A contains the principal types inferred for all the functions occurring in the program or instances of them if the user has provieded some less general type declarations for some functions Now let us see how the full process works in the example shown in Section E 1 We had the three blocks even odd lstEven an from and the initial context was A Ao true bool false bool A B B gt B zero nat suc nat nat For processing the first block we initially build the environment T even C odd D Then we process the four program rules for even and odd in their textual order In fact the order chosen for processing the program rules within a fixed block is not relevant For the rule even zero true we consider O The call T even A T 0 performs two recursive calls T even A T O that produces the pair C and T zero A T O that returns nat Then we unify C with nat E this type is annotated in I as the type of even and the first call to T for the expression even zero retu
161. ffc extends the option ff by selecting the variable involved in the higher number of constraints 2 The second group controls the value ordering that is to say the order in which values are chosen for assignment For instance from the minimum to the maximum enum by selecting the minimum or maximum step or by dividing the domain in two choices by the mid point bisect Also the domain of a variable can be explored in ascending order up or in descending order down 3 The third group demands to find all the solutions all or only one solution to maximize resp minimize the domain of a variable X in L toMinimize X resp toMaximize X 4 The fourth group controls the number K of assumptions choices made during the search assumptions K e Reifiable Not applied e Example 75 The next goal looks via backtracking for assignments to all variables in the list L and follows a first fail strategy Toy FD gt L X Y domain L 1 2 labeling ff L L gt 1 1 X gt 1 Y gt 1 Elapsed time 16 ms sol 1 more solutions y n d a y L gt 1 2 X gt 1 Y gt 2 Elapsed time O ms sol 2 more solutions y n d a y L gt 2 1 X gt 2 Y gt 1 Elapsed time O ms sol 3 more solutions y n d a y L gt 2 2 X gt 2 Y gt 2 Elapsed time O ms sol 4 more solutions y n d a y no Elapsed time O ms indomain 1 e Type Declaration indomain
162. for obtaining interpretations in a non deterministic way bval true bval false inter bval bval bval If we evaluate eval imples conj p q r inter we will obtain true and false what means that this formula is a contingency The easier test is that for contradictions that can be programmed as isContradiction F fails success eval F inter This rule is read as a formula is a contradiction if the evaluation function does not success over any interpretation The other tests are easy to define using this one isTautology F isContradiction neg F isContingency F and not isContradiction F not isTautology F isSatisfiable F not isContradiction F If we evaluate isSatisfiable implies p conj q neg p we get true We can program the generation of formulas that satisfy a given test Moreover we can introduce the concept of complexity of a formula in order to obtain more interesting answers Such a complexity is defined as the number of conectives that they have we use z and s for representing natural numbers and the usual function add complexity p z complexity q z complexity r z 166 complexity neg A s complexity A complexity conj A B s add complexity A complexity B complexity disy A B s add complexity A complexity B complexity implies A B s add complexity A complexity B complexity iff A B s add complexity A complexity B With this program we ca
163. for the variables involved in the cost function Toy R gt X Y Z X gt 0 X lt 2 Y gt 0 Y lt 2 X Y minimize Z Y gt X Z gt 0 I gt 0 X lt 2 0 X gt 0 0 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms bb_minimize real gt real gt real The application bb_minimize X Is returns the minimum for X in the context of the con straints in the real constraint store assuming that the variables in the list Is can only take integral values This allows the evaluation of mixed integer linear problems X is demanded to be in head normal form and Is in normal form The evaluation of this application raises an exception if unboundedness is guessed because either the problem is actually unbounded or boundness cannot be detected because of suspended non linear constraints A value is considered integral with an error of 0 001 Strict bounds on the decision variables are honored but strict inequalities and disequalities are not handled For example Toy R gt X gt Y Z Y gt 1 Z gt 1 bb_minimize X Y Z X gt 4 Y gt 2 Z gt 2 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms 64 Note that this function only generates one particular solution in contrast to both minimize and maximize which deliver a general solution Consider for instance the same problem presented to illustrate the function minimize but adding i
164. g to the solution to the OGR with a marks in S i e Sa 01 0a feeds the o queens solver and the first solution to the o queens problem is computed For example the goal shown above for N 2 first calculates the solutions for the OGR with 4 marks i e 0 1 4 6 and 5 marks i e 0 1 4 9 11 and feeds the queens solver with each mark returning the first solution for 0 1 4 6 0 1 4 9 and 11 queens Toy FD gt map map queens ff map golomb requests 2 L gt O 1 1 2 4 1 3 I 2 4 6 1 3 5 1 fl 1 1 2 4 1 3 J 1 3 6 8 2 4 9 7 5 1 1 3 5 7 9 11 2 4 6 8 10 gt Elapsed time 187 ms more solutions y n d y n This example illustrates how easy and natural may be the combination of different problems in TOY without adding extra code A Tiling Problem tiling toy This example addresses the problem of tiling a given rectangular region with a set of available pieces The simplest piece is a unit square 1 x 1 Less simple pieces can be seen as composed of unit squares For instance a 1 x 2 rectangle can be seen as two stacked unit squares 4X x Y means a rectangle of X horizontal length units by Y vertical length units 191 Client Server 4 fo 4 5678 A 5 6 7 8 yor Na Process requests NY answers NM requests OGR Solution for e OM 0 Queens solver 1
165. h element of L1 resp L2 is the successor resp predecessor of 7 in the graph Reifiable No Example Toy FD gt domain X Y Z 1 3 circuit X Y Z circuit X Y Z X in 2 3 Y in 1 3 Z in 1 2 gt Elapsed time 16 ms sol 1 more solutions y n d a y no Elapsed time O ms count 4 Type Declaration count int int int gt int gt bool int gt bool Modes count in inout inout inout inout Definition count V L Op Y returns true if the number of elements of L that are equal in the sense of FD constraint equality to V is N and also N is related with Y via the relational constraint operator Op i e N Op Y holds Reifiable No Example The next goal returns true and constrains X to be 1 as the number of elements in L that are equal to 1 is imposed to be exactly 2 83 Toy FD gt L X 1 2 domain X 1 2 count 1 L 2 L gt 1 1 2 X gt 1 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms element 3 e Type Declaration element int int int bool e Modes element inout inout inout inout e Definition element I L X returns true if X is the I th element in the list L in the sense of FD I X and the elements of L are integers or domain variables e Reifiable No e Example Toy FD gt L X Y Z domain L 1 10 element 2 L 7
166. h empty z depth tree L N R s mx depth L depth R BINARY TREE TRAVERSALS module bintree_traversals extends bintree imports list exporting all exports leaves bintree A gt list A preorder bintree A gt list A inorder bintree A gt list A postorder bintree A gt list A body leaves empty nil leaves tree empty N empty N nil leaves tree L N R leaves L leaves R leaves L leaves R nil preorder empty nil preorder tree L N R N preorder L preorder R inorder empty nil inorder tree L N R inorder L N inorder R postorder empty nil postorder tree L N R postorder L postorder R N nil Y SEARCH TREES 210 module searchtree parameters type elt le elt gt elt gt bool eq elt gt elt gt bool imports bintree renaming type bintree elt to stree elt exporting types stree elt ops empty root left right exports insert stree elt gt elt gt stree elt delete stree elt gt elt gt stree elt is_in stree elt gt elt gt bool body local auxiliary operations mint and maxt are not defined on the empty tree mint stree elt gt elt mint tree empty N _ N mint tree L _ _ mint L lt L empty maxt stree elt gt elt maxt tree _ N empty N maxt tree _ _ R maxt R lt R empty is_stree is not used in the following but may be useful i
167. hat can be stored in data structures passed as parameters to other functions and also returned as results 2 5 Type Synonyms Type synonyms also called type alias allow to declare a new identifier as shorthand for a more complex type This facility helps to write more concise and readable programs Definitions of type synonyms are introduced by the keyword type and have the following schematic syntax type vA rT where y is the identifier chosen as alias A is a sequence of different type variables acting as formal type parameters and 7 is a type built from the type variables A built in types and user defined type constructors The effect of a type definition like this is to declare y A as an alias of 7 In fact type syn onyms work like parametric user defined macros that are eliminated at compile time Therefore definitions of type synonyms cannot be recursive As long as this restriction is respected the definition of a type synonym may depend on other type synonyms As a simple example we can define a type alias for representing coordinates as numbers and points of the plane as pairs of coordinates 24 type x coordinate real type y coordinate real type point x coordinate y coordinate Another example involving a type parameter is the definition type myPairOf A A A In contrast to the datatype pairOf A shown in Section 2 3 this definition does not introduce data constructors Values of types pairOf A
168. he following First if you want to load two different programs you have to include one inside the other via the include statement see Section 2 9 or pasting the contents of one file to the other And second if you load any system library the user program definitions are lost so you have to reload the user program If you are interested in trying more examples of TOY programs look in the directory examples and read Appendix A pg 153 Chapter 2 pg 18 explains in detail all the components that can occur in a TOY program From the previous discussion it is easy to notice that at the TOY prompt you can type not only goals but also commands line q compile etc which always start with a symbol Next section explains TOY commands 1 5 Commands 1 5 1 Syntax TOY provides an easy command interpreter for manipulating editing compiling loading etc programs at the system prompt Commands in JOY must be preceded by the special symbol Type h for an on line reference of the available commands Arguments of commands when used must be enclosed between parentheses both and and there can not be any blank between the name of the command and the symbol As an example the following commands are recognized by the system compile my_program compile my_program load one_of_my_programs system cd cd cd home local bin q help but the following are not valid commands 12 com
169. he set of these datatypes Table 3 1 Predefined Datatypes for FD Constraints data labelingType ff ffc leftmost mini maxi step enum bisect up down each toMinimize int toMaximize int assumptions int data reasoning value domains range data allDiffOptions on reasoning complete bool data typeprecedence d int int liftedInt data liftedInt superior lift int data serial0ptions precedences typeprecedence path consistency bool static_sets bool edge finder bool decomposition bool data range cte int int uni range range inter range range compl range data fdinterval interval int int type fdset fdinterval data statistics resumptions entailments prunings backtracks constraints In the following we describe all the FD constraints functions and operators currently supported by TOY see Table 3 2 as well as the set of impure FD functions see Table 3 3 in the sense that they depend on the program state Despite they are useful in several applications like defining search strategies the programmer should be aware of its impure functional behaviour 3 2 2 Membership Constraints Membership constraints restrict the values that a variable can be assigned to There are several such constraints domain 3 e Type Declaration 68 Table 3 2 The Predefined Set of FD Constraints Functions and Operators MEMBERSHIP CONSTRAINTS
170. he size of the gate selected by the operational mechanism For instance the circuit area domain is reduced in a number of notGateArea when the rule for notGate has been selected For domain reduction we use the reflection functions fd_min and fd_max This approach allows us to submit the following goal domain Area O maxArea genCir Area Power Cost Delay Circuit which initially sets the possible range of area between 0 and the problem parameter area ex pressed by the function maxArea and then generates a Circuit Recall that testing is performed during search space exploration so that termination is ensured because the add operation is monotonic The mechanism which allows this test when generating is the set of propaga tors which are concurrent processes that are triggered whenever a domain variable is changed pruned The state variable delay is more involved since one cannot simply add the delay of each function at each generation step The delay of a circuit is related to the maximum number of levels an input signal has to traverse until it reaches the output This is to say that we cannot use a single domain variable for describing the delay Therefore considering a module with several inputs we must compute the delay at its output by computing the maximum delays 185 from its inputs and adding the module delay So we use new fresh variables for the inputs of a module being generated and assign the maximum delay to
171. he unit square located at L is not out of bounds by means of constraints Then if there is room for the unit square tested by the function free it is allocated by the disequality constraint removing the location L from the domain of R The inbounds function is implemented as follows inbounds location gt int gt int gt bool inbounds L X Y true lt L mod spaceX X lt spaceX 2X limit L spaceX Y lt spaceY spaceX Y limit where spaceX and spaceY are problem parameters for imposing the horizontal and vertical available space free is implemented via the predefined FD reflection function fdset_belongs L R see Section 3 2 9 Given the complete program we can submit goals as Toy FD gt domain R O 15 pieces R L L gt squarel 0 squarel 1 squarel 2 square1 4 square1 5 squarel 6 square1 8 square1 9 square1 10 R in 3 7 11 15 Elapsed time O ms which fills the region R with unit squares Note that labeling is not needed since fdset_belongs bounds its argument whenever it is not bound We can also submit the following goal which tests whether a region can be filled with at least some pieces Toy FD gt domain R O 15 pieces R rectangle2x1 L1 rectangle1x2 L2 square2 L3 P L1 gt 0 L2 gt 2 L3 gt 4 P gt squarei 10 R in 1SH 17H9 11 15 Elapsed time 15 ms 193 Note that we can request
172. ic otherwise Moreover a datatype 6 is called recursive whenever itself is involved in the type of the arguments of at least one of the data constructors declared in 6 s definition To illustrate the possibilities of datatype definitions we present a series of typical examples The simplest datatypes are enumerated types whose definition declares finitely many constant constructors For instance the datatype of boolean values is predefined as data bool false true and the following enumerated type represents the days of the week data weekDay monday tuesday wednesday thursday friday saturday sunday Next we show a polymorphic datatype with one parameter and a single data constructor whose values bear the same information as pairs of type A A Nevertheless TOY treats the two types as different data pairOf A pair A A The next example is a datatype with two data constructors which represents the disjoint union of the types given as parameters data either A B left A right B Another useful datatype is maybe A which behaves as the disjoint union of the type A given as parameter with a special value nothing which can be used as an error indication It can be defined as follows data maybe A nothing just A Finally we show some examples of recursive datatype definitions Type nat represents Peano natural numbers built from a constant zero and a unary constructor suc data nat zero suc nat Dif
173. icate that the user detects that the answer is incorrect which obviously is not the case and we want to start the debugger The debugger is discussed in detail in Chapter 6 pg 142 It is also possible to directly evaluate narrow 22 an expression by preceding the expression by the symbol gt For example the evaluation of the following goal Toy gt gt 3 5 displays the result 8 To quit TOY at any moment simply type Toy gt q 1 4 Compiling and Loading Programs TOY programs can be written with any text editor The default extension of source program files in TOY is toy and the system will associate this extension to every file name if there is not another explicit extension Nevertheless any explicit extension is allowed Let us try to compile and run a simple program 1 Create a new text file with any text editor Let us assume that the file is saved with name insert toy in the folder examples which you can find in the TOY distribution of course any other name and place is also allowed 2 Using the text editor write the following short program insert A gt A gt A insert X X insert X Y Ys X Y Ys insert X Y Ys Y insert X Ys The code of the program consists of a single function insert The first line is the type declaration of the function which is not compulsory and the three next lines are the rules defining the function Types and functions are explained in Secti
174. if N 0 then Xs else drop N Xs drop N H drop N X Xs drop N 1 Xs Building an infinite list of consecutive integers from int gt int from N N from N 1 In these examples we have used the infix operators and and as function symbols See Section 2 7 for more information about infix operators The definitions of take and drop also use the if then else notation Conditional expressions of the form if b then el else e2 are syntactic sugar for if then else b el e2 where the if then else function is predefined as follows if then else bool gt A gt A gt A if then else true X Y X if then else false X Y Y 28 The use of local definitions is illustrated by the following function roots intended to compute the real roots of a quadratic equation Ax Bx C 0 with real coefficients The definition of roots uses some predefined functions explained in Section 2 8 type coeff real type root real roots coeff gt coeff gt coeff gt root root roots ABC B D E B D E lt E gt 0 where D sqrt B B 4 A C E 2 A As explained in Section 2 2 TOY uses a type inference algorithm at compile time to infer most general types for functions on the basis of the function and the datatype definitions occurring in the program see Appendix E For the purposes of type inference TOY assumes the following types for the operators involved in conditions
175. ike blank spaces 2 11 Predicate Definitions Predicates in TOY are viewed as a particular kind of functions with type 71 gt gt Tn gt bool As a syntactic facility TOY allows to use clauses as a shorthand for defining rules whose 35 right hand side is true This allows to write Prolog like predicate definitions according to the following scheme p o Ty T gt gt Tn gt bool pipet t Ci Cm where Di Dp Here each clause abbreviates a defining rule of the form p ti tn true lt Cy Cm where Dj Dp When using clausal notation the conditions correspond to the body of a clause A clause body cannot be empty in TOY but it can be simply true The following is a simple example of Prolog like programming in TOY Type alias for persons type person string fatherOf predicate father0f X Y holds if Y is father of X fatherOf person person gt bool fatherOf peter john true fatherOf paul john true fatherOf sally john true fatherOf bob peter true fatherOf lisa peter true fatherOf alan paul true fatherOf dolly paul true fatherOf jim tom true fatherOf alice tom true motherOf predicate mother0f X Y holds if Y is mother of X motherOf person person gt bool motherOf peter mary true motherOf paul mary true mother0f sally mary true mother0f bob mol1y true mothe
176. ile toy amp In this case the name of the command is edit it uses one argument File and the effect will be to edit the corresponding file with extension toy 17 Chapter 2 The Language A TOY program is a collection of definitions of various entities including types functions predicates and operators Once a program has been successfully compiled users can interact with the TOY system by proposing goals TOY computations solve goals and display computed answers which can include the result of a functional reduction and or a constraint In particular answer constraints can represent bindings for logic variables as in answers computed by a Prolog system The different sections of this chapter explain the features available in TOY for writing programs and solving goals 2 1 Expressions As every programming language TOY uses expressions built from operation symbols and vari ables Following Prolog conventions variables in TOY are represented by identifiers starting with an uppercase letter Following the conventions adopted by Haskell and other functional languages operation symbols are classified into two disjoint sets data constructors correspond ing to so called functors in Prolog and defined functions TOY uses identifiers starting with a lowercase letter as well as some special symbols both for data constructors and for defined functions Data constructors are easily recognized because they are either predefined
177. imes Sl A a 2 xX Increment Reset stop In order to increment the counter we have used a reference tkRef Val which allows to modify the display by using Val The function tkUpdate has been used to increment the display On the other hand the action associated to button Reset puts 0 in the display by using the built in function tkSetValue Note that the event handler of the button Increment function incrText does not require extra information because all that it needs is contained in the proper GUI but in general the event handlers are more complicated and it is usually useful to use mutable variables 16 38 in order to store states 136 5 5 1 Mutable Variables TOY incorporates the possibility of using mutable variables The system module io_graphic defines operations to manipulate the State Reader monad by means of a new datatype varmut which is implementation dependent The built in functions associated to mutable variables are the following e newVar A gt io varmut A newVar V creates a mutable variable with an initial value V e readVar varmut A gt io A readVar Mut returns the value of the mutable variable Mut e writeVar A gt varmut A gt io unit writeVar V Mut writes a new value V in the mutable variable Mut As an example here we have a TOY program which implements a calculator In the associated code we have used a mutable variable consisting of a pair whe
178. ingType gt bool smm S E N D M 0 R Y Label true lt domain S E N D M 0 R Y 0 9 S 0 M gt 0 all_different S E N D M 0 R Y sum S E N D M O R Y labeling Label S E N D M 0 R Y sum int gt bool sum S E N D M O R Y true lt 1000 S 100 E 10 N D 1000 M 100 O 10 fx R E 10000 M 1000 O 100 N 10 E Y This code is included in the file smm toy provided with the distribution After compiling and loading it see Section 1 4 we can solve goals as Toy FD gt smm L ff L gt 9 5 6 7 1 0 8 2 gt Elapsed time 20 ms sol 1 more solutions y n d a y no Elapsed time O ms 104 3 3 3 N Queens queens toy Here we present a JOY solution for the classical problem of the N Queens problem place N queens in a chessboard in such a way that no queen attacks each other Observe the use of the directive include to make use of the function hasLength 2 Note also that it is not needed to include the FD library since haslength toy loads it already include cflpfd toy include miscfd toy queens int gt int gt labelingType gt bool queens N L Label true lt length L N domain L i N constrain_all L labeling Label L constrain_all int gt bool constrain_all true constrain_all X Xs true lt constrain_between X Xs 1 constrain_all Xs constrain_between int gt int gt i
179. ins repeat A gt A repeat X Xlrepeat X rcoins int rcoins gt repeat coin Due to call time choice semantics coins computes an infinite list of integers where each element is chosen non deterministically as O or 1 independently of the choice for the other elements There are uncountably many such lists On the other hand rcoins computes an infinite list consisting of repeated occurrences of the same integer value v which is non deterministically chosen as 0 or 1 This behaviour is also consistent with call time choice semantics Now there are only two possibilities for the resulting list Strict equality conditions and disequality conditions must be properly understood w r t non determinism In order to solve e e2 the TOY system tries to compute some common finite value for e and ez On the other hand e1 ez is solved by computing some possible values of e and eg which are in conflict to each other For instance e coin coin can be obviously solved e coin double coin can be solved due to the common value 0 of both sides e coin coin can also be solved due to the possibility to compute the value O for one side and the conflicting value 1 for the other side In a similar way eventual non determinism must be taken into account when computing with disequality and inequality conditions All the examples shown in this section up to now achieve non determinism by means of over lapping left hand sides
180. ints and constraints over real numbers but not programs including fi nite domain constraints e Non terminating goals Generally declarative debuggers work only after some completed computation whose outcome is found incorrect by the user This is also the case for our debugger Tools to prove termination of a given goal are undoubtedly useful but they are outside the scope of declarative debugging as such e Input output Although the TOY system supports I O interaction in monadic style see Chapter 5 the current debugger can only be applied to computations that do not involve any kind of I O operations Extensions of the debugger to deal with missing answers and other constraints are currently being investigated 6 5 How Does it Work Our debugger uses a program transformation approach to obtain the computation tree associated to a wrong computation The process is described in 5 and can be summarized as follows 1 The original program P is transformed into a new program P Each function f Tn gt 7 in P is transformed into a function f 7 7 cTree in P that associates a computation tree to each produced result This new program is then compiled by TOY and loaded as the current program 2 The goal is also transformed and solved using the new program P In this way a com putation tree corresponding to the wrong answer is obtained 3 Finally the computation tree is searched asking questions to the us
181. ions of Bj for any j gt i i e let By Bn a partition of FS such that i Bis By FS ii if f Bi g Bj and j gt i then g f In the sequel we call block to each element B of this partition The set of blocks B1 Bn corresponds to the strongly connected components of a directed graph in which nodes are labeled 227 with the function symbols of the program and arcs are defined by the relation lt Therefore it is clear that any ordering of the blocks satisfies item i For satisfying item 7 we consider a new graph in which each node is labeled with a strongly connected component and arcs are defined by the relation lt extended to components B lt Bj iff there exists f B and g B such that f lt g Notice that this is a directed acyclic graph and we can perform a topological sort on it in order to obtain an ordered sequence B Bn which verifies item ii In practice TOY implements both algorithms they can be found e g in 6 to obtain the ordered sequence of blocks As an example consider the following program data nat zero suc nat even nat gt bool even zero true even suc X odd X odd nat gt bool odd zero false odd suc X even X lstEven mat gt bool lstEven true lstEven X Xs lstEven Xs lt even X true lstEven X Xs false lt odd X true from nat gt nat from N Nlfrom suc N In this program we have FS
182. is activated the function log 2 is now handled by the real solver e The file miscfd toy is added to contain useful finite domain functions e More run time errors due to demandness are handled by means of exceptions instead of failures e g belongs sum scalar_product e The implementation of several finite domain functions has been modified also adding some missing usage mode information e New commands prolog Goal Executes the Prolog goal Goal status Informs about the loaded libraries version Displays the Toy software version e More examples have been added Moreover the directory examples becomes more struc tured examples Uncataloged examples examples apifd Program examples for the API FD examples cflpfp Program examples for CFLP FD examples cflpr Program examples for CFLP R examples debug Debugging examples examples failure Programming with failure examples examples flp Functional logic programming examples examples fp Functional programming examples examples h_constr Program examples for Herbrand constraints equality and disequality examples io_file Program examples for the library 10 File examples io_graphic Program examples for the library IO Graphic examples lp Logic programming examples examples tads Program examples for abstract data types e New sections in the manual 250 Release Notes History Known Bugs Deprecations e substract in misc toy See Section
183. is shown include cflpfd toy distribution int gt int gt int gt int gt int gt int gt int gt real gt real gt real gt real gt real gt real gt real gt real gt real distribution D1 D2 D3 CDi CD2 CD3 CD R1 R2 R3 CR1 CR2 CR3 CR X C lt new bridges are created for discreet quantities of raw material Di Dir D2 D2r D3 D3r quantities integer of raw material domain D1 D2 D3 O 100 quantities real of raw material R1 gt 0 0 R2 gt 0 0 R3 gt 0 0 R1 lt 100 R2 lt 100 R3 lt 100 Cost of the raw material provided by the discreet suppliers CD1 3 D1 CD2 2 D2 CD3 2 D3 CD CDr CD CD1 CD2 CD3 Cost of the raw material provided by the continuous suppliers 122 CR1 2 R1 CR2 2 CR CR1 CR2 CR3 E is necessary to avoid 1 lt E E lt 1 C CDr X is units of weight to X Dir D2r D3r Ri minimize C C labeling 1 5 R2 CR3 3 1 2 R3 rounding errors CR E satisfy R2 R3 mini D1 D2 D3 If we compile and load this program we can submit a goal which the demand to satisfy is of 9 units of weight As the propagation has not been activated this goal is solved using only binding Toy R FD gt distribution Di D2 D3 CDi CD2 CD3 CD R1 R2 R3 CR1 CR2 CR3 CR 9 SYSTEM ERROR system_error Non linear constraints or unbounded problem The system shows us that is not able to solve it How
184. ise it returns false e Reifiable Not applied e Example Finite Domain Constraints library loaded Toy FD gt empty_fdset S 8S gt 0 B gt true Elapsed time 10 ms sol 1 more solutions y n d a y 1 B gt false 0 AS Elapsed time 10 ms 93 sol 2 more solutions y n d a y no Elapsed time O ms fdset_parts 3 fdset_split 3 Type Declaration fdset_parts int int fdset fdset fdset_split fdset int int fdset Modes fdset_parts in in gt in gt inout fdset split in inout inout inout Definition fdset_parts Min Max P returns the FD set which is the union of the non empty interval Min Max and the FD set P and all elements of P are greater than Max 1 Both Min and Max are integers or the functions inf and sup fdset_split S returns the tuple of parameters Min Max P which constructs the FD set S in the same way as fdset_parts Reifiable Not applied Example Toy FD gt fdset_parts 0 1 interval 3 4 S fdset_split S S gt interval 0 1 interval 3 4 T gt 0 1 interval 3 4 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms empty_interval 2 Type Declaration empty_interval int int bool Modes empty_interval in in inout Definition empty_interval Min Max returns true if Min Max is the empty FD set Othe
185. ist concatenation A gt A gt A Ys Ys X Xs Ys X Xs Ys 4 Xs N is the Nth element of Xs A gt int gt A X Xs N if N 0 then X else Xs N 1 iterate A gt A gt A gt A iterate F X Xliterate F F X repeat A gt A repeat X X repeat X copy int gt A gt A copy N X take N repeat X filter A gt bool gt A gt A filter L O 198 filter P X Xs Ah Ah Ah Ah Ah Ah Ah Ah Ah Ah Ah if P X then X filter P Xs else filter P Xs Fold primitives The foldl and scanl functions variants foldli and scanli for non empty lists and strict variants foldl scanl describe common patterns of recursion over lists Informally foldl F a x1 x2 xn F C a x1 x2 xn a Sf x1 ff x2 f xn etc The functions foldr scanr and variants foldri scanri are duals of these functions e g foldr F a Xs foldl flip f a reverse Xs for any finite lists Xs foldl A gt B gt A gt A gt B gt A foldl FZ Z foldl F Z X Xs foldl F F Z X Xs foldl1 A gt A gt A gt A gt A foldli F X Xs foldl F X Xs foldl A gt B gt A gt A gt B gt A foldl FA A foldl F A X Xs strict foldl F F A X Xs scanl A gt B gt A gt A gt B gt A scanl FQ O Q scanl FQ X Xs Q
186. it universal quantification The type inference algorithm uses a function T for obtaining the type of a expression e making use of the type annotations in A I and O A general call to the function T has the form T e A T 0 and it returns a pair 7 0 where 7 is the type inferred for e and 0 is a type substitution variables which must be applied to enable the type inference Type substitutions are just substitutions of types for type variables Tey can be represented as sets of variable 229 bindings in the usual way in particular represents the empty type substitution A call T e A T 0 expects that the three stores A TP and contain type annotations for all the symbols occurring in the expression e The formal definition of T works by recursion on the syntactic structure of the expression e The main cases are presented below assuming that X is a variable c DC f FS and e e are expressions We also use the notation 0102 for the composition of two type substitutions meaning that 02 is applied after 01 e T X A T 9 7 if X T f A T O 7 if f arer T T h A T 7 if hk T A and 7 is a variable renaming of 7 with fresh variables T e1 e2 A L O 7 02 T2 0102 if T e1 A T 0 71 41 and T e2 A T01 001 72 02 T e e A T 0 A40 01020 if T e AL O Ti 01 T e A 101 061 72 02 and 0 is a m g u for 7 02 and T2 gt
187. itions X true lt X 31 XY X Y XY X Y XY X Y real division XY X xY real multiplication xx XY X raised to the power of Y XY X raised to the positive integer power of Y i e XY lt XY X lt Y lt XY X lt Y gt XY X gt Y gt XY X gt Y XY X Y XY XAY abs X Absolute value of X acos X Arc cosine of X acosh X Hyperbolic arc cosine of X acot X Arc cotangent of X acoth X Hyperbolic arc cotangent of X asin X Arc sine of X asinh X Hyperbolic arc sine of X atan X Arc tangent of X atanh X Hyperbolic arc tangent of X ceiling X The least integer greater or equal to X i e X Table 2 1 Primitive Functions 1 2 32 cos X Cosine of X cosh X Hyperbolic cosine of X cot X Cotangent of X coth X Hyperbolic cotangent of X div XY Integer quotient of X and Y exp X Natural exponent of X i e e floor X The greatest integer less or equal to X i e X gcd XY Geatest common divisor of X and Y In X Neperian logarithm of X log XY Logarithm of Y in base X max XY Greater value of X and Y min XY Lesser value of X and Y mod XY Integer remainder after dividing X by Y round X Closest integer to X If X is exactly half way between two integers it is rounded up to the least integer greater than X sin X Sine of X sinh X Hyperbolic si
188. ks are unique This feature makes Golomb Rulers to be really 187 interesting for practical applications such as radio astronomy X ray crystallography circuit layout geographical mapping radio communications and coding theory Traditionally researchers are usually interested in discovering rulers with minimum length and Golomb rulers are not an exception An Optimal Golomb Ruler OGR is defined as the shortest Golomb ruler for a number of marks OGRs may be multiple for a specific number of marks However the search for OGRs is a task extremely difficult as this is a combinatorial problem whose bounds grow geometrically with respect to the solution size 34 This has been a major limitation as each new ruler to be discovered is by necessity larger than its predecessor Fortu nately the search space is bounded and therefore solvable 18 To date the highest Golomb ruler whose shortest length is known is the ruler with 23 marks 35 Solutions to OGRs with a number of marks between 10 and 19 were obtained by very specialized techniques and best solutions for OGRs between 20 and 23 marks were obtained by massive parallelism projects these solutions took several months to be found 35 TOY FD enables the solving of optimization problems by using the function labeling with the value toMinimize X and or toMaximize X these values are intended for the minimization and maximization respectively of an FD variable X Below we show a TOY FD
189. l OL OL merge N OL M OL if le N M 208 then N merge OL M OL else M merge N OL OL le_elems list elt gt elt gt list elt le_elems nil M nil le_elems N L M if le N M then N le_elems L M else le_elems L M gr_elems list elt gt elt gt list elt gr_elems nil M nil gr_elems N L M if le N M then gr_elems L M else N gr_elems L M equations for main operations is_ordered nil true is_ordered N nil true is_ordered N N L is_ordered N L is_ordered N M L if le N M then is_ordered M L else false lt N M insertsort nil nil insertsort N L insert_list insertsort L N mergesort nil nil mergesort N nil N nil mergesort L if length L gt s z then merge mergesort take length L dv s s z L mergesort drop length L dv s s z L quicksort nil nil quicksort N L quicksort le_elems L N N quicksort gr_elems L N Y BINARY TREES module bintree imports nat exporting types nat ops Z S exports data bintree A empty tree bintree A A bintree A left bintree A gt bintree A 209 right bintree A gt bintree A root bintree A gt A depth bintree A gt nat left right and root are only defined for non empty trees body left tree L__ L right tree ___R R root tree __N _ N dept
190. l clauses for goal solving solve G OutStore solve G OutStore solve G Gs Cin Cout solve G Cin Cout1 solve Gs Coutl Cout solve E1 E2 Cin Cout equal E1 E2 Cin Cout solve E1 E2 Cin Cout notEqual E1 E2 Cin Cout It is clear that the predicate solve can be eliminated by partial evaluation resulting in direct calls to equal and notEqual This is done in the system Clauses for Solving Equalities Equalpc equal E1 E2 Cin Cout hnf E1 H1 Cin Cout1 hnf E2 H2 Cout1 Cout2 equalHnf H1 H2 Cout2 Cout equalHnf X H Cin Cout var X binding X H Cin Cout equalHnf H X Cin Cout var X binding X H Cin Cout equalHnf c X1 Xn c Y1 Yn Cin Cout a clause for each c DO equal X1 Y1 Cin Couty equal Xn Yn Coutn 1 Cout binding X Y Cin Cin var Y X Y binding X Y Cin Cout var Y extractCtr Cin X Cout1 CX 243 not member Y CX extractCtr Cout1 Y Cout2 CY append CX CY CXY x Y Cout X CXY Cout2 binding X H Cin Cout occursNot X H SkelH Res extractCtr Cin X Cout1 CX X SkelH propagate X CX Cout1 Cout2 continueBind Res Cout2 Cout occursNot X Y SkY Res occursNot X Y SkY Res occursNot X Y Y Res Res var Y X Y occursNot X c Y1 Yn c Ski Sk Reso Res occursNot X Y1 Sk Reso Res occursNot X Y Sk Res 1 Res occursNot X susp E R S U Res U susp E R S Res v
191. lained in detail in chapter 3 2 16 1 Syntactical Equality and Disequality Constraints Equality tests are frequently used in daily programming As an example consider the following simple function definition likely to appear in many real functional or functional logic programs member X false member X Y Ys if X eq Y then true else member X Ys The symbol eq expresses here some suitable notion for equality In a language like TOY with lazy evaluation the sensible notion for eq is that of strict equality which means that e eq e reduces to true if both e and e are reducible to the same pattern and to false if e and e can be reduced to some extent as to detect inconsistency i e different constructor symbols at the same position in e and e Using the program above as a functional program the expression member zero s loop zero could be reduced to the value true this has involved the evaluation of zero eq s loop yielding the value false in spite of the fact that loop is a diverging function and zero eq zero yielding the value true Now a functional logic language like TOY is also able to perform reductions over expressions containing variables which may become instantiated in the process This reversibility property is one of the nicest that functional logic programming shares with logic programming But reversibility is not easy to achieve in programs requiring equality tests like the example above C
192. le _F therefore a real constraint is buildt _F RX RY afterwards the constraint F lt 2 0 is buildt and submitted to the real solver Second goal is similar 4 4 2 Propagation from R to FD In order to propagate a constraint from R to FD is necessary that each variable has its corre sponding bridge if there is a variable without bridge then it not possible to propagate Now we can not created bridges because a real value is not a integer value Despite sum of two real variables with bridges is a new variable for the flattering process explained previously a new bridge will be created for this new variable Constraints that support propagation from R to FD are listed in Table 4 2 and explained below RX lt RY analogously RX lt RY RX gt RY RX gt RY e Checking Bridges X RX and Y RY e Propagation Constraint If checking bridges is successful then the constraint X lt Y is buildt as mate constraint and submitted to the finite domain solver e Example Toy R FD gt X RX Y RY RX lt RY X RX 115 Constraint Bridges Tested Constraint Created RX lt RY X RX and Y RY X lt Y RX lt a X RX X lt a with aeR a lt RY Y RY la lt Y with acR RX lt RY X RX and Y RY XA lt Y RX lt a X RX X lt a with aeR a lt RY Y RY a 4 lt Y with aeR RX gt RY X RX and Y RY X gt Y RX gt a X RX XH gt a with ack a g
193. lias rank is used to compute the number of compositions involved in a compos ite relationship basicFamilyRelation person gt person gt bool basicFamilyRelation fatherOf true basicFamilyRelation motherOf true basicFamilyRelation son0f true basicFamilyRelation daughterOf true basicFamilyRelation brother0f true basicFamilyRelation sisterOf true type rank nat someRank rank someRank gt zero suc someRank familyRelation rank gt person gt person gt bool familyRelation z F basicFamilyRelation F familyRelation s N F G basicFamilyRelation F familyRelation N G These definitions along with suitable definitions for the behaviour of the basic family relations could be used to solve goals such as R someRank familyRelation R F F alice allan where the non deterministic nullary function someRank is used to search for ranks The goal has the following solution among others R suc suc zero F son0f brotherOf motherOf Note that the answer computed for F can be equivalently written as sonOf brotherOf motherOf which is a higher order pattern according to the syntactic characterization given in Section 2 1 Unfortunately some TOY computations involving higher order patterns can break the type discipline as we explain in the rest of this section A first kind of problem arises when solving goals which include expressions of the form F e1 en
194. lists with elements of type A It behaves as if it were defined by data A 1 A A 23 with the constant constructor for the empty list and the infix right associative data constructor to build a non empty list X Xs with headX Aand tailXs A The Prolog notation X Xs is also supported as an alias of X Xs As in Prolog and Haskell the list notation elemo elem elem 1 is allowed as a shorthand for the reiterated application of the list constructor For instance 1 2 3 is viewed as shorthand for 1 2 3 e Product types and tuples are supported by TOY as explained in Section 2 2 Of course predefined types products functional types and user defined types can be freely combined to build more complex types following the type syntax explained in Section 2 2 For example e leafTree char int is the type of lists of binary trees storing pairs of type char int at their leaves e int gt int is the type of functions which accept a list of integers as an argument and return an integer result e int gt int is the type of the lists whose elements are functions of type int gt int e A gt B gt leafTree A gt leafTree B is the type of polymorphic functions which expect two parameters a function of type A gt B and a tree of type leafTree A and return as result another tree of type leafTree B The last two items above illustrate the use of functions as first class values t
195. llowing categories e identifier A lower case letter followed by any sequence of letters digits and symbols and _ e variable Analogous to identifier but beginning with an upper case letter e Integer sequence of digits optionally preceded by a symbol e Float sequence of digits including a decimal dot and optionally preceded by a symbol gt e Char Any character enclosed between single quotes Also some special characters in cluding control characters must be preceded by a backslash The following list presents these special characters AY backslash AP quote double quote A new line E carriage return t horizontal tabulator Av vertical tabulator Na bell 216 lt gt data else if in include includecflpfd reserved infix infixl infixr primitive then type where Table D 1 Reserved Symbols User Defined Function Data Type Data Constructor Function x J x Predefined Data Type V x v Data Constructor x V x Table D 2 Predefined vs User Defined Symbol Compatibility Table Ab backspace AP form feed Me escape d delete e String Sequence of characters enclosed by double quotes e Bool Either true or false e Operator Sequence of characters in the set PP 7 7 amp 7 747 77 L 737 77 ANA 71 7 72 7 whose first character is neither nor nor e
196. ls to find a winning movement form it This scheme can be applied for a variety of games As an example we introduce the Nim 52 game we have a set of rows with sticks and a movement consists in dropping one or more sticks from an unique row The state of the game can be represented by a list of integers where each one represents the number of sticks of a row A legal movement is defined in a non deterministic way with the function move as follows pick N N 1 lt N gt 0 pick N pick N 1 lt N gt 0 move N Ns move N Ns pick N Ns N move Ns Here the function pick takes one or more sticks from a row and move picks some sticks from one row Now we can evaluate Toy gt winMove 1 2 2 S s gt E Elapsed time 16 ms sol 1 more solutions y n d a y no Elapsed time O ms That is we must drop the stick from the first row It is easy to check that for any possible movement of the adversary we can assure the victory The reader may try to program the tic tac toe game by providing a representation for the panel and the function move Apart from fails TOY provides some other related primitives In a non deterministic language it is interesting in some cases to have a set of solutions more than a single solution for a given problem The usual way for providing these solutions is to get one by one by backtracking like in Prolog or also in TOY But there are situations for which it is useful to obtain the full set
197. lscanl F F Q X Xs scanli A gt A gt A gt A gt A scanli F X Xs scanl F X Xs scanl A gt B gt A gt A gt B gt A scanl FQ O Q scanl F Q X Xs Qlstrict scanl F F Q X Xs foldr A gt B gt B gt B gt A gt B foldr FZ Z foldr F Z X Xs F X foldr F Z Xs foldr1 A gt A gt A gt A gt A foldri F X X 199 foldri F X Y Xs F X foldri F Y Xs scanr A gt B gt B gt B gt A gt B scanr F QO Q0 scanr F QO X Xs auxForScanr F X scanr F QO Xs Zwhere auxForScanr F X Ys F X head Ys Ys scanr1 A gt A gt A gt A gt A scanri F X X scanri F X Y Xs auxForScanr F X scanri F Y Xs hp List breaking functions Ah hh take n Xs returns the first n elements of Xs hh drop n Xs returns the remaining elements of Xs hh splitAt n Xs take n Xs dropn Xs hh hh takeWhile P Xs returns the longest initial segment of Xs whose Ah elements satisfy p hh dropWhile P Xs returns the remaining portion of the list hh span P Xs takeWhile P Xs dropWhile P Xs hh hh takeUntil P Xs returns the list of elements upto and including the hilo first element of Xs which satisfies p take int gt A gt A take N 1 O take N X Xs if N 0 then else X take N 1 Xs drop int gt A gt A drop N drop N X Xs Il H
198. lt i lt m This may be possible if 7 is a type variable or a functional type For example using the instance obtained from twice s principal type by the substitution At bool gt bool gt bool gt bool one obtains twice twice not true bool 2 3 Datatype Definitions Datatypes also called constructed types are defined along with data constructors for their val ues Datatype definitions in TOY are introduced by the keyword data and have the following schematic syntax data 6A oTo Cm 1 Tm 1 where 6 is the type constructor A is a shorthand for A An n gt 0 a sequence of different type variables acting as formal type parameters c 0 lt i lt m are the data constructors for values of type 6 A and 7 is a shorthand for Ti 1 Tin a Series of types corresponding to the arguments of ci The types 7 must be built from the type variables A predefined types and user defined type constructors according to the syntax of types explained in Section 2 2 21 Different datatype definitions must declare disjoint sets of data constructors The principal type of any data constructor c occurring in a program is determined by the datatype definition where c has been declared In terms of the general scheme above Ci i Tir gt gt Tin gt A for allO lt i lt m A datatype is called polymorphic or also generic iff the number n of formal type parameters in its definition is greater than zero and monomorph
199. lutions y n d y X gt 0 L gt bisect ff Elapsed time O ms Up to all the correct answers e More examples added to the distribution e User Manual updated draft published e New formatted output e Nonlinear real functions revisited Arguments of nonlinear real functions do not need to be instantiated when the library CLP R is loaded 1n exp cot asin acos atan acot sinh cosh tanh coth asinh acosh atanh acoth Deprecations e all_distinct is deprecated since its behaviour is the same as all_different e all_distinct is deprecated since its behaviour is the same as all_different Changes e fdset becomes simply fdset See type declaration in User Manual Fixed Bugs e The goal labeling X Y ran into an infinite loop Fixed 253 e The goal domain id X 0 1 with the program id A gt AidA A shows the following error SYSTEM ERROR type_error domain susp id _116 _121 _122 0 1 1 integer susp id _116 _121 _122 The same situation held for labeling Fixed e Reification Missing answer Toy FD gt domain X 0 1 B lt gt X 0 X gt 0 B gt true Elapsed time O ms more solutions y n d y no Elapsed time O ms With the current version Toy FD gt domain X 0 1 B lt gt X 0 X gt 0 B gt true Elapsed time O ms more solutions y n d y X 1 B gt false Elapsed time O ms more solutions y n d y
200. magicfrom int gt int magicfrom N lazymagic Nlmagicfrom N 1 Now it is easy to generate a list of N magic series For example the following goal generates a 3 element list containing respectively the solution to the problems of 7 magic 8 magic and 9 magic series Toy FD gt take 3 magicfrom 7 Le 13 2 d ty 04 0s 5 2 1 0 0 1 Elapsed time 141 ms sol 1 more solutions y n d a y no 0 gt gt 0 0 0 Elapsed time O ms More expressiveness is shown by mixing curried functions HO functions infinite lists and func tion composition another nice feature from the functional component of TOY For example consider the code below from int gt int from N Nlfrom N 1 lazyseries int gt int lazyseries map lazymagic from where the operator defines the composition of functions as follows again the function 2 is predefined in the file misc toy B gt C gt A gt B gt A gt C F G X F G X Observe that lazyseries curries the composition map lazymagic from Then it is easy to generate the 3 element list shown above by just typing the goal Toy FD gt take 3 lazyseries 7 L gt 3 2 1 1 0 0 0 4 2 1 0 1 0 0 0 5 2 1 0 Oy 1 0 0 0 1 Elapsed time 125 ms sol 1 more solutions y n d a y no Elapsed time O ms 3The function take 2 is predefined in the file misc toy see
201. me gt that must have been previously compiled where lt filename gt will be the desired name of the dumped state 14 1 5 5 Commands for Constraint Solvers e cflpr Enables arithmetical constraints over real numbers The effect of this command is the loading of the library for constraint solving over real numbers Once executed the system prompt changes to Toy R gt and equations as the following can be solved Toy R gt X 3 X gt 2 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms or more complex equation systems as Toy R gt 2 X 3 Y Z 3 X 6 Y 2 Z Z 2 Y X gt 2 Y gt f Z gt 4 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms For a detailed explanation of this kind of constrains see Section 2 16 e nocflpr Disables arithmetical constraints over real numbers e cflpfd Enables constraints over finite domains The effect of this command is the loading of the library for constraint solving over finite domains Once executed the system prompt changes to Toy FD gt and TOY can solve goals as Toy FD gt domain X Y 1 10 X gt Y Y lt 3 This goal asks for integral values of X Y belonging to the interval 1 10 and that X 3 gt Y the symbols and gt are used in finite domain constraints instead of and gt respectively The answer provided by the system is Y lt X X in 2 10
202. mited to the derivation of approxi mation statements and strict equality conditions However TOY programs can also use other kinds of conditions including disequality and arithmetic constraints see Sections 2 6 and 2 16 In order to obtain a declarative semantics for such programs CRWL must be extended to a more powerful inference system CCRWL say with the ability to derive conditional statements of the form o gt y where is a finite conjunction of atomic conditions and y is either an ap proximation statement or an atomic condition The definition of CCRWL is currently ongoing work Our aim is to characterize the declarative semantics of a program P as the set of all the conditional basic facts of the form o gt f t tn gt t such that P FecrwL o gt f ti tn gt t This will naturally lead to a logical criterion of correctness for computed answers includ ing constraints For instance in Section 2 13 whe have already met the computed answer L 2 X 3 X gt 2 0 X lt 3 0 for the goal permutationSort 3 2 X L The logical correctness of this computation means that CCRWL should be able to derive the conditional statement L 2 X 3 A X gt 2 0 A X lt 3 0 gt permutationSort 3 2 X L We also expect CCRWL to provide a logical basis for the declarative debugging of TOY programs with constraints thus eliminating one limitation of the current debugger see Chapter 6 239 Appendix G Operational Semantics
203. ms sol 1 more solutions y n d a y no Elapsed time O ms fd_degree 1 e Type Declaration fd degree int int e Modes fd degree inout gt inout e Definition fd_degree V returns the number of constraints that are attached to V e Reifiable Not applied e Example 90 Toy FD gt domain X Y 0 10 X gt Y Degree fd_degree X Degree gt 1 Y lt X X in 1 10 Y in 0 9 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms fd_neighbors 1 e Type Declaration fd_neighbors int gt int e Modes fd_neighbors inout inout e Definition fd_neighbors V returns the set of FD variables that can be reached from V via constraints posted so far e Reifiable Not applied e Example Toy FD gt domain X Y 0 10 X 5 X lt Y Vars fd_neighbors X Vars gt _C X Y gt Y X X in O 4 6 9 Y in 1 10 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms fd_closure 1 e Type Declaration fdclosure int int e Modes fd_closure inout inout e Definition fd_closure V returns the set of FD variables including V that can be transitively reached via constraints posted so far Thus fd_closure 1 returns the transitive closure of fd_neighbors 1 91 e Reifiable Not applied e Example Toy FD gt domain
204. n d a y X gt 2 Y gt 1 Elapsed time O ms 120 sol 2 more solutions y n d a y X gt 2 Y gt 2 Elapsed time O ms sol 3 more solutions y n d a y X gt 3 Y gt 1 Elapsed time O ms sol 4 more solutions y n d a y no Elapsed time O ms Figure 4 5 Four solution This goal computes four solutions for X Y corresponding to the points 2 2 1 1 2 1 and 3 1 Table 4 3 compares the timing results for executing below goals The first column indicates the height of triangle second indicate the vertice RXo RYo third indicate the size of the square grid The next columns show running times in milliseconds in the form tg tgp where tg stands for the system using bridges for binding alone and tgp for the system using bridges also for propagation These last columns are headed with a number i which refers to the i th solution found and the last column with numbers stands for the time needed to determine that there are no more solutions In this simple example we see that the finite domain search space has been hugely cut by the propagations from R to FD Finite domain solvers are not powerful enough to cut the search space in such an efficient way as simplex methods do for linear real constraints The cooperation of a FD solver and a R solver via communication bridges can lead to great reductions of the FD search space manifesting as significant speedups of the e
205. n defining operations such that they check the arguments is_stree stree elt gt bool is_stree empty true is_stree tree empty _ empty true is_stree tree L N empty if is_stree L then le maxt L N else false lt L empty is_stree tree empty N R if is_stree R then le N mint R else false lt R empty is_stree tree L N R if is_stree L then if le maxt L N then if is_stree R 211 then le N mint R else false else false else false lt L empty R empty equations for main operations insert empty M tree empty M empty insert tree L N R M if eq M N then tree LMR else if le M N then tree insert L M NR else tree L N insert R M delete empty _ empty delete tree L N R M tree delete L M NR lt le MN delete tree L N R M tree L N delete R M lt le NM delete tree empty NR M R eq NM delete tree L N empty M L eq NM delete tree L N R M tree L X delete R X lt eq N M L empty R empty X mint R is_in empty _ false is_in tree L N R M if eq MN then true else if le MN then is_in L M else is_in RM SORTING A LIST USING A SEARCH TREE module searchtree_sort parameters type elt le elt gt elt gt bool eq elt gt elt gt bool extends ordlist default instantiation imports searchtree 212 default instantiation exports stree_sort list elt gt list elt body local auxiliary op
206. n generate for example tautologies of complexity 3 with the goal Toy gt complexity F s s s z isContradiction F true F gt neg disy p iff p p gt Elapsed time 94 ms more solutions y n d y F gt neg disy p iff q q gt Elapsed time O ms more solutions y n d y In the same way we can produce contradictions or contingencies A 5 Programming with Equality and Disequality Constraints One of the most interesting characteristics of TOY is that of dealing with equality and disequality constraints as well as arithmetic constraints over real numbers We show the power of this feature by means of some examples A 5 1 The Cardinal of a List cardinal toy Next example shows that JOY can represent solutions by using equality and disequality con straints Function card determines the cardinal of a given list regarded as a set It relies on the boolean function member that specifies whether an element occurs in a list or not card A gt int card 0 card X Xs if member X Xs then card Xs else 1 card Xs member A gt A gt bool member X 0 member X Y Ys if X Y then true else member X Ys Let s consider as an example 167 Toy gt card 1 0 1 N gt 2 Elapsed time O ms more solutions y n d y no Elapsed time O ms A more involved example using logic variables shows the convenience of equality and disequality constraints in solution
207. n logic is an open Herbrand model of P and even the least open Herbrand model w r t set inclusion All this can be generalized to the case of multiparadigm declarative languages like TOY Here we limit ourselves to introduce the analog of open Herbrand models results about more general models can be found in 11 13 Given a TOY program P an open Herbrand interpretation is defined as any set Z of atomic facts ft tn t which satisfies the three following closure properties 1 fti tn gt L EJ for all f FS and all possible partial patterns t 1 lt i lt n 2 IF fti tn gt t ET and t E t 1 lt i lt n and t It THEN ft t gt t EZ 3 IF fti tn gt t E T and is any substitution of total patterns for variables THEN fti tn gt HOET Given an open Herbrand interpretation Z and any statement y let us use the notation Z E y reads p is valid in T to indicate that y can be derived in the inference system consisting of all the CRWL inference rules except FC which is replaced by the following inference rule A Tig ies tn TA q t AF7 Atomic Fact in T a a k gt 0 fei enai ag gt t IF fti tn gt r ET An open Herbrand interpretation Z is called a model of a program P iff every program rule instance f t tn gt r lt 4 C P 1 is true in Z when interpreted as a conditional implication more precisely the following must hold IF TEC i
208. n their domains again in ascending order search_naive int gt bool search_naive true search_naive X false lt empty_fdset fd_set X search_naive X true lt domain X fd_min X fd_min X search_naive X true lt Next fd_min X 1 domain X Next fd_max X search_naive X search_naive X X1 Xs true lt search_naive X search_naive X1 search_naive Xs search_ff int gt bool search_ff true search_ff X false lt empty_fdset fd_set X search_ff X true lt domain X fd_min X fd_min X search_ff X true lt 194 Next fd_min X 1 domain X Next fd_max X search_ff X search_ff X X1 Xs true lt choose_min_and_remove X X1 Xs Y Ys choose_min_and_remove Ys Y2 Yss search_ff Y search_ff Y2 search_ff Yss choose_min_and_remove int gt int gt int gt bool choose_min_and_remove X X true choose_min_and_remove X Y Ys M YI Rs fd_set X SX fd_set Y SY fdset_size SX lt fdset_size SY choose_min_and_remove X Y Ys M X Rs choose_min_and_remove Y Ys M Rs lt fd_set X SX fd_set Y SY fdset_size SX gt fdset_size SY choose_min_and_remove X Ys M Rs lt Observe that when there are several variables to label this function selects the one with the minimum domain cardinality via choose min_and_remove 3 by making use of information recovered by the reflection functions fd_set 2
209. n this sense CLP FD may be considered as a strict subset of CFLP FD with respect to problem formulation As a direct consequence our language is able to cope with a wide range of applications in particular all those pure programs that can be formulated with a CLP FD language Due to its functional component CFLP FD adds further expressiveness to CLP FD as allows the declaration of functions and their evaluation in the FP style Functions are first class citizens which means that a function and thus any FD constraint can appear in any place where data do As a direct consequence an FD constraint may appear as an argument or even as a result of another function or constraint The functions managing other functions are called higher order HO functions Also polymorphic arguments are allowed in CFLP FD In contrast to logic languages functional languages support lazy evaluation where function arguments are evaluated to the required extend the call by value used in LP vs the call by need used in FP Strictly speaking lazy evaluation may also correspond to the notion of only once evaluated in addition to only required extent 31 TOY increases the power of CLP FD by incorporating a novel mechanism that combines lazy evaluation and FD constraint solving in such a way that only the demanded constraints are sent to the solver For example it is possible 66 to manage infinite lists of constraints 3 1 1 Efficiency In 9 we
210. name gt toy together with other information e As we have seen in order to compute a goal from a program it is needed to 1 compile the program and 2 to load the target code These processes are performed by means of three commands compile lt filename gt compiles the file lt filename gt lt filename gt toy if there is not an explicit extension in the name and produces the file lt filename gt pl as a result This target file is not loaded so it is not possible to evaluate goals from this program yet The compilation of a program implies several kinds of analysis of the source code The system checks the syntax the functional dependencies and the types During these phases the system delivers messages about the evolution of the process and detected errors If there is not any error the target code is produced 11 load lt filename gt loads the target code of the program lt filename gt toy previ ously compiled with compile Then goals can be evaluated from this program run lt filename gt compiles and loads the program This is the most frequently used command for processing programs Therefore in the example above we could have tried simply Toy gt run insert Note about Loaded Code Each time a code a compiled code from either a user program or a system library CFLP R CFLP FD IO File or IO Graphic is loaded the definitions previously loaded for user programs are removed This means t
211. ne of X sqrt X Square root of X tan X Tangent of X tanh X Hyperbolic tangent of X toReal X The real number equal to the integer X trunc X The integer part of X uminus X X Table 2 2 Primitive Functions 2 2 33 X Y false lt X Y X Y false lt X Y X Y true lt X Y Similar defining rules could be also written for the behaviour of gt lt gt and lt as boolean functions Actually the TOY system runs optimized versions of these definitions The system file basic toy includes also definitions for some other predefined functions given by TOY defining rules of the kind described in Section 2 6 Currently the predefined functions are if_then_else bool gt A gt A gt A if_then_else true X Y X if_then_else false X Y Y if_then bool gt A gt A if_then true X X flip A gt B gt C gt B gt A gt C flipFXY FYX Instead of writing if_then_else b e e and if_then b e in prefix notation TOY allows to use the standard syntax if b then e else e and if b then e Nevertheless the prefix versions are useful for enabling partial applications The function flip has been predefined for technical reasons since it is used internally by the TOY system in order to express operator sections as partial applications The coexistence of both primitive and predefined function definitions in the system file basic toy also obeys to technical reasons
212. ng tkOval int int int int string The last arguments are further options in tcl syntax The type tkRefType allows to reference widgets This datatype is built in and the references are built automatically Thus the data constructor tkRef must always be used with a variable as an argument Such a variable will be able to be used by the programmer whenever he wants to reference the widget in order to access or to change its configuration We will show the use of the constructor tkRef in following examples The datatype defining the options for geometric alignment of widgets is data tkConfCollection tkCenter Centered alignment tkLeft Left alignment tkRight Right alignment 134 tkTop Top alignment tkBottom Bottom alignment tkExpand 7 Expands subwidgets if extra space is avalaible tkExpandX Expands subwidgets horizontally if extra space is avalaible tkExpandY Expands subwidgets vertically if extra space is avalaible As an example consider the function hello_world2 defined previously The associated layout of the GUI can be defined now by using the new datatypes The resulting code would be win_hello tkWidget io unit win_hello tkRow tkButton eventHello tkText Hello World tkButton eventExit tkText Exit eventExit channel gt io unit eventExit Ch do putStrLn Goodbye tkExit Ch eventHello channel gt io unit eventHello Ch putStrLn Hello World The execution loop d
213. ng all applications in first order syntax using the new symbols of the enhanced signature whenever necessary e Adding program rules for the new function symbol 240 The details of this translation are given below The semantic correctness of the translation has been justified in 12 G 1 1 Enhancing the Signature Given a signature Y DC U FS the first order signature corresponding to is Xo DC fo U FS fo where FSf FSU A DC fo Ucepon nen oiy Cn U Usersn nent fo gt fn 1 where c0 Cn fo fn 1 are new symbols The idea is that in first order syntax we use the symbol c whenever in higher order syntax we encounter the symbol c applied to i arguments and similarly for f G 1 2 First Order Translation of Program Rules and Rules for Let P be a TOY program consisting of the rules R Rn Then the first order translation of P fo P is defined as follows fo P fo R1 fo Rn U Rules fol e lt C fo l fo e fo C fo X X fo n n fol e1 n _ fo e1 folen fo c e1 ex cr fo er fo ex fc e DO k lt n fo f e1 ex f fo e1 fo ex if fe FS k lt n fo f e1 en f foler folen if f EFS fo f 1 en n41 ntk Q f foler folen folen 1 Folen 1 iffeFS k gt 0 fo X ener Q Q X fo er fo ex folei o e2 fole1 o fo e2 if o lt lt gt gt The
214. not enough to produce an outcome as the goal requests goes into a non ending loop However the lazy evaluation mechanism of TOY FD allows to evaluate a finite number N of requests this can be done by redefining the functions client answers and requests as follows client int gt int gt int client Ini Rs Ini client next head Rs tail Rs answers int gt int answers N server requests N requests int gt int requests N take N client initial take N answers N where head 1 and tail 1 return the head and tail of a list respectively Below we show an example of solving that evaluates exactly the first 15 requests Toy FD gt requests 15 L gt 4 7 10 13 16 19 22 25 28 31 34 37 40 43 46 Elapsed time 47 ms more solutions y n d y no Elapsed time O ms 160 A 3 Functional Logic Programming Now we turn to simple examples that show the skill of JOY in combining the features of the functional and logic languages A 3 1 Inserting an Element in a List insert toy Function insert defined below inserts an element X in a list insert A gt A gt A insert X J X insert X YlYs X Y Ys insert X Yl Ys Ylinsert X Ys If the list is empty there is only one possibility as the first rule of insert reflects On the contrary if the list has n elements with n gt 0 there are n 1 different ways of inserting X In logic programming and in
215. ns u int and v real to take the same integer value Bridges are used for two purposes Binding and propagation Binding simply instantiates a variable occurring at one end of a bridge whenever the other end of the bridge becomes a numeric value Propagation is a more complex operation which takes place whenever a pure constraint is submitted to the FD or R solver At that moment propagation rules relying on the available bridges are used for building a mate constraint which is submitted to the mate solver think of R as the mate of FD and viceversa Propagation enables each of the two solvers to take advantage of the computations performed by the other In order to maximize the opportunities for propagation the CFLP goal solving procedure has been enhanced with operations to create bridges whenever possible according to certain rules 4 1 1 Efficiency Example 4 5 1 compares the timing results for executing the same goals with only binding and binding and propagation shown that the propagation of mate constraints dramatically cuts the search space thus leading to significant speedups in execution time as it is shown in Table 4 3 109 4 1 2 Libraries necessaries for Cooperation In order to use cooperation is necessary to activate finite domain and real solvers it is done by means of the commands cflpfd and cflpr as explained in Section 1 5 5 With both solvers activated is possible compile programs that use the communication constraint b
216. nt gt bool constrain_between X N true constrain_between X Y Ys N true lt no_threat X Y N N1 N 1 constrain_between X Ys N1 no_threat int gt int gt int gt bool no_threat X Y I true lt X Y X I Y X I Y Again if we compile and load this program we can solve goals as Toy FD gt queens 4 L ff L gt 2 4 1 2 Elapsed time 20 ms sol 1 more solutions y n d a y L gt 3 dy 4y 2 F Elapsed time 10 ms sol 2 more solutions y n d a y 105 no Elapsed time O ms 3 3 4 A Cryptoarithmetic Problem alpha toy Alpha is a cryptoarithmetic problem where the numbers 1 26 are randomly assigned to the letters of the alphabet The numbers beside each word are the total of the values assigned to the letters in the word e g for LYRE L Y R E might equal 5 9 20 and 13 respectively or any other combination that add up to 47 The problem consists of finding the value of each letter under the following equations BALLET 45 GLEE 66 POLKA 59 SONG 61 CELLO 43 JAZZ 58 QUARTET 50 SOPRANO 82 CONCERT 74 LYRE 47 SAXOPHONE 134 THEME 72 FLUTE 30 OBOE 53 SCALE 51 VIOLIN 100 FUGUE 50 OPERA 65 SOLO 37 WALTZ 34 A TOY solution included in the distribution in the directory Examples in the file alpha toy is shown below include cflpfd toy alpha labelingType gt int gt bool al
217. ntegral constraints for X and Y Toy R gt X Y Z X gt 0 X lt 2 Y gt 0 Y lt 2 X Y bb_minimize Z X Y I X gt 0 Y gt 0 Z gt 0 I gt 0 Elapsed time 16 ms sol 1 more solutions y n d a y no Elapsed time O ms That is the answers X gt 1 Y gt 1 Z gt 0 I gt O and X gt 2 Y gt 2 Z gt 0 I gt 0 are missing e bb_maximize real gt real gt real The application bb_maximize X Is is equivalent to bb_minimize X Is 65 Chapter 3 Constraints over Finite Domains In this chapter we present the implementation of Constraint Functional Logic Programming over Finite Domains CF LP FD with the lazy functional logic programming language TOY which seamlessly embodies finite domain FD constraints CF LP FD increases the expressiveness and power of constraint logic programming over finite domains CLP FD by combining functional and relational notation curried expressions higher order functions patterns par tial applications non determinism lazy evaluation logical variables types domain variables constraint composition and finite domain constraints 3 1 Introduction CFLP FD provides the main characteristics of CLP FD i e FD constraint solving non determinism and relational form Moreover CF LP FD provides a sugaring syntax for LP predicates and thus any pure CLP FD program can be straightforwardly translated into a CFLP FD program I
218. nterleaved way which also includes an optimized occur check see Appendix G for details Disequality Constraints A constraint e e is satisfied if e and e can be reduced to an extent as to have a constructor clash which means having different constructor symbols at the same external position that is positions not insidea function application A disequality e e can be satisfied even if e or e do not have a normal form 57 Examples With the following definitions loop loop divergence undefined undefined lt false failed reduction from N N from suc N infinite list the following ground goals have in each case the indicated behaviour 0 0 1 0 succeeds from zero from suc zero succeeds 0 undefined 1 undefined succeeds undefined 0 undefined 1 succeeds 0 loop 1 loop succeeds loop 0 loop 1 succeeds 0 0 0 0 fails O undefined 0 undefined fails 0 loop 0 loop diverges from zero from zero diverges In presence of variables the constraint solving mechanism to check satisfiability of disequal ity constraints tries to reduce them to solved forms of the shape X t X tn Y 51 Y Sm which are known to be satisfiable if the set of ground terms is infinite 8 During a computation the accumulation of these solved forms constitutes a disequality con straint store which plays a dynamic role if at a gi
219. o so that they can be used both for constraints and for functions Strict Equality Constraints To understand how constraint solving proceeds it is useful to explain two different things e When a constraint is satisfied or valid that is it is true for all values of its variables e When a constraint is satisfiable that is there are values of its variables making it true The first notion fixes the semantics of the constraint while the second is more related to constraint solving which tries to check satisfiability by reducing constraints to solved form For the case of equality constraints we can say that e e el is satisfied if e and e can be reduced to the same pattern e A constraint e e is satisfiable if e and e can be reduced to unifiable patterns Solved forms are the results of such unifications that it idempotent substitutions which can be seen and showed as sets of solved equations According to the semantics a constraint e el could be solved by reducing e and e to normal forms patterns and then unifying them But in practice to interleave the reduction of e and e is better from the point of view of detecting failure For instance the constraint suc e zero is not satisfiable whatever the expression e is To reduce e which can be costly or even diverging is needed to reach a normal form for suc e but not to detect the failure of the constraint TOY solves equality constraints is such i
220. omata ends_ab that accepts words ending with ab 164 a b a 0 D The transiction function 6 is programmed as before but now the function accept is wrong because accept ends_ab abb would reduce to true and to false it is possible to make transictions to state 2 but also it is possible to stay at state 0 The function accept needs another definition in the case of non deterministic automata accept D I Fs W if member deltaGen D I Fs I W Fs then true default accept D I F s W false The first rule says reduces to true if there is a transiction from the initial state to a final state while the second rule reduces to false otherwise that is when there is not any sequence of transictions that reach a final state This is exactly what we want and it can be implemented using fails as accept D I Fs W accept D I Fs W accept D I Fs W false lt fails accept D I Fs W accept D I Fs W if member deltaGen D I Fs I W Fs then true A 4 2 A Propositional Tautology Generator tautology toy The function fails allows to transform failure of reduction into the boolean value false In this example we illustrate the reverse use transform the value false into a failure obtaing more control on the non deterministic reductions First of all to manage success results we introduce the function success success true true This function is the identity on the value true The interest of s
221. on function definitions to split the program into blocks of mutually dependent functions and then it uses the resulting blocks to do perform type inference in the proper sense E 1 Dependency Analysis When a function f is defined by using another function g we say that the f depends on g It is quite natural to assume that in such case the type of f must be inferred before the type of g of course if g does not use f in its definition But if we have a set of mutually recursive functions then we must infer their types simultaneously So first of all we have to study the dependencies between the function definitions of the program to extract blocks of mutually dependent functions We define the relation lt over function symbols of a program as f lt y the definition of g uses f This relation corresponds to a simple syntactical criteria we have f lt g iff there is some defining rule of g that includes the symbol f in its right hand side or in its conditions or in its local definitions Consider now the reflexive and transitive closure lt of lt and the relation defined as f g iff f lt g and g lt f i e the definitions of f and y are mutually dependent The relation is an equivalence relation and we can consider the quotient set F S where FS is the set of function symbols of the program We need to consider a sorted sequence B Bn of equivalence classes of FS in such a way that functions of B do not use funct
222. on readFile reads a file named by a string and returns the contents of the file as a string The file is read lazily on demand that is the effect of the action readFile FileName only opens the file named FileName A character in the file only is read if it is needed in following computations As an example consider the function only_one_char io unit only_one_char do putStr Name of the file Name lt getLine Cs lt readFile Name putStrLn head Cs The execution of the expression only_one_char has the following effect The text file named Name is opened when the action readFile Name is executed After this the action putStrLn head Cs demands the head of Cs Then the first character of the file is read Since the computation finishes the rest of the file is not read and the file is closed by the system The function writeFile writes the string its second argument to the file its first argument Writing to a file is an eager action in the sense that the second argument must be totally evaluated before writing it to the file Once the process terminates the file is closed by the system The action copyFile below shows how to copy the contents of a file into another copyFile io unit copyFile do putStr First File Filet lt getLine putStr Second File 129 File2 lt getLine Cs lt readFile Filel writeFile File2 Cs It is important to point out that the evaluation of th
223. ons 2 2 pg 19 and 2 6 pg 26 respectively 3 After saving the file insert toy we are ready to compile the program But first we must move to the directory where the file has been stored For this type Toy gt cd examples in order to change to the folder examples 4 Compile the program by typing 10 Toy gt compile insert If there is some error the compilation will stop with a hopefully informative error mes sage If so fix the error and repeat the command compile insert until no error is found 5 Load the compiled file with Toy gt load insert The program is ready to be used 6 Now we can submit a goal as Toy gt insert 0 1 2 3 R and TOY will yield a first computed answer R gt 0 1 2 3 Elapsed time O ms sol 1 more solutions y n d a y If we type y the system will provide another computed answer In this way we can check that the goal has 4 computed answers which correspond to the 4 possible forms of inserting 0 in the list 1 2 3 This an example of an non deterministic computation 7 Type q when you want to leave the system Some remarks about this session e TOY uses Prolog as target code so in the process of compilation the user programs are translated into Prolog code The compilation of a source file lt filename gt toy produces the file lt filename gt pl that contains the code corresponding to the translation of the functions and predicates in lt file
224. ons given in the text of a TOY program are well typed In the positive case the algorithm infers a principal type of the form foun Ti gt gt TH gt T for each n ary function symbol f FS occurring in the program Boolean functions with type pi Ty gt gt Tn gt bool are called also predicates in TOY Note that two functions fou 1 gt 72 gt T and g Ti T2 gt T have related but different types Function f can be applied to an argument of type 7 and returns a function that expects another argument of type T2 returning in turn a result of type T On the other hand g expects a pair of product type T1 T2 as argument and returns a result of type T Assumming that the final result is always the same i e FAY g X Y fral X 2 n Y Ts one says that function f is the curried version of function g The word curried comes from Haskell Curry one of the first mathematicians who discovered this idea The principal type of a function can include type variables In this case the function as well as its type is called polymorphic A polymorphic function has an implicit universal quantification 20 over the type variables occurring in its principal type Different substitutions of types for those type variables give rise to different instances of the function For example from the definition of twice shown in Section 2 1 the TOY system infers the principal type twice A gt A gt A gt A As an instance of
225. onsider for instance an expression containing variables such as member X Y One possible reduction could yield the value true together with the substitution X Y which can be also seen as a constraint X Y But member X Y can also be reduced to false if X and Y are given different values An attempt of covering such values by means of substitutions results in infinitely many answers For instance if the program contains the datatype declaration nat zero suc nat then the possible answers would include the following X zero Y suc U X suc U Y zero X suc zero Y suc suc U X suc suc U Y suc Zero 7At least if the set of terms corresponding to the given signature is infinite 56 This family of answers cannot be replaced by any equivalent finite set of substitutions The situation changes drastically if we consider disequality constraints since one single disequality namely X Y collects all the information embodied in all those substitutions TOY ex hibits such behavior because of its ability of explicitly handle equality and disequality constraints corresponding respectively to the positive and negative cases of strict equality as described above Using these constraints the function eq can be defined by the rules X eq Y true lt X Y X eq Y false lt X Y For the sake of clarity we have used throughout this discussion the symbol eq However TOY overloads the symbols and als
226. onstraints in solved form can occur within computed answers TOY provides some additional features which are not found in traditional functional or logic lan guages Non deterministic functions combined with lazy evaluation help to improve efficiency in search problems Higher order patterns enable an intensional representation of functions useful both for functional and logic computations and they do not introduce undecidable uni fication problems These and other features of the language including a declarative semantics in the spirit of logic programming have a firm mathematical foundation This report is intended both as a manual for TOY users and as an informal but hopefully precise description of the language and system Here is a brief description of the overall purpose of each chapter e Chapter 1 Explains how to download and install the TOY system This chapter also gives a first overview of the system s features and tools sufficient to start writing and running program e Chapter 2 Introduces a detailed description of TOY programs covering syntax informal semantics and pragmatics e Chapter 3 Presents the finite domain solver and their applications e Chapter Presents the cooperation between finite domain and real solvers and their applications e Chapter 5 Explains how to include input output interactions in TO e Chapter 6 Introduces the declarative tool for debugging TOY programs In addition a series
227. or intro duced in some datatype declaration see Section 2 3 Defined predicates in TOY are viewed as a particular case of defined functions whose result is boolean As in functional languages expres sions which include defined functions can be evaluated in TOY to compute a result while those expressions which are built only from data constructors can be seen as symbolic representations of computed results In the rest of this document we often use capital letters X Y Z possibly with subscripts as variables Moreover we use the notation c DC to indicate that c is a data constructor which expects n arguments and the notation f FS to indicate that f is a defined function symbol whose definition expects n formal parameters The number n is called the arity of c resp f Constant values belonging to primitive datatypes can be viewed as nullary data constructors in DC Under these conventions the abstract syntax for TOY expressions is as follows e X c f e e1 e1 en Expressions e1 en n gt 0 represent tuples while e es represents the application of the 18 function denoted by e to the argument denoted by es Following usual conventions application associates to the left and outermost parentheses can be omitted Therefore f X g Y Z can be written more simply as f X g Y Z In programming examples we will use meaning ful identifiers rather than these abstract notations The concret
228. or symptom and locates a program fragment responsible for the error In the case of constraint logic programs error symptoms can be either wrong or missing computed answers The overall idea behind declarative debugging is to build a computation tree 29 as logical representation of the computation Each node in such a tree represents the result of a computation step which must follow from the results of its children nodes by some logical inference Diagnosis proceeds by traversing the computation tree asking questions to an external oracle generally the user until a so called buggy node 29 is found whose result is erroneous but whose children have all correct results The user does not need to understand the computation operationally Any buggy node represents an erroneous computation step an the debugger can display the program fragment responsible for it 142 6 3 An Example 6 3 1 Starting DDT Recall the datatype nat and the functions head tail and map all defined in Chapter 2 Consider also the functions from plus and times defined as follows from nat gt nat from N N from suc N plus nat gt nat gt nat plus z Y Y plus suc X Y suc plus X Y times nat gt nat gt nat times z Y z times suc X Y plus X times X Y Should be plus Y times X Y The intended meaning of this program fragment should be clear In particular the functions plus and times are expected to compute the ad
229. otEqual X c X1 Xn Cout1 Cout addCtr X Term Cin Cout extractCtr Cin X Cout1 CX Cout X Term CX Coutl 1 G 3 2 Clauses for Computing Head Normal Forms Hnfs hnf X H Cin Cin var X var H X H hnf X H Cin Cout var X extractCtr Cin X Cout1 CX X H propagate X CX Cout1 Cout hnf c X1 Xn H Cin Cin lL H c X1 Xn hnf susp f Xi Xn R S H Cin Cout var S F X1 Xp H Cin Cout R H S hnf hnf susp E R S H Cin Cout 245 hnf R H Cin Cout G 3 3 Clauses for Function Definitions Prologrs Construction of Definitional Trees Definition G 1 Demanded positions e A position u is demanded by a rule f ti tn e lt C if f t tn has a constructor symbol at position u e A position u is demanded by a set of rules S if it is demanded by at least one rule of S e A position u is uniformly demanded by a set of rules S if it is demanded by all the rules of S Definition G 2 Call patterns e A call pattern for f is f s1 5n where 5 Sn is a linear tuple of patterns e A call pattern f s51 5n is compatible with a set of rules S if f s1 Sn matches all the left hand sides of the rules in S that is f s1 8n lt f ti tn for any F t1 tn which is a left hand side of a rule of S In the following definition we write vpos e for the set of positions in e occupied by variables Definition G 3 Definitional trees Le
230. ote that although the maximum is computed after the input modules had been generated the information in the given output delay has been propagated to the input delay domains so that whenever an input delay domain becomes empty the search branch is no longer searched and another alternative is tried Putting together the constraints about area power dissipation cost and delay is straightforward since they are orthogonal factors that can be handled in the same way In addition to the constraints shown we can further constrain the circuit generation with other factors as fan in fan out and switching function enforcement to name a few Then we could submit the following goal domain A O maxArea domain P O maxPower domain C O maxCost domain D O maxDelay genCir A P C D B S switchingFunction B sw where switchingFunction can be defined as the switching function that returns the result of a behavior B for all its input combinations and sw is the function that returns the intended result sw is referred to as a problem parameter as well as maxArea maxPower maxCost and maxDelay data functionality bool switchingFunction behavior gt functionality switchingFunction Behavior 0ut1 0ut2 0ut3 0ut4 0ut5 Dut6 0ut7 0ut8 lt 186 Behavior Behavior Behavior Behavior Behavior Behavior Behavior Behavior false false false false true true true true false false false true true f
231. pha Label LD true lt LD A B C _D E F G H I J K L M N O P Q R S T U V W X Y Z domain LD 1 26 all_different LD B A L L E T 45 C E L L 0 43 C 0 N C E R T 74 106 F L U TA E 30 F U G tU tE 50 G L trE tE 66 J A Z H Z 58 L Y R E 47 O B H O E 53 O P E R A 65 P O L K A 59 Q U HtA H R T E T 50 S A X O P H O N E 134 S H C A L HE 51 S H 0 L O 37 S O N G 61 S 0 P R A N O 82 T H E MA E 72 V I 0 H L A 1 H N 100 W A L T Z 34 labeling Label LD Solving at the command prompt is shown below Toy FD gt alpha ff L L gt 5 13 9 16 20 4 24 21 25 17 23 2 8 12 10 19 7 11 15 3 1 26 6 22 14 18 Elapsed time 9735 ms 3 3 5 Magic Series magicser toy We present another simple and well known example the magic series problem 37 Let S So 51 Sy 1 be a non empty finite serial of non negative integers As convention we number its elements from 0 The serial S is said N Magic if and only if there are s occurrences of i in S for all in 1 N 1 Below we show a possible J OY solution included in the distribution in the directory Examples in the file magicseq toy to this problem include cflpfd toy include mi
232. pile my_program cd cd wif a Next sections describe the available commands 1 5 2 Interaction with the Operating System There are three special commands for interacting with the underlying operating system q quit e or exit end the TOY session cd lt dir gt sets the directory lt dir gt as the current directory cd changes the current working directory to the distribution root where the system was installed pwd Displays the current working directory 1s Displays the contents of the working directory 1s lt dir gt Displays the contents of the given directory lt dir gt system lt comm gt submits the command lt comm gt to the operating system to the cor responding shell For example for copying a file system cp prog toy home users axterix This command allows to interact with the operating system ant it accepts any valid input at the OS command prompt In particular the command cd lt dir gt can be seen as a shorthand for system cd lt dir gt There is a shorthand for executing operating system commands Simply type comm wherever comm is not recognized as a JOY command 1 5 3 Compiling and Loading Programs The following commands are used for compiling and loading programs compile lt file gt Compiles the file lt file gt toy load lt file gt Loads the file lt file gt pl provided that lt file gt toy was compiled run lt file gt Compiles and loads the file l
233. ple we can obtain the first two solutions for the goal winMove 2 2 2 solving the goal Toy gt collectN 2 winMove 2 2 2 L gt L 109 21 2 0 2 3 Elapsed time 94 ms sol 1 more solutions y n d a y no Elapsed time O ms There is another primitive once e that returns the first reduction for the expression e For example Toy gt once winMove 2 2 2 L gt TO 2 247 Elapsed time 16 ms sol 1 more solutions y n d a y no Elapsed time O ms For more complex uses of these primitives see Appendix A 4 2 16 Constraints TOY can be described as a narrowing based functional logic language which means that the the basic operational mechanism is narrowing a combination of unification and rewriting But narrowing is not the only computational process as we see now 54 As we have explained in Section 2 6 functions in JOY programs are defined functions which are defined by means of conditional rules with local definitions of the form fti tn r EC Cm where D Dp Each condition C is a constraint of the form eo e where o can be lt lt gt or gt Well typedness of constraints implies that e and e should have the same type for the case of and and the same numeric type int or float for the case of lt lt gt or gt The reading of the program rule above is that ft t can be reduced to r if the constraints C1 Cm are satisfied using the local d
234. precedes T2 Ti A task is modelled via the type task as a 5 tuple which holds its name duration list of precedence tasks list of required resources and the start time Two functions for accessing the start time and duration of a task are provided start and duration respectively that are used by the function precedes This last function imposes the precedence constraint between two tasks The function requireList imposes the constraints for tasks requiring resources i e if two different tasks require the same resource they cannot overlap The function noOverlaps states that for two non overlapping tasks t1 and 2 either t1 precedes t2 or vice versa The main function is schedule which takes three arguments a list of tasks to be scheduled the scheduling start time and the maximum scheduling final time These last two arguments represent the time window that has to fit the scheduling The time window is imposed via domain pruning for each task s start time a task cannot start at a time so that its duration makes its end time greater than the end time of the window this is imposed with the function horizon The function scheduleTasks imposes the precedence and requirement constraints for all of the tasks in the scheduling Precedence constraints and requirement constraints are imposed by the functions precedeList and requireList respectively With this model we can declare for example a function that defines the solution to the problem
235. program to solve OGRs with N marks golomb int gt int gt bool golomb N L true lt hasLength L N NN trunc 2 N 1 1 domain L O NN append 0 _ Xn L distances L Diffs domain Diffs 1 NN all_different Diffs append D1 _ Dn Diffs Di lt Dn labeling toMinimize Xn L distances int gt int gt bool distances true distances X Ys DO true lt distancesB X Ys DO Di distances Ys D1 distancesB int gt int gt int gt int gt bool distancesB _ D D true distancesB X Y Ys Diff D1 DO true lt Diff Y X distancesB X Ys D1 DO The next goal solves a rule for N 12 marks Toy FD gt golomb 12 L L lt 0 2 6 24 29 40 43 55 68 75 76 85 TOY FD solves 10 marks OGRs in 17 seconds and 12 marks OGRs in 10 918 seconds i e about three hours in a Pentium 1 4 Ghz under Windows See 9 for performance results 188 A 7 7 Lazy Constraint Programs A very powerful characteristic of TOY FD is lazy evaluation of goals to our knowledge TOY FD is the first constraint programming language providing laziness in the solving of goals In this section we show some examples of programs that combine FD constraint solving and lazy evaluation Lazy Magic Series lazymagicser toy Now we present a lazy solution for the problem of the magic series problem that was already treated in Section 3 3 5 With this new solution we illustrate some of the e
236. programs listed in this section The program title is annotated with the correspond ing file name with extension toy A 1 Logic Programming TOY embodies all the purely declarative features of logic programming languages such as Prolog Next we show two simple examples in TOY that correspond to typical logic programs A 1 1 Peano Numbers peano toy The next program represents in TOY a logic program that generates Peano natural numbers Datatype for Peano natural numbers data nat z s nat Generator for Peano numbers isNat nat gt bool isNat z true isNat s N isNat N The main differences with the corresponding program in Prolog come from the existence of types in TOY Thus the type nat is explicitly declared by means of a data definition In the same way the type of isNat can be declared In TOY predicates are considered as functions returning 153 booleans values and in this case the type of isNat reflects that it is a predicate with a natural number as argument An example of a goal solved by this program Toy gt isNat N N gt 27 Elapsed time O ms more solutions y n d y N gt s z Elapsed time O ms more solutions y n d y N gt s s z Elapsed time O ms more solutions y n d y n The goal has infinitely many solutions although in this example the user has stopped after the first three solutions answering n to the question more solutions y To provide
237. quality conditions e es the extension of CRWL to deal with other kinds of conditions will be briefly discussed in Section F 5 CRWL can be presented as an inference system consisting of the six inference rules displayed below In each of them the premises and the conclusion are approximation statements except in the case of the inference SE where the conclusion is a strict equality condition BT Bottom PRO VR Variable XLX T Ei t ln gt tn TD Tuple Decomposition p p CREEN e tiy ads t PD Pattern Decomposition a T bn e1 gt ti En gt tn C ray apt FC Function Call k gt 0 fei enai ap gt t IF fti tn gt r HC Pl ey gt t e amp t SE Strict Equality e 2 IF t is a total pattern In all the rules t stand for possibly partial patterns while e aj stand for possibly partial expressions In rule FC the notation P refers to the set of all the possible instances of program rules where each particular instance is obtained from some function defining rule in P by some substitution of possibly partial patterns in place of variables Moreover the formulation of rule FC must be understood assumming that C includes both strict equality conditions e ez and approximation statements d s in place of the local definitions s d occurring in the defining rule This means that CRWL specifies the semantics of local definitions as a particular case of app
238. quirements Graphical I O Tcl Tk Declarative Debugger Java Runtime Environment 1 3 or higher Notice that these extra requirements are not needed for installing and running TOY but only for using the corresponding features Tcl Tk come pre installed on most nix systems as well as on Mac OS X nevertheless it can be downloaded from http www tcl tk software tcltk The Java Runtime Environment is part of most of the modern OS distributions It can be otherwise downloaded form http java com 1 2 Downloading and Running 7 OY The latest version of the system can be downloaded from http toy sourceforge net The same distribution file is valid for all the platforms After downloading the file and unzipping it the system is ready no further installation steps are needed TOY can be alternatively started as follows e From the binary distribution Move to the folder toy and depending on the OS Windows Execute toywin Linux Execute toylinux Solaris Execute toy e From the source distribution regardless of the OS 1 Move to the toy folder 2 Start SICStus Prolog 3 Type toy where is the SICStus prompt 1 3 First Steps in TOY After starting the system the following prompt is shown Toy gt At this point the system is ready to work For example using the addition predefined function and the equality predefined constraint we can submit the goal Toy gt X 3 5 The sy
239. r 3 power units With this the second approach we get a more awkward representation due to the use of suc cessor arithmetics The first approach to express this problem is indeed more declarative than the second one but we get non termination FD constraints can be profitably applied to the representation of this problem as we show in the next example Simple Circuits with FD Constraints circuitFD pl As for any constraint problem modelling can be started by identifying the FD constraint vari ables Recalling the problem specification circuit limitations refer to area power dissipation cost and delay Provided we can choose finite units to represent these factors we choose them as problem variables A circuit can therefore be represented by the 4 tuple state area power cost delay The idea to formulate the problem consists of attaching this state to an ongoing circuit so that state variables reflect the current state of the circuit during its generation By contrast with the first example we do not generate and then test but we test when generating so that we can find failure in advance A domain variable has a domain attached indicating the set of possible assignments to the variable This domain can be reduced during the computa tion Since domain variables are constrained by limiting factors during the generation of the 184 circuit a domain may become empty This event prunes the search space avoiding
240. r C2 Then we can submit the goal power B P P lt maxPower provided the function maxPower acts as a problem parameter that returns just the maximum power allowed for the circuit in which the function power is used as a behavior generator As outcome we get several solutions B 10 P 0 B i1 P 0 B i2 P 0 2Equivalently and more concisely power B lt maxPower could be submitted but doing so we make the power unobservable 183 B not 1i0 P 1 acid B not not i0 P 2 Declaratively it is fine but our operational semantics requires a head normal form for the application of the arithmetic operand This implies that we reach no more solutions beyond not not i0 because the application of the fourth rule of power yields to an infinite computation This drawback is solved by resorting to Peano s arithmetics that is data nat z s nat plus nat gt nat gt nat plus z Y Y plus s X Y s plus X Y less nat gt nat gt bool less s X s Y less X Y less z s X true power behavior gt nat power i0 z power il z power 12 z power notGate C plus notGatePower power C power andGate C1 C2 plus andGatePower plus power C1 power C2 power orGate C1 C2 plus orGatePower plus power C1 power C2 So we can submit the goal less power P s s s z where we have written down explicitly the maximum powe
241. r0f lisa molly true motherOf alan rose true motherOf dolly rose true motherOf jim sally true motherOf alice sally true 36 parentOf predicate parentOf X Y holds if Y is parent of X parentOf person person gt bool parentOf X Y fatherOf X Y parentOf X Y motherOf X Y ancestorOf predicate ancestorOf X Y holds if Y is ancestor of X ancestorOf person person gt bool ancestor0f X Y parentOf X Y ancestorOf X Y parentOf X Z ancestorOf Z Y As another syntactic facility JO allows defining rules whose left hand sides are not linear Such rules are understood as a shorthand for the result of transforming them as follows repeated occurrences of a variable X say in the left hand side are replaced by fresh variables X and new conditions X X are added This facility is very helpful for writing predicate definitions in clausal notation For instance a Prolog like definition of the well known permutation sort algorithm could include the following clauses permutationSort real gt real gt bool permutationSort Xs Ys permutation Xs Ys sorted Ys permutation A gt A gt bool permutation true permutation X Xs Zs permutation Xs Ys insertion X Ys Zs insertion A gt A gt A gt bool insertion X x true insertion X Y Ys X Y Ys true insertion X Y Ys Y Zs insertion X Ys Zs
242. re the first component is used to store the accumulated value an integer and the second component stores the arithmetic operations pending to be executed When the button is clicked on the function stored in the second component will be applied to the first component in order to get the result The TOY code for the calculator is the following type calcState varmut int int gt int calculator io unit calculator do St lt newVar 0 id runWidget calculator calc_GUI St calc_GUI calcState gt tkWidget io unit calc_GUI St tkCol tkEntry tkRef Display tkText 0 tkRow map cbutton St Display 1 2 3 tkRow map cbutton St Display 4 5 6 tkRow map cbutton St Display 7 8 9 tkRow map cbutton St Display C 0 cbutton calcState gt tkRefType gt string gt tkWidget io unit cbutton St Display C tkButton button_pressed St Display C tkText C button_pressed calcState gt tkRefType gt string gt channel gt io unit button_pressed St Display C Ch if digit C then do Acu lt readVar St FC lt return 10 fst Acu strToint C writeVar FC snd Acu St tkSetValue Display intTostr FC Ch else if C then do Acu lt readVar St F lt return snd Acu fst Acu 137 writeVar F id St tkSetValue Display intTostr F Ch else if C C then do writeVar 0 id
243. ridge this allows only binding Additionally constraints can be propagate to other solver a FD constraint can be propagate to R solver and viceversa Propagation is enabled by means of the command prop and disabled with noprop 4 2 The Constraint Cooperation Bridge Bridge is a constraint of the form u v where u and v are variables with integer and real types respectively Furthermore u and v are constrained to take the same integer value 2 e Type Declaration int gt float bool e Modes dinout gt inout inout e Reifiable Yes e Examples Toy R FD gt X RX domain X 2 4 RX lt 3 4 X RX RX lt 3 4 X in 2 4 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms 4 3 Binding As cooperation mechanism binding instantiates a variable occurring at one end of a bridge whenever the other end of the bridge becomes a numeric value For example next goals unify RX with the real value 2 first goal and X with the integer value 2 second goal Toy R FD gt X RX X X gt 2 RX gt 2 110 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms Toy R FD gt X RX RX X gt 2 RX gt 2 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms 4 4 Propagation Propagation takes place whenever a constraint is submitted to the FD or R solver At that mo
244. rived from P in the Constructor based ReWriting Logic CRWL presented in the next section In the case of pure logic programs CRWL behaves just as Horn Logic As seen from the examples in this motivating section the logical meaning of TOY 235 programs given by CRWL lacks information on computed answers In a way this is a limitation Note however that any semantics which provides information on computed answers must be more dependent on some particular operational model for goal solving CRWL semantics is more abstract in this sense and still useful for various purposes as e g investigating the completeness of goal solving methods see 11 13 or designing provably correct declarative debugging tools like those described in Chapter 6 F 2 A Constructor Based Rewriting Logic As explained in the previous section the main aim of CRWL is to derive atomic facts from a program However due to the occurrence of nested function calls in defining rules see Section 2 6 CRWL must be able to derive more general facts of the form e t where t is a possibly partial pattern and e is a possibly partial expression These facts are called approximation statements The abstract syntax for partial expressions is like the one introduced for expressions in Section 2 1 extended to allow occurrences of 1 Moreover due to the occurrence of conditions in defining rules CRWL must also be able to derive conditions For the moment we consider only strict e
245. rns E C gt nat E For the right hand side the call 232 T true A T returns bool and the types inferred for the left hand side and the right hand i e E and bool are unified Finally we obtain T even nat gt bool odd D For the second rule even suc X odd X the initial environment O X F is created From the expression suc X the type nat is inferred for X The type of the left hand side inferred from I is bool Regarding the right hand side the call T odd X A T 0 unifies through recursive calls the type D asssumed for odd in I with nat G returning G as the type for odd X Then by unification of types of the left hand side and the right hand side we obtain odd nat bool This yields T even nat bool odd nat bool The two rules for odd do not supply new information about the type annotations in I and do not produce any error Finally the algorithm contrasts the inferred types for even and odd with the declared types that are identical in this case The types for the first block are now inferred and we can update A obtaining A Ao U even nat gt bool odd nat bool For the second block IstEven the initial environment is T istEven H From the first program rule we obtain lstEven I bool where the variable I is obtained by renaming the type A taken from A Then checking the condition even X true leads to
246. roximation statements 236 A derivation in CRWL can be presented as a finite sequence of statements y 0 lt i lt n such that each statement y 0 lt i lt n follows from some other statements pz i lt j lt n by means of some CRWL inference rule A statement y is called CRWL provable from a program P in symbols P Fcrwz iff there is some CRWL derivation such that yo is p using only rule instances from the set P at the FC steps The declarative semantics of a TOY program P is modelled by the set of all atomic facts ft ty gt t such that P Horwz f ti tn gt t For example assume any program P including the defining rules for coin and coins given in Section 2 12 Then P Forw coins gt 0 1 is proved by the following CRWL derivation 0 coins 0 1 1 by FC 1 1 coin coins 0 1 L by PD 2 3 2 coin 0 by FC 4 3 coins 1 1 by FC 5 4 0 gt 0 by PD 5 coin coins gt 1 1 by PD 6 7 6 coin 1 by FC 8 7 coins gt L by BT 8 1 1 by PD Note that all the CRWL inference rules with the exception of FC are program independent In particular the rules BT VR TD and PD essentially specify the semantic ordering Con sidering the empty program and any approximation statement t t where t and t are both patterns it is easy to check that Forw t t holds if and only if t E t Some other technical properties of CRWL can be found in 11 13 F 3 Correctness of Compute
247. rsion 2 2 2 Launched on March 2006 H 4 Version 2 2 1 Launched on November 2005 o H 5 Version 2 2 0 Launched on August 2005 o H 6 Version 2 1 0 Launched on May 2005 o e o 196 196 204 206 216 216 219 227 227 228 234 234 236 237 238 239 H 7 Version 2 0 Launched on February 2002 I Known Bugs Preface TOY is a multiparadigm programming language and system designed to support the main declarative programming styles and their combination Programs in TOY can include definitions of lazy functions in Haskell style as well as definitions of predicates in Prolog style Both functions and predicates must be well typed with respect to a polymorphic type system Moreover J OY programs can use constraints in CLP style within the definitions of both predicates and functions The constraints supported by the system include symbolic equations and disequations linear arithmetic constraints over the real numbers and finite domain constraints Computations in TOY solve goals by means of a demand driven lazy narrowing strategy first proposed in 22 and closely related to the needed narrowing strategy independently introduced in 1 This computation model subsumes both lazy evaluation and SLD resolution as particular cases For TOY programs using constraints demand driven lazy narrowing is combined with constraint solving and c
248. rwise it returns false Reifiable Not applied 94 e Example Toy FD gt empty_interval 0 1 B1 empty_interval 1 0 B2 Bi gt false B2 gt true Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms fdset_to_interval 2 interval_to_fdset 2 e Type Declaration fdset_to_interval fdset int int interval_to_fdset int int fdset e Modes fdset_to_interval in inout inout interval_to_fdset in in gt inout e Definition fdset_to_interval S returns a tuple which is the non empty interval Min Max interval_to_fdset Min Max is the inverse operation of fdset_to_interval e Reifiable Not applied e Example Toy FD gt fdset_to_interval interval 0 1 Min Max interval_to_fdset 0 1 Min gt 0 Max gt 1 S gt interval 0 1 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms fdset_singleton 2 e Type Declaration fdset_singleton fdset int bool e Modes fdset_singleton in inout inout inout in inout 95 e Definition fdset_singleton S E returns true if the FD set S only contains the element E Otherwise it returns false e Reifiable Not applied e Examples Toy FD gt fdset_singleton S 1 B S gt interval 1 1 B gt true Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time
249. s Toy gt card X Y X Z Y gt X Z gt X N gt 1 Elapsed time O ms more solutions y n d y Y gt X N gt 2 X Z Elapsed time O ms more solutions y n d y Z gt Y N gt 2 Y X Elapsed time O ms more solutions y n d y Z gt X N gt 2 X Y Elapsed time O ms more solutions y n d y N gt 3 X Z X Y Y Z Elapsed time O ms more solutions y n d y no Elapsed time O ms A 6 Programming with Real Constraints In order to compile real constraint programs in JOY the user must first activate the constraint solver over reals by means of the command cflpr Recall the explanations in Section 1 5 5 168 A 6 1 Defining Regions of the Plane regions toy The program below shows the usefulness of using functions with arithmetic constraints over real numbers It contains some stuff for dealing with regions subsets of the plane Regions are sets of points represented by their characteristic function see the type region below This is a typical approach in functional programming However the novelty is that constraints provide a much more flexible way of using and defining functions include misc toy type point real real type region point gt bool infixr 50 lt lt lt lt point gt region gt bool P lt lt R RP rectangle point gt point gt region rectangle A B
250. s H Cin Cout g s H Cin Cout gm 5 H Cin Cout U prolog dt1 91 U prolog dtm gm where g1 gm are new function symbols e prolog f s gt try e1 Ci em amp Cm 9 g s H Cin Cout solve C1 Cin Cout1 hn f e1 H Coutl Cout g 5 H Cin Cout solve Cm Cin Cout1 hn f em H Coutl Cout y 248 Appendix H Release Notes History This chapter lists in reverse chronological order the release notes history from the first maintained versioning system Toy system version 2 0 February 2002 H 1 Version 2 3 Launched on December 2006 Enhancements e communication function bridge has beed added int gt real gt bool e The libraries CLP R and CLP FD can be activated together Implementation of the propagation for the cooperation between the real and finite domain solvers see 4 e New commands prop Enables propagation noprop Disables propagation e More examples have been added examples Uncataloged examples New chapter in the manual hapter 4 Cooperation of Solvers Deprecations Changes Fixed Bugs 249 H 2 Version 2 2 3 Launched on July 2006 Enhancements e Optimization functions have beed added to the library CFLPR minimize maximize real gt real for linear optimization bb_minimize bb_maximize real gt real gt real for linear optimization with integral constraints e When the library CLP R
251. s ei 1 lt i lt n the function call f e1 en can return results of type 7 provided that the logic variables introduced during the computation as fresh renamings of extra variables in right hand sides are bound to values of the expected types The TOY system always leaves logic variables unbound until some bindings are demanded by the rest of the current computation This ensures a well typed behaviour except in some special cases to be discussed at the end of Section 2 14 2 13 Goals and Computed Answers In the preceding section we have already met some examples of goals and answers In general there are two different modes of computing in TOY solving goals and evaluating expressions For the first modality a goal is a set of conditions C1 Cn where as in function definitions each condition C must have the form e e2 being gt lt gt lt gt and e1 e2 42 expressions Each condition C is interpreted as a constraint to solve using the definitions of functions and predicates included in the current program as well as the intended meanings of lt gt lt gt which have been explained in Section 2 6 More precisely goal solving in JOY involves a combination of lazy evaluation and computation of bindings for logic variables see Appendix G for a more formal specification Whenever a goal is satisfiable the system answers yes and shows the computed answer consisting of a set of constrain
252. s sections and partial applications see Section 2 2 are the two main tools available for expressing the computation of functional values 2 8 Primitive and Predefined Functions TOY has a number of primitive functions which are not defined by means of defining rules Their definitions are included in a special system file called basic toy Currently the primitive functions supported by the system are min max real gt real gt real real gt int gt real log real gt real gt real div mod gcd int gt int gt int round trunc floor ceiling real gt int toReal int gt real uminus abs sqrt ln exp sin cos tan cot asin acos atan acot sinh cosh tanh coth asinh acosh atanh acoth real gt real lt lt real gt real gt bool A gt A gt bool Tables 2 1 and 2 2 show the intended meaning for each one of the primitive functions As we have remarked already in Section 2 6 the symbols gt lt gt lt have a double role they can be used to build conditions in defining rules and also as operators denoting functions which return a boolean result Both r les can be distinguished by the context As we will see in Section 2 16 they are conceptually different and not to be confused A natural relation between the two roles of strict equality and disequality is shown by the following defin
253. s y n d a y no Elapsed time O ms Toy R FD gt X RX X lt Y X RX Y _D RX _D lt 0 0 Y gt X Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms In the last goal a new bridge is created for the variable Y ti to gt t3 analogously t to gt t3 was explained in section 4 4 t and t2 can be either integer constants or else a integer variables but one of this must be a variable so that the propagation is possible e Creation of Bridges If t and or tz are variables X and Y and they have no bridges then X RX and or Y RY are created with RX and or RX new If t or ta are variables then t3 is a new variable Z and a bridge Z RZ is buildt for Z with RZ also new e Propagation Constraint Afterwards the constraint RX RY RZ is buildt as mate constraint e Example Toy R FD gt X RX Y RY X Y lt 2 X RX Y RY _E _F _F lt 2 0 RY RX _F 114 X Y _E E in inf 1 gt Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms Toy R FD gt X RX 5 X lt 10 X RX _C _D RX lt 5 0 _D 5 0 RX 5 X _C X in inf 4 _C in inf 9 Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms In the first goal new variable _E links with result of X Y New bridge _E _F is created with the new real variab
254. s for the cartesian product of the types T1 Tn while a functional type of the form T gt T stands for the type of all functions which can be applied to arguments of type 7 and return results of type T Syntactically gt behaves as a predefined binary type constructor written in infix notation Following common practice we assume that gt associates to the right and omit parentheses accordingly For instance the type Cint gt bool gt int gt int gt int gt int can be abbreviated as int gt bool gt int gt int gt int gt int The notation e 7 is used to indicate that expression e has type 7 For instance some typing rules have the following form IF e 7 foralll1 lt i lt nTHEN e en Ti Tn IFe i n gt rande n THEN ce 7 Using these and other rules the type inference algorithm described in Appendix E can decide whether a given expression e is well typed In the positive case the algorithm computes the most general type T of e also called principal type along with a set TA of type assumptions X Tx for the variables X occurring in e such that e 7 follows from the assumptions in TA and the type inference rules For instance given the expression X not Y involving two boolean operations the type inference algorithm computes X not Y bool under the assumptions X bool Y bool The type inference algorithm also checks whether the function definiti
255. s with a closed bracket Each sentence can be either an include a datatype definition a type synonym definition an operator definition a function type declaration or a function defining rule For instance the following is a valid program text in TOY include misc toy real gt real gt real X Y zipWith X Y lt length X length Y Different sentences belonging to the same level must be separated by semicolons The layout rule allows to omit the symbols and replacing them by certain natural layout conventions Briefly the layout rule specifies e Before reading the first character of each section an open bracket is inserted automatically e The end of the section is reached when the only open bracket is the one described in the previous item and the first character of the current line is found at some column position less or equal than the column position occupied by the section s first character e If the first character of the current line is at the same column position as the first character of the innermost level of opened brackets and this level is strictly greater than one a semicolon is inserted before e A closed bracket will also be inserted wherever an unknown token is found e Empty lines as well as lines containing only blank spaces tabulators and comments are ignored by the layout rule That is they are handled just l
256. s with overlapping left hand sides For instance the following JOY definitions compute ancestors by means of non deterministic functions Functions fatherOf and motherOf fatherOf person gt person fatherOf peter john fatherOf paul john fatherOf sally john father0f bob peter fatherOf lisa peter fatherOf alan paul father0f dolly paul fatherOf jim tom fatherOf alice tom motherOf person gt person motherOf peter mary motherOf paul mary motherOf sally mary motherOf bob molly motherOf lisa molly motherOf alan rose motherOf dolly rose motherOf jim sally motherOf alice sally Non deterministic functions parentOf and ancestorOf parentOf person gt person parentOf X gt fatherOf X parentOf X gt motherOf X 38 ancestorOf person gt person ancestorOf X gt parentOf X ancestorOf X gt ancestorOf parentOf X As in this example definitions of non deterministic functions use the sign gt gt in place of More precisely programmers are expected to use rather than gt to indicate that a particular function is deterministic Determinism is an undecidable semantic property There are sufficient conditions for determinism that can be decided efficiently see 11 The current system however does not check wether the functions defined by
257. scfd toy magic int gt int gt labelingType gt bool magic N L Label true lt hasLength L N domain L 0 N 1 constrain L L 0 Cs sum L N redundant 1 scalar_product Cs L N redundant 2 107 labeling Label L constrain int gt int gt int gt int gt bool constrain A B true constrain X Xs L I _ I S2 true lt count I L X constrain Xs L I 1 S82 Below we show an example goal Toy FD gt magic 10 L L gt 6 2 1 O O O 1 0 0 0 1 Elapsed time 31 ms sol 1 more solutions y n d a y no Elapsed time O ms 108 Chapter 4 Cooperation of Solvers In this chapter we present the cooperation of solvers Cooperation is based on the commu nication between the FD and R solvers by means of special communication constraint called bridge Bridges are used for two purposes namely binding and propagation Solver cooperation is allowed with binding alone or both binding and propagation 4 1 Introduction CFLP goal solving takes care of evaluating calls to program defined functions by means of lazy narrowing and decomposing hybrid constraints by introducing new local variables Eventually pure FD and R constraints arise which must be submitted to the respective solvers Cooperation of solvers is based on the communication between the FD and R solvers by means of special communication constraints called bridges A bridge u v constrai
258. se insert D K combine C C lt C lookup D K deletekey D K delete D lookup empty K default lookup D K if keq K K then C K default else if kle K kK then lookup left D K else lookup right D K lt D empty K C root D Y MULTISET AS DICTIONARY module multiset parameters type elt le eq elt gt elt imports nat exporting all gt bool dictionary type key to elt type contents op kle to le op keq to eq op default to op combine to exports type multiset elt empty_ms multiset elt add_one multiset elt to nat elt gt multiset elt 214 add_many multiset elt gt elt gt nat gt multiset elt mult multiset elt gt elt gt nat delete_one multiset elt gt elt gt multiset elt delete_all multiset elt gt elt gt multiset elt body type multiset elt dict elt nat empty_ms empty add_one MS E insertcont MS E s z add_many MS E N insertcont MS E N mult MS E lookup MS E delete_all MS E deletekey MS E if s z lt N then add_many MS N s z else MS lt mult MS E MS delete_all MS E delete_one MS E 215 Appendix D Syntax In this appendix the lexicon and grammar of the language are presented D 1 Lexicon First we describe the set of tokens allowed in the language as well as the reserved words and operations A token must belong to one of the fo
259. se they represent functions When comparing patterns J OY relies on syntactic equality For instance the two patterns twice times 2 and times 4 are regarded as different although they behave in the same way as functions Therefore the representation of functional values as patterns in TOY is intensional rather than extensional As a consequence pattern unification has the same behaviour and complexity as syntactic unification of terms in Prolog 2 2 Types TOY is a typed programming language based essentially on the Damas Milner polymorphic type system 7 Programs are tested for well typedness at compile time by means of a type inference algorithm see Appendix E In particular each occurrence of an expression in a TOY program has a type that can be determined at compile time Syntactically types are built from type variables and type constructors Any identifier starting with an uppercase letter can be used as a type variable while identifiers for type constructors must start with a lowercase letter Type constructors are introduced in datatype declarations along with data constructors see Section 2 3 Primitive types such as bool and int see Section 2 4 can be viewed as type 19 constructors of arity 0 Assuming the abstract notation A B for type variables and 6 TC for type constructors of arity n the syntax of TOY types can be defined as follows Tu A T 0 ETOC a 7 Ti gt 7T Here 71 7n stand
260. section getLine io string getLine do C lt getChar if C n then return else do Cs lt getLine return C Cs read_3_chars io unit read_3_chars do C1 lt getChar C2 lt getChar C3 lt getChar putChar C1 gt gt putChar C2 gt gt putChar C3 In general a do construction has the form do Cy lt pi C2 lt p2 Ck lt Pk 3 r where C 1 lt i lt k are pairwise distinct variables and p are expressions of type io 7 for some types Ti Each C only can be used after its definition i e C can appear in p only if j gt i If p is an expression of type io 7 then the type of C is 7 In the particular case 7 unit Ci does not need to be used by any other p and C lt p can be abbreviated to p Finally r is an expression of type io 7 which is also the type of the entire do expression The above do construction has also a declarative meaning because it is equivalent to the fol lowing combinations of the operator gt gt 128 p gt gt conti cont Cy po gt gt conta C conta Cy Ca pz gt gt cont3 C Co contz_1 Cy Co Cx 1 pe gt gt cont Cy Co Ch 1 cont Ci Co Ck r 5 4 Files File names are values of type path where type path string There are two standard functions which operate on text files These functions are readFile path gt io string writeFile path gt string gt io unit Functi
261. sistency of such bindings at run time As an additional disadvantage guessing bindings for higher order variables generally leads to the exploration of a huge search space and often even to non termination A second kind of problem can arise when solving goals of the form f e1 em f en where f is a defined function of arity n gt m Such a goal must be solved by decomposing it into m new subgoals e e m l Assume that the principal type of f is T gt gt Tn gt T such that some type variable occurring in 7 for some 1 lt lt m does not occur in Tm 1 gt gt Tn gt T If this is the case some of the m new subgoals e e may be ill typed This problem is called opaque decomposition the name points to the fact that the type of f e em does not uniquely determine the types of the argument expressions ej For example using a function snd A gt B gt B snd X Y Y as well as other functions presented in previous examples one can build the well typed goal snd head Xs true snd head Ys 15 where both sides of the strict equality have type B gt B under the type assumptions Xs bool Ys int In order to solve this goal TOY starts with an opaque decomposition step leading to the new goal head Xs true head Ys 1 which is ill typed In spite of this TOY can succesfully complete a computation which returns the ill typed solution Xs Ys 50
262. sses are often suspended until the evaluation of certain expression is required by other process In these cases lazy evaluation corresponds to particular coroutines for the processes One interesting application is to solve the communication between a client and a server with the Input Output model via Streams If the client generates requests from one initial requirement the server will generate answers that will be again processed by the client and so on For simplicity we consider that requests and answers are integer numbers This process network can be clearly defined in TOY FD with recursive definitions as follows requests answers int 159 requests client initial answers answers server requests Suppose now that the client returns the request and generates a new one i e a next one from the first answer of the server and that the server processes each request to generate a new answer This is defined in ZOY FD as follows client int gt int gt int client Ini RIRs Ini client next R Rs server int gt int server P Ps process P server Ps The architecture is completed by defining adequately the initial requirement the processing function and the selection of the next request As an example and for simplicity we can define them as follows process int gt int process 3 initial int initial 4 next int gt int next id Idempotence Note that this is
263. stem solves the goal producing the following computed answer Toy gt X 3 5 X gt 8 Elapsed time O ms sol 1 more solutions y n d a y meaning that the replacement of the variable X by 8 in the goal expression satisfies the goal At this stage TOY informs that it has found a solution and asks whether the user does y or does not n require the next solution asks for a debugging session d or requires all the pending solutions a y is the default request so that typing Intro is equivalent to request the next solution Notice that the symbol is used instead of in order to distinguish the syntactical strict equality from the function definition operator respectively Goals and computed answers are discussed in Section 2 13 pg 42 but at the moment we can introduce some initial concepts e X isa logical variable represented in TOY by identifiers starting with an uppercase letter e The symbol stands for the predefined strict equality constraint e In order to solve a goal e e2 the system will look for values of the variables occurring in the expressions e 1 e2 such that both can be reduced to the same pattern The notions of expressions and patterns are introduced more formally in Section 2 1 pg 18 Now type n standing for no to indicate that we do not need more solutions for the goal In fact there are no more solutions so typing y yes will have the same effect The answer d debug is used to ind
264. string writeWish channel gt string gt io unit closeWish channel gt io unit The execution of the expression openWish Title opens a Tcl Tk window with title Title and returns a bidirectional communication channel After executing this command the operations 131 readWish and writeWish allow communication with the new window by means of the returned channel The action writeWish Channel Str writes the string Str which must be a well formed Tcl Tk command in the channel Channel whereas readWish Channel returns the string read from the channel Channel The communication between the Tcl Tk window and TOY may be closed by executing the command closeWish Channel As a first simple example consider the following Hello World program hello_world io unit hello_world do Ch lt openWish Hello World writeWish Ch button butExit text Exit command puts e writeWish Ch pack butExit Str lt readWish Ch closeWish Ch The execution of the expression gt hello_world opens the window below in such a way that a click on the button closes the window Hello World o ox As a second example here we have an extension of the program above In this version one more button has been added whose associated command has as effect to write Hello World in the standard output The TOY code of the program is hello_world2 io unit hello_world2 do Ch lt openWish Hello World writeWish Ch
265. sts 2 returns the intersection of its two input ordered integer lists allowing infinite lists intersectOrdIntLists int gt int gt int intersectOrdIntLists 204 L intersectOrdIntLists X Xs intersectOrdIntLists X Xs Y Ys if X lt Y then intersectOrdIntLists Xs YIYs else if X gt Y then intersectOrdIntLists X Xs Ys else X intersectOrdIntLists Xs Ys 205 Appendix C Sample Modules Y NATURAL NUMBERS module nat exports data nat z nat nat nat lt nat gt nat lt nat mx nat mn nat even nat odd nat dv nat md nat dv and md are body Z N M s M N Z N z s M N z N 2z s M z s M s N M s nat gt nat gt gt nat gt gt nat gt gt nat gt gt nat gt gt nat gt gt nat gt gt nat gt gt bool gt bool gt nat gt gt nat gt s M N nat nat nat bool bool bool nat nat nat nat only defined for non zero second argument Mx N N sM z lt N true s M lt z false N 206 s M lt s N M lt N M lt z false z lt s N true s M lt s N M lt N N gt M M lt N mn NM if M gt N then N else M mx NM if M gt N then M else N even z true even s M odd M odd z false odd s M even M N dv P if P gt
266. t RY YH RY a gt Y with aeR RX gt RY X RX and Y RY X gt Y RX gt a X RX X4 gt a with aeR a gt RY YH RY a gt Ywith acR tit te t3 analo t3 is a new variable RX3 with iP 172 gt ig For 1 lt i lt 2 either gously for no bridge X3 RX3 is cre t is an integer constant n and we is n ated with X3 new For 1 lt i lt 2 t or else t is a variable RX where X is either an integer constant or a RX and ie is X variable RX with bridge X RX t tg gt t3 as previous case FP Hx ig ie For 1 lt i lt 3 is determined as in the previous case Table 4 2 Propagations from R to FD Y RY RX RY lt 0 0 Y gt X Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms Goal below not propagates the constraint RX lt RY since there is not bride for the real variable RX Toy R FD gt X RX RX lt RY X RX RY RX gt 0 0 Elapsed time O ms sol 1 more solutions y n d a y no 116 Elapsed time O ms RX lt a analogously w r t Table 4 2 RX lt a RX gt a RX gt a e Checking Bridges X RX e Propagation Constraint Afterwards the constraints X lt a is buildt as mate con straints and submitted to the finite domain solver e Example Toy R FD gt X RX RX lt 2 3 X RX RX lt 2 3 X in inf 2 Elapsed time O ms sol 1 more solutions y n d a y
267. t f FS be a function symbol defined by a set of rules Ry in a program P Then o def dt f X1 Xn Rf e Let S be a nonempty subset of Ry and pat a call pattern for f compatible with S The defi nitional tree for pat corresponding to S written dt pat S is defined recursively according to the following cases exactly must hold and the second case involves a non deterministic choice 1 Some position in vpos pat is uniformly demanded by S Let u be one of them non determinism X the variable in pat at u C1 Cm the constructor symbols at u in the rules of S Si 1RESI R has c atu 1 m pat patlu c Uz Uy ci DC Uy Uj news Then dt pat S pat gt case X of c dt pat S1 Cm dt patm Sm 246 2 Some position in vpos pat is demanded by S but no one is uniformly demanded Let wi Um the demanded positions in any order non determinism Su RE S R demands u1 Qi S Su Sus R Q R demands u2 Q2 Qi Sus Sum R E Qm 1 R demands um So Qm 1 Su if So it is ignored Then dt pat S pat gt or dt pat So dt pat Su dt pat Sum 3 No position in vpos pat is demanded by S therefore since pat is compatible with S the left handsides of S are variants of pat Let R pat e EC Rn pat en Cn be variants of the rules of S Then dt pat S pat gt try ey Ci 9 Ca EA Prolog Code associat
268. t file gt toy cut Enables compilation with dynamic cut optimization nocut Disables compilation with dynamic cut optimization 13 1 5 4 Information about Programs TOY provides two commands for obtaining information about functions and predicates defined in a program The first one displays the type of an expression without evaluating it e type lt ezpr gt Shows the type of the expression lt expr gt according to the definitions of the current session Consider the following examples Toy gt type div div int gt int gt int Elapsed time O ms Toy gt type 1 int 1 real Elapsed time O ms Toy gt type 1 2 int 1 int 2 real Elapsed time O ms Toy gt type 1 2 3 int 1 int 2 int 3 bool Elapsed time O ms Toy gt type Line 1 Error 11 Error in expresion Unexpected operator Toy gt type real gt real gt real Elapsed time O ms Note that because associativity we have to type parentheses enclosing operators in order to determine their types as illustrated in the last example above e tot Enables totality constraints as part of the system answers e notot Disables totality constraints as part of the system answers e tree lt filename gt lt fun gt This command is useful only for experienced users with knowl edge about the evaluation strategy used by TOY and it shows the definitional tree 22 of the function lt fun gt in the file lt filena
269. t variable of the widget referenced by the first argument 135 e tkSetValue tkRefType gt string gt channel gt io unit sets the value a string of the text variable of the widget referenced by the first argument e tkUpdate string gt string gt tkRefType gt channel gt io unit updates the value of the text variable of the widget referenced by the second argument with respect to the update function given by the first argument e tkConfig tkRefType gt tkConfItem A gt channel gt io unit changes the configuration except for commands of the widget e tkFocus tkRefType gt channel gt io unit sets the input focus of the GUI given by the second argument to the widget referenced by the first argument e tkAddCanvas tkRefType gt tkCanvasItem gt channel gt io unit adds a list of canvas items to the canvas referenced by the first argument In the following example we illustrate the use of some of the functions above counter tkWidget io unit counter tkCol tkEntry tkRef Val tkText 0 tkRow tkButton tkUpdate incrText Val tkText Increment tkButton tkSetValue Val 0 tkText Reset tkButton tkExit tkText Stop incrText string gt string incrText Cs intTostr strToint Cs 1 The evaluation of the expression gt runWidget Counter Demo counter generates the follow ing window in which the button Increment has been pressed seven t
270. taTypeRhs Type alias declaration typeAliasDecl type typeld varld type Function type declaration funTypeDecl function ry function type FUNCTION AND CLAUSE DEFINITIONS Function rule declaration funDecl rulet Function defining rule rule ruleLhs gt expr conditionDecls whereDecls Predicate clause similar to Prolog but possibly with where declarations and not ending in clauseDecl gt ruleLhs conditionDecls whereDecls Right hand side both for program rules and for clauses ruleLhs function fPat infixOpLhs infixOpLhs fPat funOp fPat fPat funOp fPat fPat Conditional part of a function rule or predicate clause conditionDecls lt expr 7 7expr Where declarations the lhs must be a linear pattern An patBinding patBinding Ww whereDecls where patBinding pattern expr TYPES 222 type cType gt cType Types without any external occurrence of gt cType typeld simpleTypet simpleType Simple Types simpleType typeld varld listType tupleType type list Type gt ft type i gt type m type
271. tance map is a better choice than mapRel in case that a potentially infinite list must be processed More precisely the attempt to solve a mapRel goal involving an infinite list will not terminate while expressions of the form take n map fun list can be lazily evaluated even if the value of list turns out to be infinite Recall the definition of function take from Section 2 6 A special feature of higher order programming in TOY is the availability of higher order pat terns This notion has already been introduced in Section 2 1 as a syntactic device to represent functional values Higher order patterns behave as intensional representations of functions They can be compared for strict equality and disequality in the same way as first order data terms In actual programs higher order patterns can play a useful r le both as patterns occurring in the left hand sides of defining rules and as computed results In order to illustrate this idea let us consider family relationships modelled as non deterministic functions of type person gt person as we have seen in Section 2 12 It is natural to think of complex family relationships being built as the functional composition of basic relationships such as fatherOf and motherOf 48 Using the composition operator defined at the beginning of this section higher order pred icates which recognize both basic and composite family relationships are easy to define The auxiliary type a
272. tance the inverse of inserting an element in a list consists of removing such element Toy gt inverse insert 3 4 5 3 X X gt 4 5 1 Elapsed time O ms more solutions y n d y no Elapsed time O ms Of course if function F is not injective then inverse F will behave as a non deterministic function A 4 Programming with Failure A 4 1 Default Rules automata toy An interesting use of failure in functional logic programming is to express default rules These rules are implicit in functional systems like Haskell where pattern matching determines the rule to apply for reducing a call to a function the n th rule only applies if pattern matching fails for the previous n 1 rules As an example consider the following function f 0 fX 1 If we evaluate the expression f O in Haskell we get the result 0 by the first rule Here the second rule is working as a default rule as it only applies if the previous fail in pattern matching In contrast if we submit the corresponding goal f 0 X in TOY we obtain the answers X 0 and X 1 due to non determinism Nevertheless it may be usefull in some cases to have in TOY the behaviour of Haskell and this is possible by using fails 162 Oat X X 1 lt fails f X 0 0 Hh Hh Fh It is easy to check that with this definition f 0 X produces only the answer X 0 and for example f 2 X gets X 1 This scheme of transformation is applicable in the gen
273. the identifier of a machine m a resource needed for performing task tX So Figure A 3 Precedence Graph The following program included in the distribution in the directory Examples in the file scheduling toy models the posed scheduling problem Observe in the syntax that function arguments are not enclosed in parentheses to allow higher order applications Also syntactic sugar is provided for expressing Boolean functions la Prolog The rules that define a function follow its type declaration The type declaration consists of the types for each argument and for the result separated by gt Lists adhere to the syntax as Prolog lists and int is a predefined type for the integers Note also functional applications in arguments such as End D in the second rule defining horizon Logic Variables start with uppercase whereas the remaining symbols start with lowercase Adapted from 27 178 include cflpfd toy include misc toy data taskName t1 t2 t3 t4 t5 t6 data resourceName mi m2 type durationType int type startType int type precedencesType taskName type resourcesType resourceName type task taskName durationType precedencesType resourcesType startType start task gt int start Name Duration Precedences Resources Start Start duration task gt int duration Name Duration Precedences Resources Start Duration schedule task gt int gt int gt
274. the output delay This solution is depicted in the following function genCirDelay state gt delay gt circuit genCirDelay A P C D Dout i0 A P C D genCirDelay A P C D Dout i1 A P C D genCirDelay A P C D Dout i2 A P C D genCirDelay A P C D Dout notGate B A P C D lt domain Dout fd_min Dout notGateDelay fd_max Dout genCirDelay A P C D Dout B A P C D genCirDelay A P C D Dout andGate B1 B2 A P C D lt domain Din1 Din2 fd_min Dout andGateDelay fd_max Dout genCirDelay A P C D Dini B1 A P C D genCirDelay A P C D Din2 B2 A P C D domain Dout maximum fd_min Din1 fd_min Din2 fd_max Dout genCirDelay A P C D Dout orGate B1 B2 A P C D lt domain Din1 Din2 fd_min Dout orGateDelay fd_max Dout genCirDelay A P C D Dini B1 A P C D genCirDelay A P C D Din2 B2 A P C D domain Dout maximum fd_min Din1 fd_min Din2 fd_max Dout Observing the rules for the AND and OR gates we can see two new fresh domain variables for representing the delay in their inputs These new variables are constrained to have the domain of the delay in the output but pruned with the delay of the corresponding gate After the circuits connected to the inputs had been generated the domain of the output delay is pruned with the maximum of the input module delays N
275. the suspension has been evaluated or not Initially S is a variable indicating a non evaluated suspension which is set to the value hnf once the suspension is evaluated to head normal form The result of introducing suspensions into first order TOY programs is formally defined by means of the following function fs fs P fs Ri fs Rn Ja Gigs oxide Se 6 f t tn fale fs C fs X X fs n f fs e1 n fs e1 fslen fslelei n c fs e1 fs en fs f e1 n susp f fs e1 fs en R S Fs e1 o e2 fs e1 gt o fs ez G 3 Prolog Code Generation We now define the function pc which given a TOY program translated to first order and with suspensions returns a Prolog program which implements equality and disequality constraint solving by means of lazy narrowing with the demand driven strategy described in 22 We assume a first order with suspensions TOY program P for a signature DCUF S The Prolog code for P pc P is defined as pc P Solve U Equal pg U NotEqual pc U Hnfs U Prolog ps where Solve Equalpc NotEqual po Hnfs Prolog are sets of Prolog clauses to be defined below For the sake of clarity we present here in most occasions a simplification of the more optimized sets of clauses used in the actual implementation For a more detailed presentation we refer to 32 or TOY s source code specially the file toycomm pl It will be apparent below th
276. these different answers TOY performs backtracking in the same way as Prolog does A 1 2 Paths in a Graph paths toy The aim of the next program is to look for all the paths between two nodes in a given graph In logic programming this is done via a non deterministic predicate path X Y taking advantage of Prolog search mechanism to look for all the possible paths between two nodes The same idea is valid in TO the predicate path corresponds in TOY to a non deterministic boolean function indicating that X and Y are connected if either there is an arc between them or there exists an arc from X to a certain node Z such that Z and Y are connected In the example the graph considered is the following Paths in a Graph data node a b c d arc node node gt bool arc a b true arc b c true arc c a true arc d a true arc d c true 154 path node node gt bool path X Y arc X Y path X Y arc X Z path Z Y For instance the following goal asks TOY for nodes accessible from node d Toy gt path d X X gt a Elapsed time O ms more solutions y n d y X gt c Elapsed time O ms more solutions y n d y LX gt b Elapsed time O ms more solutions y n d y n A 2 Functional Programming In this section we show that TOY can also deal with functional computations TOY includes many of the features of lazy functional languages such as Haskell In particular
277. this polymorphic type we get also twice A gt A gt A gt A gt A gt A gt A gt A From the two previous facts it follows that twice twice is also a well typed expression with principal type twice twice A gt A gt A gt A More generally different uses of a polymorphic function within one and the same expression can correspond to different instances of its principal type In this way polymorphism promotes more generic and thus reusable programs Finally the following fact is interesting A function f with principal type f 71 gt gt Tn gt T can be used to build well typed expressions e f e1 m with different choices for the number m of arguments e In the case m n e 7 provided that there is some instance f T gt gt T gt 7 of f s principal type such that e 7 for all 1 lt i lt n For example twice not true bool e In the case m lt n e is called a partial application of f Moreover e Thy gt gt Ti gt 7 provided that there is some instance f T gt gt 7f gt T of f s principal type such that e 7 for all 1 lt i lt m For example twice not bool gt bool e In the case m gt n e is called an application of f with additional arguments Moreover e 7 provided that there is some instance f Ti gt gt Th gt 7 of f s principal type such that e 7 for all 1
278. tkRow tkCol of widgets whose first argument tkConfCollection specifies the geometric alignment The argument tkConfItem A of simple widgets allows to define the configuration options For a tkButton widget it is compulsory to associate a command to the press event of the button The possible configurations of a simple widget are the following data tkConfItem A tkActive bool Active state of buttons entries tkAnchor string Alignment of information in a widget argument must be n ne e se 4S SW w nw center tkBackground string Background color tkCmd channel gt A An associated command tkHeight int The height of a widget chars for text pixels for graphics tkInit string Initial value for checkbuttons tkItems tkCanvasItem List of items in a canvas tkList string Value list in a list box tkMenu tkMenuItem A The items of a menu button tkRef tkRefType A reference to the widget tkText string An initial text contents tkWidth int the width of widget chars for text pixels for graphics tkTcl string Further options in tcl syntax data tkMenultem A tkMButton channel gt A string A button with an associated command an a label tkMSeparator A separator between entries tkMMenuButton string tkMenuItem A A submenu data tkCanvasItem tkLine int int string tkPolygon int int string tkRectangle int int int int stri
279. to explore a branch known to yield no solution Let s firstly focus on the area factor The following function generates a circuit characterized by its state variables type area power cost delay int type state area power cost delay type circuit behavior state genCir state gt circuit genCir A P C D i0 A P C D genCir A P C D i1 A P C D genCir A P C D i2 A P C D genCir A P C D motGate B A P C D lt domain A fd_min A notGateArea fd_max A genCir A P C D B A P C D genCir A P C D andGate B1 B2 A P C D lt domain A fd_min A andGateArea fd_max A genCir A P C D B1 A P C D genCir A P C D B2 A P C D genCir A P C D orGate B1 B2 A P C D lt domain A fd_min A orGateArea fd_max A genCir A P C D B1 A P C D genCir A P C D B2 A P C D The function genCir has an argument to hold the circuit state and returns a circuit characterized by a behavior and a state Note that we can avoid the use of the state tuple as a parameter since it is included in the result The template of this function is like the previous example The difference lies in that we perform domain pruning during circuit generation with the membership constraint domain so that each time a rule is selected the domain variable representing area is reduced in t
280. to the solver for all the solutions via backtracking by assigning values to FD variables following an enumeration strat egy satisfaction problems Also it is possible to select from all the solutions the one which optimizes some cost function optimization problems It does not make any sense to reify enu meration functions TOY provides two enumeration constraints labeling 2 e Type Declaration labeling labelType int bool e Modes labeling inout inout inout Note Since the first argument is inout the lists of valid options can be produced How ever not all of them are produced because two of them demands a variable to be optimized as will be explained next e Definition labeling Options L is true if an assignment of the variables in L can be found such that all of the constraints already presented in the constraint store are satisfied L is a list of integers or domain variables with a bounded domain Options is a list of at most four elements that allow to specify an enumeration strategy Each element in this list can have a value in one of the following groups 1 The first group controls the order in which variables are chosen for assignment i e variable ordering and allows to select the leftmost variable in L leftmost the variable with the smallest lower bound mini the variable with the greatest upper bound maxi or the variable with the smallest domain ff The value
281. ts in solved form For example using the list concatenation function defined in Section 2 6 we can solve the goal 1 2 3 1 2 3 by typing at the prompt of the system Toy gt 1 2 3 1 2 3 yes Elapsed time O ms sol 1 more solutions y n d a y no Elapsed time O ms The previous goal is satisfiable with an empty computed answer After finding a solution for a goal the system can search for more solutions by backtracking like in Prolog inter preters In order to ask for the next solution the user must respond to the system s question more solutions y default option by typing y or simply lt Intro gt The system will answer no if no more solutions can be computed as in this example and it will display the next solution otherwise As an example of a goal with several solution consider Toy gt Xs Ys 1 2 Xs gt 0 Ys gt 1 2 5 Elapsed time O ms sol 1 more solutions y n d a y Xs gt 1 Ys gt 2 Elapsed time O ms sol 2 more solutions y n d a y Xs gt 1 2 Ys gt Elapsed time O ms sol 3 more solutions y n d a y no Elapsed time O ms In general computed answers can contain three kinds of constraints that will be showed by TOY in the following order e First the equality constraints in solved form that may be understood as bindings of vari ables to normal forms For example 43 Toy gt 1 2 3 L gt
282. uch a function is that is not defined for the value false that is it produces a failure for the value false Now we build an evaluator for first order logic formulas For simplicity we assume the proposition symbols p q and r and define the type of formulas as conj formula formula disy formula formula type formula p q r neg formula l implies formula formula iff formula formula For example the formula p A q r would be represented as implies conj p q r An interpre tation will be a 3 tuple of boolean values corresponding to the values of p q and r respectively The evaluation function eval F I evaluates the formula F over the interpretation J and it is defined as l y eval p P Q R eval q P Q R Il D 165 eval r P Q R R eval neg F P Q R not eval F I eval conj A B I and eval A I eval B I eval disy A B I or eval A I eval B I eval implies A B I eval disy neg A B I eval iff A B I eval A I eval BI false neg true neg false true and true X X and false X false true X or true X or false X For example for the previous formula p A q r and the interpretation true false true the expression eval imples conj p q r true false true will reduce to true Now we are interested in the satisfactibily of logic formulas in particular we want a tests for tautologies contradictions and contingencies First of all we need a function inter
283. ul enough to ensure the satisfiability This happens in JOY with non linear arithmetic constraints Suspended constraints can be re activated if some variables are instantiated in a later step of the computation During computations solved and suspended constraints act as a constraint store As the com putation proceed new constraints can be added to the store which must be checked again for satisfiability When the computation finishes the store is a part of the answer it is the answer it we see the substitution part of the answer as a solved form for equality constraints Currently TOY is able to manage three kinds of constraints e Syntactical constraints equality and disequality over constructor terms These are em bedded in the system and the constraint solver is implemented from the scratch gt More generally C can be any boolean expression e but in this case the condition e true is assumed by the system 6At least when using the goal solving mode of evaluation of TOY 55 e Arithmetical constraints over real numbers Their use is optional and the implementation mostly relies on the constraint solver for linear arithmetic constraints that comes with Sicstus Prolog e Constraints over finite domains As well their use is optional and the implementation mostly relies on the Sicstus Prolog finite domain constraint solver In this section we introduce the first two items The constraints over finite domains are exp
284. ume that the CD part of a program rule R l e lt CD includes both conditions and local definitions This makes sense because any condition or local definition has the syntactic form e e with two sides e and e We write var R for the set of variables occurring in R The main loop proceeds block by block from B to By For each block the algorithm builds an environment I whose type annotations represent the types inferred for all the functions in the block First I is initialized by assumming a fresh type variable as the type of each function Then the program rules in the current block are processed one by one The types of the left hand and the right hand sides are computed by means of the function T and an attempt to unify them is made Any internal type error in the left hand side or the right hand side is detected by T In the case that unification succeeds the algorithm checks the conditions and the local definitions of the program rule trying to unify the types obtained for its two sides After any application of T the environments and O are appropriately updated After processing all the program rules in the current block I contains the inferred types for all the functions in the block At this point the algorithm compares the inferred types with the types declared by the user if available If there is no declared type then the inferred type remains in I If there is a declared type which is an instance of the in
285. ut command before compiling a program e The debugger now allows programs goals with constraints over real numbers See the example examples debug ladder toy e New finite domain functions and constraints Membership constraints subset int gt int gt bool Domain subset setcomplement int gt int gt bool Domain complement inset int gt int gt bool Domain member intersect int gt int gt int Domain intersection belongs int gt int gt bool Domain definition Propositional constraints bool gt bool gt bool Disjunction lt gt bool gt bool gt bool Equivalence gt bool gt bool gt bool Implication Arithmetic constraint operators amp int gt int gt int Integer remainder e More constraints are now reifiable e g sum scalar_product e Some constraints become more declarative as they do not demand arguments with known finite types This is the case for instance of labeling Now it produces all the admissible options for labeling Consider the following goal Toy FD gt domain X 0 1 labeling L X X gt 0 L gt 1 Elapsed time 110 ms 252 more solutions y n d y X ae L gt l Elapsed time O ms more solutions y n d y X gt 0 L gt bisect Elapsed time O ms more solutions y n d y X gt gt 1 L gt bisect Elapsed time O ms more so
286. ven step of the computation a variable X is going to be bound to a term t it must be checked that the binding is compatible with all the stored disequalities for X This constraint propagation amounts to solve t s1 t Sn if X s X S was the store for X As an example we show below some stepts for the solving of a goal involving equality and disequality constraints and how the accumulated substitution and constraint store evolve The symbols a b c d are constructor symbols and indicates a don t know choice SOtherwise satisfiability of solved forms is not guaranteed For instance X Y X Z Y Z is not satisfiable if there are only two ground terms Since TO is a typed system this might happen for some types In particular this does happen for the type bool which has only the constants true and false Since the type bool is frequently used there is a special treatment of disequality in this case as to avoid unsatisfiable answers 58 Goal Substitution Constraint store c X c c Y dX Y daa dxX X d c Z c b X cY dX Y gt daa dxX X d c Z c b dXY daa dXX d c Z c b x1 X cY X a dXX d c Z c b X cY d X X d c Z c b X cY X a X c Z X cb X cY X a cZ cY cZ a cZ cb Xr cz Z Y Z a cZ cb Xr cZ cZ a cZ cb X gt cz Z Y cZ cb X gt cz Z Y Z X gt eczZ Z Y b Y XH cbZreb X cb Z b Y b The computed answer consists of the final ac
287. will be introduced in Section 2 16 26 Si Items 1 and 2 above require that the locally defined variables must be different from each other and away from the variables occurring in the rule s left hand side that act as formal parameters Moreover item 3 ensures that the variables defined in local definition number i can be used in local definition number j only if j gt i In particular this means that local definitions cannot be recursive The intended meaning of a defining rule f ti tn r lt Cj Cm where Dj Dp is the same as in functional programming languages namely an expression of the form f e1 n can be reduced by reducing the actual parameters e until they match the patterns ti checking that the conditions are satisfied and then reducing the right hand side r affected by the pattern matching substitution all this by using the local definitions to obtain the values of locally defined variables In particular this means that the equality symbol in defining rules is implicitely oriented from left to right The TOY system can apply the left to right oriented defining rules in order to compute the value of expressions using lazy evaluation This means that subexpressions occurring as actual parameters in function calls are not evaluated eagerly but delayed until their values are eventually needed The computations which obtain the values of locally defined variables are also delayed until they are needed
288. x fdset_singleton fdset_subtract fdset_union inf interval_to_fdset list_to_fdset serialized sum Table D 10 Finite Domain Library Predefined Functions allDiffOptions fdinterval labelingType range serial0ptions statistics fdset reasoning wakeOptions reserved Table D 11 Finite Domain Library Predefined Data Types 220 assumptions backtracks bisect compl complete constraints cte decomposition domains domm reserved down each edge_finder entailments enum ff ffc inter interval leftmost lift liftedInt maxi maxx reserved mini minmax reserved minn reserved path_consistency precedences prunings range reasoning resumptions static_sets step superior toMaximize toMinimize typeprecedence uni up vall reserved value Table D 12 Finite Domain Library Predefined Data Constructors PROGRAMS A program is a sequence of declarations program decl Top level declarations includeDecl infixDecl dataDecl typeAliasDecl funTypeDecl funDecl clauseDecl decl TOP LEVEL Include declaration includeDecl include Infix operator declaration DECLARATIONS String infixDecl gt 4 infix gt infixr gt infixl Integer op pp 221 Datatype declaration dataDecl gt data typeld varld dataTypeRhs dataTypeRhs type consOp type constructor simpleType da
289. xecution time 4 5 2 Distribution of raw material between suppliers and consumers distribution toy A company has six suppliers of raw material three of them supply integer quantities discreet suppliers and the other ones three supply real quantities continuous suppliers The problem is to satisfy the demand of raw material minimizing the cost with the following data 121 H RXo RYo N T 2 3 4 5 0 5 20000 5 20001 40000 1828 0 ai F z 2000000 5 2000001 4000000 179000 0 ES i I 20000 20000 5 40000 1125 0 2172 0 z z 2000000 2000000 5 4000000 111201 0 215156 0 2 20000 20000 5 40000 1125 0 1485 0 0 0 1500 0 2203 0 2000000 2000000 5 4000000 111329 0 147406 0 0 0 147453 0 216156 0 Table 4 3 Performance Results e D1 D2 and D3 are the quantities of raw material provided by the discreet suppliers They can provide until a maximum of 100 e R1 R2 and R3 are the quantities of raw material provided by the continuous suppliers They can provide until a maximum of 100 e The cost of the raw material is 3 plus its quantity CD1 3 D1 2 plus its quantity CD2 2 D2 and 2 multiply its quantity CD3 2 D3 for the discreet suppliers and CR1 2 R1 CR2 2 1 5 R2 and CR3 3 1 2 R3 for the continuous suppliers e The demand to satisfy is of X units of weight Below a JOY program that solve problem
290. xtra capabilities of the CFLP FD approach of TOY FD with respect to the traditional CLP FD approach include misc toy hh To use take 2 map 2 and 2 include cflpfd toy generateFD int gt int generateFD N X generateFD N lt domain X 0 N 1 lazymagic int gt int lazymagic N L lt take N generateFD N L Lazy evaluation constrain L L 0 Cs sum L N HO FD constraint scalar_product Cs L N HO FD constraint labeling ff L constrain int gt int gt int gt int gt bool constrain A B true constrain X Xs L I _ I S2 true lt count I L X HO FD constraint Ii I 1 constrain Xs L I1 S82 The goal lazymagic N for some natural number N returns the N magic series Observe the lazy evaluation of the condition take N generateFD N as generateFD N produces an infinite list as it was shown above A possible goal is as follows Toy FD gt gt lazymagic 10 6 2 1 0 0 O 1 O 0 0 Elapsed time 48 ms Alternative solutions and more flexibility can be reached in TOY with FD constraints For instance a more interesting case consists of returning a list of solutions for a possibly infinite set of different instances of the problem This can be done for example from a number N that 189 identified the first instance of the problem Now we can make use of the concept of infinite lists by defining the following function
291. yle Using the function fails we can even write predicates with negation replacing the predicate not by the function fails For example assume the following Prolog program member X X Xs member X Y Ys member X Y s insert X Xs X Xs not member X Xs insert X Xs Xs member X Xs The translation into a TOY program is straightforward file member toy in the examples di rectory of the distribution member X X Xs true member X Y Ys member X Ys insert X Xs X Xs fails member X Xs insert X Xs Xs member X Xs But failure has a variety of interesting uses in the context of functional logic programming itself It is useful in general search problems For example assume the following graph 3The formal semantics according to lazy evaluation is that fails e returns true if e can not be reduced to head normal form variable or constructor rooted term and false otherwise There prototype OOPS 33 available at http babel dacya ucm es jaime systems html incorporates con structive failure in a functional logic language 5l We can represent it in FLP and define a function path for checking if there is a path between two nodes file graph toy in the examples directory of the distribution data node a b c d next a b next a c next b c next b d path X X true path X Y path next X Y lt X Y Now assume we want to define the predicate safe for no
292. zation Problem golomb toy A 7 7 Lazy Constraint Programs e A 7 8 Programmable Search search toy A Miscellanea of Functions Bel MISC TOY sses o a a a de E B2 Mise TOY esla es a a do eS ae ee eG C Sample Modules Syntax DT LEXON sii a des Glee oe o A amp She Sle ot Ss Ae D2 Grammar x ros emin A oe a he poe Eh ae wes BE a Ge es Type Inference E 1 Dependency Analysis ooo ee E 2 Type Inference Algorithm e Declarative Semantics EL Motivation a 4 26o Ys ame eee a ee we SSA a RAD EK F 2 A Constructor Based Rewriting Logic 20 2000 4 F 3 Correctness of Computed Answers BA Models cerda 2224 288 22 948 26 SR Ee he REE RY eR GR ee Fb Extensions y e serina e eh eA BRE ERG Ree owe he Ge ee ad Operational Semantics G 1 First Order Translation of TOY Programs saaa G 1 1 Enhancing the Signature 2 0 0 0 2 00000 e eee ee G 1 2 First Order Translation of Program Rules and Rules for Q G 2 Introduction of Suspensions 2 a ee G 3 Prolog Code Generation G 3 1 Clauses for Goal Solving Solve o o G 3 2 Clauses for Computing Head Normal Forms Hnf9 G 3 3 Clauses for Function Definitions Prologrg Release Notes History H 1 Version 2 3 Launched on December 2006 o H 2 Version 2 2 3 Launched on July 2006 o o H 3 Ve

T OY - GPD - Universidad Complutense de Madrid

Contents

Download Pdf Manuals

Related Search

Related Contents