2026-07-21T23:17:38Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18817 2024-03-06T11:01:56Z ddc:004 open_access

Completeness for Categories of Generalized Automata ((Co)algebraic pearls) Boccali, Guido Laretto, Andrea Loregian, Fosco Luneia, Stefano Deterministic automata Moore machines Mealy machines coalgebras cocomplete category We present a slick proof of completeness and cocompleteness for categories of F-automata, where the span of maps E ←d E⊗ I s→ O that usually defines a deterministic automaton of input I and output O in a monoidal category (K,⊗) is replaced by a span E ← FE → O for a generic endofunctor F : K → K of a generic category K: these automata exist in their "Mealy" and "Moore" version and form categories F-Mly and F-Mre; such categories can be presented as strict 2-pullbacks in Cat and whenever F is a left adjoint, both F-Mly and F-Mre admit all limits and colimits that K admits. We mechanize our main results using the proof assistant Agda and the library https://github.com/agda/agda-categories. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Guido Boccali and Andrea Laretto and Fosco Loregian and Stefano Luneia 2023 Is Part Of LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CALCO.2023.20 urn:nbn:de:0030-drops-188174 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.20 eng https://creativecommons.org/licenses/by/4.0/legalcode