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:

  {x₁ -> y₁, x₂ -> y₂, ..., x_k -> y_k}

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: {binding_i}
  
```

Environments

An environment is simply a stack of frames.

  environment: <frame₀, frame₁, ..., frame_k>

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

Unifying Substitutions Dictionary

Notes

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.

CL Extensions: UNIFYING SUBSTITUTIONS Home \| Downloads \| Links
	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: {x₁ -> y₁, x₂ -> y₂, ..., x_k -> y_k} 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: {binding_i} Environments An environment is simply a stack of frames. environment: <frame₀, frame₁, ..., frame_k> The collection of operators described hereafter manipulates these opaque data structures. Unifying Substitutions Dictionary FIND-VARIABLE-VALUE MAKE-EMTPY-ENVIRONMENT MAKE-SHARED-ENVIRONMENT Notes 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.

© 2003-2013, Marco Antoniotti, all rights reserved.