
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
