Substructural Abstract Syntax with Variable Binding and Single-Variable Substitution
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912404322910208 |
|---|---|
| author | Fiore, Marcelo Ranchod, Sanjiv |
| author_facet | Fiore, Marcelo Ranchod, Sanjiv |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_24812 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Substructural Abstract Syntax with Variable Binding and Single-Variable Substitution Fiore, Marcelo Ranchod, Sanjiv Logic in Computer Science Category Theory 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. |
| title | Substructural Abstract Syntax with Variable Binding and Single-Variable Substitution |
| topic | Logic in Computer Science Category Theory |
| url | https://arxiv.org/abs/2505.24812 |