TL;DR
This paper introduces a new lambda-calculus with explicit, delayable renaming of variables and a novel structure for contexts, simplifying the process of alpha-conversion.
Contribution
It proposes a lambda-calculus with explicit, delayed variable renaming and a new context structure, enhancing the understanding and handling of alpha-conversion.
Findings
Explicit renaming can be delayed in the calculus.
Contexts have a natural order, improving variable management.
Simplifies alpha-conversion processes.
Abstract
We present a new lambda-calculus with explicit substitutions and named variables. Renaming of bound variables in this calculus is explicit (there is a special rewrite rule) and can be delayed. Contexts (environments) are not sets or lists without multiplicity, but have a more complicated structure. There is a natural order on the set of contexts. A "set" of free variables is not a set, but a context in the new sense. New definitions simplify working with alpha-conversion.
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.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Logic, Reasoning, and Knowledge