2026-07-30T14:29:15Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:27033 2026-07-30T09:16:25Z ddc:004 open_access

Mendler Dialgebras and Recursion Schemes of Mixed Variance Spahn, Stephan Alexander Mendler Algebra Dinatural Transformation Structured Recursion Scheme Grothendieck Fibration Higher-Order Abstract Syntax We introduce the notion of Mendler dialgebra and provide a categorical semantics of recursion schemes of mixed variance in its terms. The Mendler-style approach - which employs second-order inference rules - to recursion schemes of mixed variance was championed by Uustalu and Vene in [Uustalu and Vene, 1999] using dinatural transformations, and we generalize their methods to include a variety of new recursion schemes including those presented by Ahn-Sheard in [Ahn and Sheard, 2011], and Stump et al. in [Aaron Stump et al., 2020]. We give sufficient criteria for reducibility of Mendler dialgebras to Lambek algebras [Joachim Lambek, 1968] which correspond to first-order inference rules. A similar reduction in elementary terms for the special case of the systems studied in [Uustalu and Vene, 1999] had been given by the authors, but our approach differs in that we use the language of two-sided fibrations [Street, 1974] to express the reduction for our generalization. This reveals that the "diagonal" of every two-sided fibration with a fibered initial object is isomorphic to a category of Lambek algebras; a dual version concerning reduction to Lambek coalgebras, as well as to bialgebras (inserters), [Joachim Lambek, 1970] is given. We also discuss various properties and examples of Mendler dialgebras, including higher-order abstract syntax which is paradigmatic for definitions of mixed variance. Generally, we regard the paper as a contribution to a more systematic understanding of the relation between higher-order and first-order inference rules. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Stephan Alexander Spahn 2026 Is Part Of LIPIcs, Volume 384, 31st International Conference on Types for Proofs and Programs (TYPES 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2025.15 urn:nbn:de:0030-drops-270338 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.15 eng https://creativecommons.org/licenses/by/4.0/legalcode