Substructural Abstract Syntax with Variable Binding and Single-Variable Substitution

TL;DR

This paper presents a unified categorical framework for substructural abstract syntax with variable binding and substitution, covering various structural rules like exchange, weakening, and contraction.

Contribution

It introduces a universal categorical approach to abstract syntax with variable binding and substitution across different structural theories.

Findings

Unified categorical theory for substructural syntax

Finitary algebraic axioms for substitution laws

Construction and correctness proof of substitution operations

Abstract

We develop a unified categorical theory of substructural abstract syntax with variable binding and single-variable (capture-avoiding) substitution. This is done for the gamut of context structural rules given by exchange (linear theory) with weakening (affine theory) or with contraction (relevant theory) and with both (cartesian theory). Specifically, in all four scenarios, we uniformly: define abstract syntax with variable binding as free algebras for binding-signature endofunctors over variables; provide finitary algebraic axiomatisations of the laws of substitution; construct single-variable substitution operations by generalised structural recursion; and prove their correctness, establishing their universal abstract character as initial substitution algebras.