A categorical approach to unification of generalised terms1 1This work has been developed as a cooperation organised within COST 274.
Patrik Eklund, M.A. Galán, Jesús Medina, Manuel Ojeda‐Aciego, Agustín Valverde · Electronic Notes in Theoretical Computer Science · 2002
Unification of generalised terms in a many-valued setting involves considerations for equalities in the sense of similarity degrees between operators and thus similarities between terms. Further, allowing for substitutions of variables with powersets of terms requires ‘flattening’ operators for handling composition of variable substitutions. These techniques are available when using powerset functors composed with the term functor so that this composition of functors is extendable to a monad. In this paper we provide a framework for unification of such generalised terms.