Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Variable binding and substitution for (nameless) dummies

André Hirschowitz, Tom Hirschowitz, Ambroise Lafont, Marco Maggesi

TL;DR

This paper develops a simple, set-based initial-algebra semantics for syntax with variable binding using nameless De Bruijn dummies. It formulates De Bruijn monads and binding signatures, proving the existence of an initial De Bruijn S-algebra that models substitution, and shows this framework aligns with Fiore–Plotkin–Turi’s presheaf approach when restricted to well-behaved objects. It further provides two abstract reinterpretations: a strength-based view identifying binding signatures with structurally strong endofunctors (Sigma-monoids) and a module-based view via parametric De Bruijn modules, both yielding category isomorphisms with S-DBAlg. The theory extends to simply-typed languages through De Bruijn T-monads, supports equations (via De Bruijn equational theories), and is mechanised in HOL Light and Coq. Together, these results offer a robust, implementation-friendly foundation for syntax with binding and substitution, bridging traditional approaches and enabling practical reasoning in proof assistants.

Abstract

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.

Variable binding and substitution for (nameless) dummies

TL;DR

This paper develops a simple, set-based initial-algebra semantics for syntax with variable binding using nameless De Bruijn dummies. It formulates De Bruijn monads and binding signatures, proving the existence of an initial De Bruijn S-algebra that models substitution, and shows this framework aligns with Fiore–Plotkin–Turi’s presheaf approach when restricted to well-behaved objects. It further provides two abstract reinterpretations: a strength-based view identifying binding signatures with structurally strong endofunctors (Sigma-monoids) and a module-based view via parametric De Bruijn modules, both yielding category isomorphisms with S-DBAlg. The theory extends to simply-typed languages through De Bruijn T-monads, supports equations (via De Bruijn equational theories), and is mechanised in HOL Light and Coq. Together, these results offer a robust, implementation-friendly foundation for syntax with binding and substitution, bridging traditional approaches and enabling practical reasoning in proof assistants.

Abstract

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.
Paper Structure (44 sections, 42 theorems, 52 equations, 1 figure)

This paper contains 44 sections, 42 theorems, 52 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Overview
  3. Plan of the paper
  4. Related work
  5. Abstract frameworks for variable binding
  6. Proof assistant libraries
  7. General notation
  8. De Bruijn monads
  9. Definition of De Bruijn monads
  10. Lifting assignments
  11. Binding arities and binding conditions
  12. Binding signatures and algebras
  13. Initial-algebra semantics of binding signatures in De Bruijn monads
  14. A category of De Bruijn monads
  15. De Bruijn monads as relative monads and as monoids
  16. ...and 29 more sections

Key Result

Theorem 2.21

Consider any binding signature $S= (O,{\mathit{ar}})$, and let ${\mathrm{DB}_{S}}$ denote the initial $(ℕ+Σ_S)$-algebra, with structure maps $v∶ ℕ → {\mathrm{DB}_{S}}$ and $a∶ Σ_S({\mathrm{DB}_{S}}) → {\mathrm{DB}_{S}}$. Then,

Figures (1)

  • Figure 1: Diagram chasing for the proof of Proposition \ref{['prop:coprod-strong']}.

Theorems & Definitions (186)

  • Definition 1.1
  • Example 1.2
  • Definition 1.3
  • Remark 1.4
  • Definition 1.5
  • Definition 2.1
  • Definition 2.3
  • Example 2.4
  • Example 2.5
  • Definition 2.6
  • ...and 176 more