Contraction algebras and unification of (infinite) terms

摘要

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 systems of equations attached to a context-free grammar (sometimes called ALGOL-like systems). Systems of equations with terms are used to extend the original unification algorithm of Robinson to the case of infinite terms.