Tuesday, 12 March 2002, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B216
Abstract: 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.
Tarmo Uustalu