| Koht / Place: | Ruum B 216,
Room B 216, |
Küberneetika Instituut, Akadeemia tee 21, Tallinn
Institute of Cybernetics, Akadeemia tee 21, Tallinn, Estonia |
|
| Aeg / Time: | Teisipäev,
Tuesday, |
12. märts, 2002,
March 12, 2002, |
11:00 - 12:30, 14:00 - 16:00
11:00 - 12:30, 14:00 - 16:00 |
| Esinejad / Speakers: | 11:00 - 12:30
14:00 - - 16:00 |
Heinz-Peter GUMM,
Falk BARTELS, Tarmo UUSTALU, |
Philipps-Universität Marburg
CWI, Amsterdam IoC, Tallinn |
Properties of the type functor F influence strongly the structure theory of the class Set_F of all F-coalgebras. In the early days of universal coalgebra, authors assumed F to preserve weak pullbacks. Subsequently, it has turned out that the core theory can be developed without this assumption.
Still, preservation properties of F entail additional structure theoretical consequences. If, for instance, F preserves weak pullbacks, then the largest bisimulation on any coalgebras is transitive, indistinguishability is the same as observational equivalence, congruences are bisimulations and monos are injective.
We separately consider the cases where F weakly preserves pullbacks, preimages, kernels, and coequalizers. In each case we find structural properties for the class of all F-coalgebras that are determined by such preservation assumptions.
http://www.mathematik.uni-marburg.de/~gumm/
State based dynamical systems can often be modelled as F-coalgebras for a functor F describing the type of behaviour under consideration. Final coalgebras provide an abstract domain for these processes together with the coinduction definition and proof principle. Unfortunately, many system specifications do not immediately fit into this basic coinductive definition format and not all proofs about behavioural equivalence can be stated smoothly in terms of the original coinduction proof principle.
This talk will present a framework for deriving generalized formats. Several known extensions - like e.g. primitive corecursion - arise as instances of it. Furthermore, it guarantees the unique existence of solutions to guarded recursive equations and the validity of the up-to-context proof principle for operators specifiable in a categorical format introduced by Turi and Plotkin. The latter format arose as an abstract presentation of GSOS rules.
It is well known that, given an endofunctor H on a category C, the initial (A + H -)-algebras for different objects A of C (if they all exist), i.e., the algebras of wellfounded H-branching trees-with-variables over different variable supplies A, give rise to a monad with substitution as the extension operation. A similar monad, but with the additional property of being "iterative", is induced by the inverses of the final (A + H -)-coalgebras (if they exist), i.e., the algebras of non-wellfounded H-branching trees-with-variables. Aczel, Adamek, Velebil (2001) have given one very neat generalization of these facts. We consider a different one: if M is a bifunctor such that the functors M(-, X) uniformly carry a monad structure, then the initial M(A, -)-algebras (if existing) give rise to a monad and the inverses of the final M(A, -)-coalgebras (if existing) yield an "iterative" monad.
Info: Tarmo Uustalu, (0) 620 4250.