12.96 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.

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.