Observational ultraproducts of polynomial coalgebras. (Q1408860)

Modelling data structures such as lists, streams and trees, automata, classes (in object-oriented programming) can be performed by considering a \(T\)-coalgebra \((A, \alpha)\) with \(A\) a set and \(\alpha\) a function \(A \to TA\). \(A\) is the set of states and \(\alpha\) is the transition structure. Polynomial coalgebras are those where \(T\) is a polynomial functor (obtained from constant-valued functors and identity by products, exponentials with constant exponent and coproducts). Such functors constructed from some fixed given set comprise the examples above; elements of these sets are ``observable''. It was previously established that the Boolean combinations of equations between observable terms form a natural language of observable formulas for specifying coalgebraic properties. Observable formulas provide the appropriate language for polynomial coalgebras. A notion of bisimulation is defined. It is known that in classical equational logic a class of algebras is the class of all models of some set of equations iff it is closed under homeomorphic images, subalgebras and direct products -- the so-called ``variety theorem'' of Birkhoff. The present paper proves an analogous result for polynomial coalgebras. More precisely it proves the following: Theorem: A class of polynomial coalgebras is the class Mod\,\(\Phi\) of all models of a set \(\Phi\) of rigid observable formulas if and only if it is closed under images of bisimulation, relations, disjoint unions, and observational ultrapowers. Further, the associated version of Łos' Theorem and some of its consequences are established.