Contraction Algebras and Unification of (Infinite) Terms (abstract)

We introduce the class of contraction algebras in which the algebra of infinite and finite terms is free over the set of variables. We develop a general theory of systems of equations at the level of categories in close connection with the Banach Principle of Contraction. Two applications of this theory are given. The first is the case of regular systems of equations with arbitrary terms. The second is the case of of systems of equations attached to a context-free grammar (sometimes called ALGOL-like systems). Systems of euqations with terms are used to extend the original unification algorithm of Robinson to the case of infinite terms.

back to Selected Publications