2026-07-26T11:14:48Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20354 2024-07-05T06:20:34Z ddc:004 open_access

Substitution for Non-Wellfounded Syntax with Binders Through Monoidal Categories Matthes, Ralph Wullaert, Kobe Ahrens, Benedikt Non-wellfounded syntax Substitution Monoidal categories Actegories Tensorial strength Proof assistant Coq UniMath library 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 multi-sorted 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Ralph Matthes and Kobe Wullaert and Benedikt Ahrens 2024 Is Part Of LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2024.25 urn:nbn:de:0030-drops-203540 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.25 eng https://creativecommons.org/licenses/by/4.0/legalcode