Substructural Abstract Syntax with Variable Binding and Single-Variable Substitution

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.

To appear in the Fortieth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'25)