On separation, conservation and unification

Kulaš, Marija GND

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.

Vorschau

Zitieren

Zitierform:

Kulaš, Marija: On separation, conservation and unification. Hagen 2019. FernUniversität in Hagen.

Zugriffsstatistik

Gesamt:
Volltextzugriffe:
Metadatenansicht:
12 Monate:
Volltextzugriffe:
Metadatenansicht:

Grafik öffnen

Rechte

Nutzung und Vervielfältigung:
Alle Rechte vorbehalten

Export

powered by MyCoRe