Substructural Abstract Syntax with Variable Binding and Single-Variable Substitution

2025/05/30 by Marcelo Fiore, Fiore, Marcelo, Sanjiv Ranchod +1
Computer Science · #Category Theory (math.CT) #FOS: Computer and information sciences #FOS: Mathematics #Logic in Computer Science (cs.LO) #Natural Language Processing Techniques

paper · pdf · doi:10.48550/arxiv.2505.24812

openalex publication_date 2025/05/30 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Citations

• A finite algebraic presentation of Lawvere theories in the object-classifier topos
• Taut functors and the difference operator
• Operads and PROPs
• Strong functors and monoidal monads

Related

• A unified treatment of structural definitions on syntax for capture-avoiding substitution, context application, named substitution, partial differentiation, and so on
• A Formalized General Theory of Syntax with Bindings
• Modular abstract syntax trees (MAST): substitution tensors with second-class sorts
• Substitution for Non-Wellfounded Syntax with Binders through Monoidal Categories
• Adjunction As Substitution: An Algebraic Formulation of Regular, Context-Free and Tree Adjoining Languages