万物各有其所：一种无名的共 de Bruijn 表示

任何无名的语法表示的关键都在于它如何指示我们所选择使用的变量，从而隐式地指示那些被丢弃的变量。标准的 de Bruijn 表示将丢弃尽可能推迟到项的叶子处，在那里从作用域内的变量中选出一个而舍弃其余。因此，引入新的但未使用的变量需要遍历项。本文引入一种无名的“共 de Bruijn（co-de-Bruijn）”表示，它做出相反的规范选择，将丢弃尽可能最小化地推迟，尽可能靠近根。它是文学化 Agda：依赖类型使得表达并由强内在不变式所驱动成为一种实际乐趣，这些不变式确保作用域被积极地削减到仅剩每个子项的支撑集，其中每个剩余变量都在某处出现。该构造是通用的，给出一个带高阶元变量的语法宇宙，其恰当的代换概念是遗传的。同时代换的实现利用严格的作用域控制避免繁琐工作并无遍历地平移项。令人惊讶的是，它仅凭结构递归也是内在终止的。