[pypy-svn] r22465 - pypy/dist/pypy/lib/logic
auc at codespeak.net
auc at codespeak.net
Fri Jan 20 10:01:42 CET 2006
Author: auc
Date: Fri Jan 20 10:01:40 2006
New Revision: 22465
Added:
pypy/dist/pypy/lib/logic/variable.py
Modified:
pypy/dist/pypy/lib/logic/unification.py
Log:
add a lot of documentation (from CTM)
move Var class into variable.py
Modified: pypy/dist/pypy/lib/logic/unification.py
==============================================================================
--- pypy/dist/pypy/lib/logic/unification.py (original)
+++ pypy/dist/pypy/lib/logic/unification.py Fri Jan 20 10:01:40 2006
@@ -1,83 +1,126 @@
-# Oz-like unification of dataflow variables in Python 2.4
-# within a single assignment store
-# crude ...
+## Oz-like unification of dataflow variables in Python 2.4
+## within a single assignment store
+## crude ...
+
+## Unification over dataflow variables in Oz is a powerful mechanism
+## which is the basis of relational, logic and constraint programming.
+## Please read the stuff in variable.py to understand the nature of
+## dataflow variables.
+##
+## Unification in Oz (almost verbatim from CTM*)
+## =============================================
+##
+## 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 equivalence 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); We do this through
+## memoization of called pairs.
+
+## * CTM : Concepts, Techniques and Models of Computer Programming
+## ** determined == bound
#TODO :
# * understand this :
# http://www.mozart-oz.org/papers/abstracts/ProgrammingConstraintServices.html
+# * support '_' as shown above
# * turn Var into some dataflow-ish thing (as far as Python allows)
# * ensure that the store supports concurrent access
# (using the implicit blocking provided by dataflow vars)
# * add entailment checks
# * add constraints support
-#----------- Variables ----------------------------------
-class EqSet(set):
- """An equivalence set for variables"""
- pass
-
-class NoValue:
- pass
-
-class Var(object):
-
- def __init__(self, name, store):
- self.name = name
- self.store = store
- # top-level 'commited' binding
- self._val = NoValue
- # when updated in a 'transaction', keep track
- # of our initial value (for abort cases)
- self.previous = None
- self.changed = False
-
- def is_bound(self):
- return not isinstance(self.val, EqSet) \
- and self.val != NoValue
-
- def commit(self):
- self.changed = False
-
- def abort(self):
- self.val = self.previous
- self.changed = False
-
- def set_val(self, val):
- if self.store.in_transaction:
- if not self.changed:
- self.previous = self._val
- self.changed = True
- print "in transaction, %s <- %s" % (self.name, val)
- self._val = val
- def get_val(self):
- return self._val
- val = property(get_val, set_val)
-
- def __str__(self):
- if self.is_bound():
- return "%s = %s" % (self.name, self.val)
- return "%s" % self.name
-
- def __repr__(self):
- return self.__str__()
-
- def __eq__(self, thing):
- return isinstance(thing, Var) \
- and self.name == thing.name
-
- def __hash__(self):
- return self.name.__hash__()
-
-def var(name):
- v = Var(name, _store)
- _store.add_unbound(v)
- return v
+from variable import EqSet, Var, VariableException, NotAVariable
#----------- Store Exceptions ----------------------------
-class VariableException(Exception):
- def __init__(self, name):
- self.name = name
-
class UnboundVariable(VariableException):
def __str__(self):
return "%s has no value yet" % self.name
@@ -97,11 +140,6 @@
return "%s %s can't be unified" % (self.var1,
self.var2)
-#----------- Variable Exceptions-------------------------
-class NotAVariable(VariableException):
- def __str__(self):
- return "%s is not a variable" % self.name
-
#----------- Store ------------------------------------
class Store(object):
"""The Store consists of a set of k variables
@@ -299,6 +337,11 @@
_store = Store()
#-- global accessor functions
+def var(name):
+ v = Var(name, _store)
+ _store.add_unbound(v)
+ return v
+
def bind(var, val):
return _store.bind(var, val)
Added: pypy/dist/pypy/lib/logic/variable.py
==============================================================================
--- (empty file)
+++ pypy/dist/pypy/lib/logic/variable.py Fri Jan 20 10:01:40 2006
@@ -0,0 +1,72 @@
+#----------- Exceptions ---------------------------------
+class VariableException(Exception):
+ def __init__(self, name):
+ self.name = name
+
+class NotAVariable(VariableException):
+ def __str__(self):
+ return "%s is not a variable" % self.name
+
+#----------- Variables ----------------------------------
+class EqSet(set):
+ """An equivalence set for variables"""
+ pass
+
+class NoValue:
+ pass
+
+class Var(object):
+
+ def __init__(self, name, store):
+ self.name = name
+ self.store = store
+ # top-level 'commited' binding
+ self._val = NoValue
+ # when updated in a 'transaction', keep track
+ # of our initial value (for abort cases)
+ self.previous = None
+ self.changed = False
+
+ def is_bound(self):
+ return not isinstance(self.val, EqSet) \
+ and self.val != NoValue
+
+ def commit(self):
+ self.changed = False
+
+ def abort(self):
+ self.val = self.previous
+ self.changed = False
+
+ def set_val(self, val):
+ if self.store.in_transaction:
+ if not self.changed:
+ self.previous = self._val
+ self.changed = True
+ print "in transaction, %s <- %s" % (self.name, val)
+ self._val = val
+ def get_val(self):
+ return self._val
+ val = property(get_val, set_val)
+
+ def __str__(self):
+ if self.is_bound():
+ return "%s = %s" % (self.name, self.val)
+ return "%s" % self.name
+
+ def __repr__(self):
+ return self.__str__()
+
+ def __eq__(self, thing):
+ return isinstance(thing, Var) \
+ and self.name == thing.name
+
+ def __hash__(self):
+ return self.name.__hash__()
+
+def var(name):
+ v = Var(name, _store)
+ _store.add_unbound(v)
+ return v
+
+
More information about the Pypy-commit
mailing list