= Alberto Martelli
{c}
<Alberto Martelli> coauthored <An Efficient Unification Algorithm by Alberto Martelli and Ugo Montanari> in 1982. With <Ugo Montanari>, he developed a <first-order term>[term-equation] algorithm whose acyclicity check is built into the implementation rather than treated as an expensive separate afterthought.<An Efficient Unification Algorithm by Alberto Martelli and Ugo Montanari>[abstract and §2]{ref}
<Unification> asks for a <first-order substitution>[substitution] making <first-order term>[terms] identical; the <most general unifier> captures every solution through further <first-order substitution>[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.
Back to article page
