TL;DR
This paper introduces a new nameless syntax representation called 'co-de-Bruijn' that minimizes scope traversal and improves efficiency in variable handling, using dependent types in Agda for strong invariants.
Contribution
It presents the co-de-Bruijn representation, a novel approach that delays variable discarding minimally, with a generic, terminating implementation leveraging dependent types.
Findings
Reduces scope traversal for variable introduction
Ensures termination through structural recursion
Enables efficient hereditary substitution
Abstract
The key to any nameless representation of syntax is how it indicates the variables we choose to use and thus, implicitly, those we discard. Standard de Bruijn representations delay discarding maximally till the leaves of terms where one is chosen from the variables in scope at the expense of the rest. Consequently, introducing new but unused variables requires term traversal. This paper introduces a nameless 'co-de-Bruijn' representation which makes the opposite canonical choice, delaying discarding minimally, as near as possible to the root. It is literate Agda: dependent types make it a practical joy to express and be driven by strong intrinsic invariants which ensure that scope is aggressively whittled down to just the support of each subterm, in which every remaining variable occurs somewhere. The construction is generic, delivering a universe of syntaxes with higher-order…
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.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
