A structural co-induction theorem
The Structural Induction Theorem (Lehmann and Smyth, 1981; Plotkin, 1981) characterizes initial F-algebras of locally continuous functors F on the category of cpo’s with strict and continuous maps. Here a dual of that theorem is presented, giving a number of equivalent characterizations of final coalgebras of such functors. In particular, final coalgebras are order strongly-extensional (sometimes called internal full abstractness): the order is the union of all (ordered) F-bisimulations. (Since the initial fixed point for locally continuous functors is also final, both theorems apply.) Further, a similar co-induction theorem is given for a category of complete metric spaces and locally contracting functors.
|International Conference on Mathematical Foundations of Programming Semantics|
|Organisation||Centrum Wiskunde & Informatica, Amsterdam, The Netherlands|
Rutten, J.J.M.M. (1994). A structural co-induction theorem. In Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence (pp. 83–102).