A Practical View on Renaming

TL;DR

This paper presents a practical approach to variable renaming in logic programming, introducing prenaming as a formal tool to handle variable bindings efficiently, with applications to Horn clause logic.

Contribution

It introduces the concept of prenaming and a relaxed core representation, providing a constructive variant lemma for Horn clause logic.

Findings

Prenaming formalizes variable renaming with minimal bindings.

A constructive variant lemma for Horn clause logic is developed.

Prenaming enables incremental handling of local variables.

Abstract

We revisit variable renaming from a practitioner's point of view, presenting concepts we found useful in dealing with operational semantics of pure Prolog. A concept of relaxed core representation is introduced, upon which a concept of prenaming is built. Prenaming formalizes the intuitive practice of renaming terms by just considering the necessary bindings, where now some passive "bindings" x/x may be necessary as well. As an application, a constructive version of variant lemma for implemented Horn clause logic has been obtained. There, prenamings made it possible to incrementally handle new (local) variables.