[pypy-svn] r22598 - pypy/dist/pypy/lib/logic
auc at codespeak.net
auc at codespeak.net
Tue Jan 24 15:57:32 CET 2006
Author: auc
Date: Tue Jan 24 15:57:31 2006
New Revision: 22598
Added:
pypy/dist/pypy/lib/logic/computationspace.py
Log:
(auc, ale)
add computation space 'manifesto'
Added: pypy/dist/pypy/lib/logic/computationspace.py
==============================================================================
--- (empty file)
+++ pypy/dist/pypy/lib/logic/computationspace.py Tue Jan 24 15:57:31 2006
@@ -0,0 +1,105 @@
+## 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