Unifying Substitutions

The central notion of every unification machinery is that of unifying substitution. A unifying substitution - or environment - is a mapping from variable names (or variables) to values (which can be variables themselves.)

The generic function UNIFY, and several other functions and macros in the package accept unifying substitutions as parameters, and return them as values.

There are several notations to describe such unifying substitutions. The one chosen here is simply the following:

  {x1 -> y1, x2 -> y2, ..., xk -> yk}

The UNIFY library has a number of functions and data structures that can be used to construct and manipulate unifying substitutions.

In order to facilitate the construction of interpreter-like programs the UNIFICATION library provides data structures representing bindings, frames, and environments - i.e. the unifying substitions proper.

  • Bindings

    A binding simply represent the mapping between a variable and a value.

      binding: variable --> value

  • Frames

    A frame is simply a collection of bindings.

      frame: {bindingi}

  • Environments

    An environment is simply a stack of frames.

      environment: <frame0, frame1, ..., framek>

The collection of operators described hereafter manipulates these opaque data structures.

Unifying Substitutions Dictionary


Current Implementation Details

The current implementation is rather straightforward. A binding is a CONS, a frame is a wrapper around an A-LIST, and an environment is a wrapper around a LIST (stack) of frames.

Functional Style Unifying Substitutions

There are very elegant implementations of unification and substitutions based on curried functions. A typical exercise in functional programming using ML or a similar language is to write a simplified Milner Type Checker. Writing the unifying substitution support can be achieved by using curried functions in that context.