Alberto Martelli coauthored An Efficient Unification Algorithm by Alberto Martelli and Ugo Montanari in 1982. With Ugo Montanari, he developed a term-equation algorithm whose acyclicity check is built into the implementation rather than treated as an expensive separate afterthought.[ref]
Unification asks for a substitution making terms identical; the most general unifier captures every solution through further substitution. This is stronger than finding one arbitrary matching assignment. The paper's equation transformations preserve the solution set while detecting incompatible constructors and cyclic finite-term requirements, connecting a declarative specification to an efficient procedure.
Articles by others on the same topic
There are currently no matching articles.