A practical view on substitutions
For logic program analysis or formal semantics, the issue of re- naming terms and generally handling substitutions is inevitable. We revisit substitutions from a practitioner’s point of view, pre- senting concepts we found useful in dealing with operational se- mantics of pure Prolog. A concept of relaxed core representation is introduced, upon which a concept of prenaming is built. Prenam- ing formalizes the intuitive practice of renaming terms and allows for extensibility. A novel algorithm for term matching is proposed, which also solves the problem of substitution generality (and thus equivalence), using witness term technique. The technique aleviates the problem of ad-hoc proofs involving generality.
Nutzung und Vervielfältigung:
Alle Rechte vorbehalten