On separation, conservation and unification
Based on variable substitution, we discuss a practical aspect of Prolog computation, algorithms for unification and standardizing-apart. The focus is on simplicity and desirable mathematical properties. For unification, we start from a deterministic version of Martelli-Montanari’s algorithmic scheme that also happens to correspond to Robinson’s algorithm (hence, "the" classical unification algorithm) and discuss two of its adaptations, concerned with modularity or with ordering of variables. Standardizing-apart is defined as a special case of (relatively) fresh renaming. Examples for both kinds of algorithms are given, and some properties are discussed. As a common ground, the issue of variable separation (i.e. variable-disjointness between parts of terms) is raised. Variable conservation, important for formal semantics, is also approached.
Nutzung und Vervielfältigung:
Alle Rechte vorbehalten