By abstracting over well-known properties of De Bruijn's representation with nameless dummies, we design a new theory of syntax with variable binding and capture-avoiding substitution. We propose it as a simpler alternative to Fiore, Plotkin, and Turi's approach, with which we establish a strong formal link. We also show that our theory easily incorporates simple types and equations between terms.
翻译:通过抽象化德布鲁因表示法中关于无名虚名的已知性质,我们设计了一种新的语法理论,支持变量绑定与避免捕获的替换操作。该理论被提出作为Fiore、Plotkin与Turi方法的更简化替代方案,并与后者建立了紧密的形式化关联。我们同时证明,该理论可自然融入简单类型与项间等式处理。