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