10.1 What is Unification?

The idea of unification is to describe values by logical equations which can be resolved automatically by some unification algorithm. First-order unification is a form of unification whose values are trees. There are several kinds of first-order unification which differ in the choice of the notion of trees. Trees may be ground terms (tuples) or feature trees (records), they may be finite or infinite. First-order unification for feature trees is called feature unification.

Oz provides first-order unification for tuples and records. Feature unification is a prerequisite for building a parser for a unification grammar. In order to write unification-based chart parser in a high-level manner, something beyond feature unification is needed. Is is essential to treated solved forms of equations as first-class values which then can be associated with the edge of a chart. Indeed, Oz supports constraints as first-class values by so called encapsulated search. Oz is unique in this respect.