Abstract
We describe a generic construction of non-wellfounded syntax involving variable binding and its monadic substitution operation.
Our construction of the syntax and its substitution takes place in category theory, notably by using monoidal categories and strong functors between them. A language is specified by a multisorted binding signature, say Σ. First, we provide sufficient criteria for Σ to generate a language of possibly infinite terms, through ω-continuity. Second, we construct a monadic substitution operation for the language generated by Σ. A cornerstone in this construction is a mild generalization of the notion of heterogeneous substitution systems developed by Matthes and Uustalu; such a system encapsulates the necessary corecursion scheme for implementing substitution.
The results are formalized in the Coq proof assistant, through the UniMath library of univalent mathematics.
Our construction of the syntax and its substitution takes place in category theory, notably by using monoidal categories and strong functors between them. A language is specified by a multisorted binding signature, say Σ. First, we provide sufficient criteria for Σ to generate a language of possibly infinite terms, through ω-continuity. Second, we construct a monadic substitution operation for the language generated by Σ. A cornerstone in this construction is a mild generalization of the notion of heterogeneous substitution systems developed by Matthes and Uustalu; such a system encapsulates the necessary corecursion scheme for implementing substitution.
The results are formalized in the Coq proof assistant, through the UniMath library of univalent mathematics.
| Original language | English |
|---|---|
| Title of host publication | 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024) |
| Editors | Jakob Rehof |
| Publisher | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |
| Number of pages | 22 |
| ISBN (Electronic) | 978-3-95977-323-2 |
| DOIs | |
| Publication status | Published - 2024 |
| Event | 9th International Conference on Formal Structures for Computation and Deduction - Tallinn, Estonia Duration: 10 Jul 2024 → 13 Jul 2024 |
Publication series
| Name | Leibniz International Proceedings in Informatics, LIPIcs |
|---|---|
| Volume | 299 |
| ISSN (Print) | 1868-8969 |
Conference
| Conference | 9th International Conference on Formal Structures for Computation and Deduction |
|---|---|
| Abbreviated title | FSCD 2024 |
| Country/Territory | Estonia |
| City | Tallinn |
| Period | 10/07/24 → 13/07/24 |
Keywords
- Actegories
- Monoidal categories
- Non-wellfounded syntax
- Proof assistant Coq
- Substitution
- Tensorial strength
- UniMath library