3. 状態遷移系（システム）の基礎理論としての余代数

Jan Rutten の Universal coalgebra: a theory of systems によると

Jan Rutten's Universal coalgebra

Abstract:
In the semantics of programming, finite data types such as finite lists, have traditionally been modelled by initial algebras. Later final coalgebras were used in order to deal with infinite data types. Coalgebras, which are the dual of algebras, turned out to be suited, moreover, as models for certain types of automata and more generally, for (transition and dynamical) systems. An important property of initial algebras is that they satisfy the familiar principle of induction. Such a principle was missing for coalgebras until the work of Aczel (Non-Well-Founded sets, CSLI Leethre Notes, Vol. 14, center for the study of Languages and information, Stanford, 1988) on a theory of non-wellfounded sets, in which he introduced a proof principle nowadays called coinduction. It was formulated in terms of bisimulation, a notion originally stemming from the world of concurrent programming languages. Using the notion of coalgebra homomorphism, the denition of bisimulation on coalgebras can be shown to be formally dual to that of congruence on algebras. Thus, the three basic notions of universal algebra: algebra, homomorphism of algebras, and congruence, turn out to correspond to coalgebra, homomorphism of coalgebras, and bisimulation, respectively. In this paper, the latter are taken as the basic ingredients of a theory called universal coalgebra. Some standard results from universal algebra are reformulated (using the aforementioned correspondence) and proved for a large class of coalgebras, leading to a series of results on, e.g., the lattices of subcoalgebrasand bisimulations, simple coalgebras and coinduction, and a covariety theorem for coalgebras similar to Birkho's variety theorem.

• • -

1. Introduction
In the semantics of programming, data types are usually presented as algebras (cf.[24, 47]). For instance, the collection of nite words A over some alphabet A is an algebra

hA;  : (1 + (AA))!Ai;

where  maps  (the sole element of the singleton set 1=fg) to the empty word and a pair ha;wi to a
w. This example is typical in that A is an initial algebra. Initial algebras are generalizations of least xed points, and satisfy familiar inductive proof
and denition principles. For innite data structures, the dual notion of coalgebra has been used as an alternative to the algebraic approach [6]. For instance, the set A1 of nite and innite
words over A can be described by the pair

hA1;
: A1!(1 + (AA1))i;

where maps the empty word to  and a non-empty word to the pair consisting of its head (the rst letter) and tail (the remainder). It is a coalgebra because is a function from the carrier set A1 to an expression involving A1, that is, 1 + (AA1), as opposed to the algebra above, where  was a function into the carrier set A. Again
the example is typical because A1 is a nal coalgebra, which generalizes the notion of greatest xed point.