Binder aware recursion over well-scoped de Bruijn syntax

Abstract

The de Bruijn representation of syntax with binding is commonly used, but flawed when it comes to recursion. As the structural recursion principle associated to an inductive type of expressions is unaware of the binding discipline, each recursive definition requires a separate proof of compatibility with variable instantiation. We solve this problem by extending Allais' notion of syntax traversals to obtain a framework for instantiation-compatible recursion. The framework is general enough to handle multivariate, potentially mutually recursive syntactic systems.