Categories of coalgebras with monadic homomorphisms. (English) Zbl 1445.68119

Bonsangue, M. (ed.), Coalgebraic methods in computer science. 12th IFIP WG 1.3 international workshop, CMCS 2014, colocated with ETAPS 2014, Grenoble, France, April 5–6, 2014. Revised selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 8446, 151-167 (2014).
Summary: Abstract graph transformation approaches traditionally consider graph structures as algebras over signatures where all function symbols are unary.{
}Attributed graphs, with attributes taken from (term) algebras over arbitrary signatures do not fit directly into this kind of transformation approach, since algebras containing function symbols taking two or more arguments do not allow component-wise construction of pushouts. We show how shifting from the algebraic view to a coalgebraic view of graph structures opens up additional flexibility, and enables treating term algebras over arbitrary signatures in essentially the same way as unstructured label sets. We integrate substitution into our coalgebra homomorphisms by identifying a factoring over the term monad, and obtain a flexible framework for graphs with symbolic attributes. This allows us to prove that pushouts can be constructed for homomorphisms with unifiable substitution components.{
}We formalised the presented development in Agda, which crucially aided the exploration of the complex interaction of the different functors, and enables us to report all theorems as mechanically verified.
For the entire collection see [Zbl 1318.68010].


68Q42 Grammars and rewriting systems
18C15 Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
68V20 Formalization of mathematics in connection with theorem provers


Agda; CASL; RATH-Agda
Full Text: DOI Link