[pypy-svn] r23508 - pypy/dist/pypy/lib/logic

auc at codespeak.net auc at codespeak.net
Mon Feb 20 11:30:43 CET 2006


Author: auc
Date: Mon Feb 20 11:30:39 2006
New Revision: 23508

Added:
   pypy/dist/pypy/lib/logic/oz-clp.txt
Log:
doc about constraint & logic programming in oz (excertps from CTM)


Added: pypy/dist/pypy/lib/logic/oz-clp.txt
==============================================================================
--- (empty file)
+++ pypy/dist/pypy/lib/logic/oz-clp.txt	Mon Feb 20 11:30:39 2006
@@ -0,0 +1,306 @@
+===========================================
+Aspects of Oz extracted towards use in Pypy
+===========================================
+
+This is a set of (most of the time verbatim) notes, taken by aurelien
+while reading Van Roy & Haridi's great book (Concepts, Techniques and
+Models of Computer Programming), sometimes refered to as CTM.
+
+Relational Programming
+======================
+
+Basics : choice & fail statements
+---------------------------------
+
+* choice creates a 'choice point' : snapshot of the current state in
+  which to possibly rollback (to pick another alternative in case of
+  unification failure or explicit fail 'exception')
+
+* fail indicates that the current alternative is wrong
+
+How is choice different from slurping from a data sink ? The treatment
+of fail is taken into account. It provokes 'rolling back' (whatever
+that means now) and giving the next available value, if any. ((auc) I
+suspect that choice is no different than a dataflow source which
+output values on a special 'fail' exception.)
+
+The following code illustrate a basic generate-and-test search using
+these primitives. It is supposed to pick suitable colours for a man's
+suit, respecting the constraints : adjacent garments are in
+contrasting colours and shirt and socks have different colours.
+
+
+ declare fun {Soft} choice beige [] coral end end
+ declare fun {Hard} choice mauve [] ochre end end
+
+ declare proc {Contrast C1 C2}
+    choice C1={Soft} C2={Hard} [] C1={Hard} C2={Soft} end
+ end
+
+ declare fun {Suit}
+    Shirt Pants Socks
+ in
+    {Contrast Shirt Pants}
+    {Contrast Pants Socks}
+    if Shirt==Socks then fail end
+    suit(Shirt Pants Socks)
+ end
+
+This is executed sequentially; the choice statements are executed in
+the order that they are encountered during execution.
+
+Encapsulated search
+-------------------
+
+We might want to select a search strategy (depth-first, A*, ...), a
+solution delivering schedule (all at once, one at a time, ...); also
+to protect the whole program from interferences from the search
+(modularity concern, especially important in the context of concurrent
+programs).  For this, an "environement" is provided to encapsultate
+and direct the search.
+
+One can get this by adding the Solve primitive, which lazily calculate
+the needed solutions.
+
+One-solution search can be defined as :
+
+ fun {SolveOne F}
+    L={Solve F}
+ in
+    if L==nil then nil else [L.1] end
+ end
+
+It will return a list containing the first solution or nil (when no
+solution exists).
+
+All-solutions search using first-depth :
+
+ fun {SolveAll F}
+    L={Solve F}
+    proc {TouchAll L}
+       if L==nil then skip else {TouchAll L.2} end
+    end
+ in
+    {TouchAll L}
+    L
+ end
+
+(note Mozart users : a {Browse {SolveAll Suit}} will show the list of
+all solutions.)
+
+Relation to logic programming
+-----------------------------
+
+"The advantage of logic programming is that programs have two
+semantics, a logical and an operational semantics, which can be
+studied separately".
+
+LP in Prolog uses the resolution algorithm. Not in Oz.
+
+
+
+
+Unification in Oz
+=================
+
+Unification as put in Oz is a very powerful operation. It is provided
+through the '=' operator.
+
+"Binding a variable to a value is a special case of an operation
+called unification. The unification <TERM1>=<TERM2> makes the partial
+values <TERM1> and <TERM2> equal, if possible, by adding zero or more
+bindings to the store. For example, f(X Y)=f(1 2) does two bindings:
+X=1 and Y=2. If the two terms cannot be made equal, then an exception
+is raised. Unification exists because of partial values; if there
+would be only complete values, then it would have no meaning."
+
+Unification adds information to the single-assignment store (a set of
+dataflow variables, where each variable is either unbound or bound to
+some other store entity).
+
+Example : if the store has X=foo(A) and Y=foo(25), then doing X=Y will
+bind A to 25.
+
+*failure* is the exception raised when unification cannot happen. For
+instance (unification of two records) :
+
+ person(name:X1 age:23)
+ person(name:"Auc" age:32)
+
+will raise it. The fail statement raises this exception.
+
+It is symetric : X=Y means the same as Y=X
+It can create cyclic structures, as in : X=person(grandfather:X)
+It can bind cyclic structures :
+
+ X=f(a:X b:_)
+ Y=f(a:_ b:Y)
+ X=Y
+
+creates a two cycles structure writable as : X=f(a:X b:X)
+
+
+Unification algorithm :
+
+operation unify(x, y) that unify two partial values x and y in the
+store st.
+
+The Store : consists of a set of k variables : x1, ... xk that are
+partitioned as follows: 
+
+* set of unbound variables that are equal (also called equivalence
+  sets of variables). The variables in each set are equal to each
+  other but not to any other variables.
+
+* variables bound to a number, record or procedure (also called
+  determined variables).
+
+Example : st = {x1=foo(a:x2), x2=25, x3=x4=x5, x6, x7=x8} that has 8
+variables. It has three equivelence sets : {x3,x4,x5},{x6},{x7,x8}. It
+has two determined variables x1 and x2.
+
+The primitive bind operation : unification is defined in terms of a
+primitive bind operation on the store st. The operation binds all
+variables in an equivalence set:
+
+* bind(ES,<v>) binds all variables in the equivalence set ES to the
+  number or record <v>. For example, the operation
+  bind({x7,x8},foo(a:x2)) binds x7 and x8, which no longer are in an
+  equivalence set.
+
+* bind(ES1,ES2) merges the equivalence set ES1 with the equivalence
+  set ES2.
+
+Algorithm unify(x,y)
+
+1. if x is in the equivalence set ESx and y is in the equivalence set
+   ESy, then do bind(ESx,ESy). It is a noop if ESx == ESy.
+
+2. if x is in the equivalence set ESx and y is determined, then do
+   bind(ESx,y)
+
+3. if y is in the equivalence set ESy and y is determined, then do
+   bind(ESy,x)
+
+4. if x is bound to l(l1:x1,...,ln:xn) and y is bound to
+   l'(l'1:y1,...,l'm:ym) with l!=l' or {l1,...,ln}!={l'1,...,l'm},
+   then raise a failure exception
+
+5. if x is bound to l(l1:x1,...,ln:xn) and y is bound to
+   l(l1:y1,...,ln:yn), then for i from 1 to n do unify(xi,yi).
+
+
+With cycles : the above algorithm does not handle unification of
+partial values with cycles. For example, on x=f(a:x) and y=f(a:y) a
+call to unify(x,y) results in the recursive call unify(x,y), which is
+identical to the original call, looping forever.  A simple fix is to
+make sure that unify(x,y) is called at most once for each possible
+pair of two variables (x,y). With k variables in the store, this means
+at most k^2 unify calls. We do this through memoization of called
+pairs.
+
+
+The Constraint-based computation model
+======================================
+
+A computation space collects together basic constraints (in fact
+variable domains) and propagators (aka constraints), and puts them
+inside an encapsulation boundary. A propagator is simply a thread that
+can add new basic constraints to the store. A computation space is
+always created inside a parent space; it can see the constraints of
+its parent.
+
+Basic constraints and propagators
+---------------------------------
+
+Basic constraints are constraints that are directly represented in the
+single-assignment store. An example of a basic constraint is a binding
+of a dataflow variable, such as x = person(age:y). This gives partial
+information about x. (SEE CHAPTER 2) The binding represents an
+equality constraint between the dataflow variable and a partial value.
+
+Here, we extend the store with a new kind of basic constraint, namely
+membership in a finite domain. A finite domain is a finite set of
+integers. The new basic constraint is an equation of the form x in D,
+where D is a finite domain. This gives partial information about
+x. This basic constraint is added to the store by the statement
+x::D. Note that the finite domain constraint x in {n} is equivalent to
+the binding x=n.
+
+Adding the constraints x::D1, x::D2, ..., x::Dn restricts the domain
+of x to the intersection of the n domains, provided that the latter is
+nonempty. Adding a constraint with an empty domain for a variable
+would result in an inconsistent store.
+
+The single-assignment store seen previously can be considered as a
+constraint store. The basic constraints it represent are all of the
+form x=y, where x and y are partial values. We call these constraints
+'bindings', althhough they can do more than simply bind a variable to
+a value. The general operation of binding two partial values together
+is called unification.
+
+What are all the complete values to which a fresh variable can be
+bound ? This is not an obvious question since we can add cyclic
+bindings to the store, e.g X=foo(X). It turns out that variable can be
+bound to rational trees. A rational tree generalizes the finite trees
+to allow a certain kind of infinite trees that can be stored in a
+finite space. A rational tree can be represented as a root directed
+graph. Unfolding the graph to remove cycles and sharing yields the
+tree. For example the graph X=foo(X) represents the tree
+X=foo(foo(...)).
+
+When a variable is initially declared, it can potentially be bound to
+any rational tree. Each basic constraint (i.e each binding) that we
+add to the store restricts the set of rational trees to which the
+variable can be bound. For example, adding the constraint
+x=person(age:y) restricts the possible bindings of x, namely to
+rational trees whose root is a record of label person with one field
+whose feature name is age.  The single-assignment store therefore
+implements constraints over rational trees.
+
+The set of complete values to which a variable can be bound is called
+its domain. We talk here about constraints over two domains: rational
+trees and finite domains (the Mozart system implements finite sets of
+integer, fine-grained records and real interval).
+
+A propagator is a thread that continually observes the store and
+occasionally adds new basic constraints to the store. Each time a
+variable's domain is changes into the store, the propagators that use
+that variable must be given a chance to execute, so they can propagate
+new partial information ot variables. Wainting for a domain change is
+fine-grained variant of waiting for determinacy.
+
+The execution of these propagators must be order-independant.
+
+Programming searches with computation spaces
+--------------------------------------------
+
+We outline how computation spaces are used to implement search and
+distribution strategies. A search strategy defines how the search tree
+is explored (ie breadth-first,...). A distribution strategy defines
+the shape and content of the search tree, i.e how many alternatives
+exist at a node and what constraint is added for each
+alternative. Computation spaces can be used to program search
+strategies and distribution strategies independant of each other. How
+it is done :
+
+* create the space with the correct program inside. This program
+  defines all the variable and constraints in the space.
+
+* let the program run into the space. Variables and propagators are
+  created. All propagators execute until no more information can be
+  added to the store in this manner. The space eventually reaches
+  stability.
+
+* during the space's execution, the computation inside the space can
+  decide to create a choice point. The decision of which constraint to
+  add for each alternative defines the distribution strategy. One of
+  the space's thread will suspend when the choice point is created.
+
+* when the space has become stable, execution continues outside the
+  space, to decide what to do next. There are different possibilities
+  depending on whether or not a choice point has been created in that
+  space. If there is none, then execution can stop and return with a
+  solution. If there is one, then the search strategy decides which
+  alternative to choose and commits to that alternative.
+



More information about the Pypy-commit mailing list