Proper Functors and Fixed Points for Finite Behaviour
The rational fixed point of a set functor is well-known to capture the behaviour of finite coalgebras. In this paper we consider functors on algebraic categories. For them the rational fixed point may no longer be fully abstract, i.e. a subcoalgebra of the final coalgebra. Inspired by \'Esik an...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2018-09-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/4822/pdf |
| _version_ | 1827322834643320832 |
|---|---|
| author | Stefan Milius |
| author_facet | Stefan Milius |
| author_sort | Stefan Milius |
| collection | DOAJ |
| description | The rational fixed point of a set functor is well-known to capture the
behaviour of finite coalgebras. In this paper we consider functors on algebraic
categories. For them the rational fixed point may no longer be fully abstract,
i.e. a subcoalgebra of the final coalgebra. Inspired by \'Esik and Maletti's
notion of a proper semiring, we introduce the notion of a proper functor. We
show that for proper functors the rational fixed point is determined as the
colimit of all coalgebras with a free finitely generated algebra as carrier and
it is a subcoalgebra of the final coalgebra. Moreover, we prove that a functor
is proper if and only if that colimit is a subcoalgebra of the final coalgebra.
These results serve as technical tools for soundness and completeness proofs
for coalgebraic regular expression calculi, e.g. for weighted automata. |
| first_indexed | 2024-04-25T01:35:07Z |
| format | Article |
| id | doaj.art-ff8b9357a44743fbbdd4d12dae78f94e |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:35:07Z |
| publishDate | 2018-09-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-ff8b9357a44743fbbdd4d12dae78f94e2024-03-08T10:02:03ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742018-09-01Volume 14, Issue 310.23638/LMCS-14(3:22)20184822Proper Functors and Fixed Points for Finite BehaviourStefan MiliusThe rational fixed point of a set functor is well-known to capture the behaviour of finite coalgebras. In this paper we consider functors on algebraic categories. For them the rational fixed point may no longer be fully abstract, i.e. a subcoalgebra of the final coalgebra. Inspired by \'Esik and Maletti's notion of a proper semiring, we introduce the notion of a proper functor. We show that for proper functors the rational fixed point is determined as the colimit of all coalgebras with a free finitely generated algebra as carrier and it is a subcoalgebra of the final coalgebra. Moreover, we prove that a functor is proper if and only if that colimit is a subcoalgebra of the final coalgebra. These results serve as technical tools for soundness and completeness proofs for coalgebraic regular expression calculi, e.g. for weighted automata.https://lmcs.episciences.org/4822/pdfcomputer science - logic in computer science |
| spellingShingle | Stefan Milius Proper Functors and Fixed Points for Finite Behaviour Logical Methods in Computer Science computer science - logic in computer science |
| title | Proper Functors and Fixed Points for Finite Behaviour |
| title_full | Proper Functors and Fixed Points for Finite Behaviour |
| title_fullStr | Proper Functors and Fixed Points for Finite Behaviour |
| title_full_unstemmed | Proper Functors and Fixed Points for Finite Behaviour |
| title_short | Proper Functors and Fixed Points for Finite Behaviour |
| title_sort | proper functors and fixed points for finite behaviour |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/4822/pdf |
| work_keys_str_mv | AT stefanmilius properfunctorsandfixedpointsforfinitebehaviour |