Next: CGI utility, Previous: Topological sort, Up: Library modules - Utilities [Contents][Index]

`util.unification`

- Unification- Module:
**util.unification** -
Implements unification algorithm.

The base API operates on abstract trees, while it is agnostic to the actual representation of the tree. The caller passes comparators and operators along the trees to unify.

We assume the abstract tree has the following structure:

Tree : Variable | Value | Tuple Tuple : { Tree ... }

Here,

`{...}`

just represents a sequence of trees.A variable can be bound to a tree. A value can only match itself.

To operate on this tree, we need the following comparators and procedures, which the API takes as arguments:

- Variable comparator:
`var-cmpr`

A comparator to see if an item is a variable, and also check equality of two variables. It must be hashable. See Basic comparators, for the details of comparators.

- Value comparator:
`val-cmpr`

A comparator to see if an item is a value, and also check equality of two values. Note that if a tree satisfies neither

`var-cmpr`nor`val-compr`, it is regarded as a tuple.- Tuple folder:
`tuple-fold`

A procedure

`(tuple-folde proc seed tuple1 [tuple2])`

. This procedure should work like`fold`

(see Walking over lists) over the elements in the tuple(s). It is only called with either one or two tuples.- Tuple constructor:
`make-tuple`

A procedure

`(make-tuple proto elements)`

, where`proto`is a tuple and`elements`are a list of trees. It must return a new tuple with the given elements, while all other properties are the same as`proto`. This procedure isn’t needed by`unify`

.

- Variable comparator:

- Function:
**unify***a b var-cmpr val-cmpr tuple-fold* {

`util.unification`} Unify two trees`a`and`b`and returns a substitution dictionary, which is a dictionary that maps variables to its bounded trees.See the entry of

`util.unification`

above for the description of`var-cmpr`,`val-cmpr`and`tuple-fold`.(dict->alist (unify '(a 3 (c b)) '(c b (2 e)) symbol-comparator number-comparator fold)) ⇒ ((e . 3) (a . c) (b . 3) (c . 2))

As you can see in the example above, a variable may be mapped to another variable, or even to a tree that contains variables. If you apply the substitution to the original tree, you must do it recursively until all the variables in the dictionary is eliminated.

If two trees cannot be unified,

`#f`

is returned.(unify '(a (a)) '(x x) symbol-comparator number-comparator fold) ⇒ #f

- Function:
**unify-merge***a b var-cmpr val-cmpr tuple-fold make-tuple* {

`util.unification`} Unify two trees`a`and`b`, and apply the result substitutions to create a new tree eliminating variables.See the entry of

`util.unification`

above for the description of`var-cmpr`,`val-cmpr`,`tuple-fold`and`make-tuple`.(unify-merge '(a 3 (c b)) '(c b (2 e)) symbol-comparator number-comparator fold (^[_ elts] elts)) ⇒ (2 3 (2 3))

If two trees can’t be unified,

`#f`

is returned.

Next: CGI utility, Previous: Topological sort, Up: Library modules - Utilities [Contents][Index]

DRAFT