A unified treatment of structural definitions on syntax for capture-avoiding substitution, context application, named substitution, partial differentiation, and so on

TL;DR

This paper presents a category-theoretic framework for defining and reasoning about complex syntax structures with auxiliary functions, enabling automation and generalization across various lambda calculi and related systems.

Contribution

It introduces admissible monad morphisms and generic tools for constructing and proving properties of auxiliary functions in syntax, unifying multiple approaches.

Findings

Automates defining auxiliary functions in layered syntax structures.

Provides induction-based proof techniques for properties of auxiliary functions.

Successfully applies to lambda-calculus variants and differential lambda-calculus.

Abstract

We introduce a category-theoreticabstraction of a syntax with auxiliary functions, called an admissiblemonad morphism. Relying on an abstract form of structural recursion,we then design generic tools to construct admissible monad morphismsfrom basic data. These tools automate ubiquitous standard patternslike (1) defining auxiliary functions in successive, potentiallydependent layers, and (2) proving properties of auxiliary functions byinduction on syntax. We cover significant examples from theliterature, including the standard lambda-calculus withcapture-avoiding substitution, a lambda-calculus with bindingevaluation contexts, the lambda-mu-calculus with named substitution, andthe differential lambda-calculus.