A COINDUCTION PRINCIPLE FOR RECURSIVE DATA-TYPES BASED ON BISIMULATION

The concept of bisimulation from concurrency theory is used to reason about recursively defined data types. From two strong-extensionality t heorems stating that the equality (resp. inequality) relation is maxim al among all bisimulations, a proof principle for the final coalgebra of an endofunctor on a category of data types (resp. domains) is obtai ned. As an application of the theory developed, an internal full abstr action result (in the sense of S. Abramsky and C.-H. L. Ong [Inform. a nd Comput. 105, 159-267 (1993)] for the canonical model of the untyped call-by-value lambda-calculus is proved. Also, the operational notion of bisimulation and the denotational notion of final semantics are re lated by means of conditions under which both coincide. (C) 1996 Acade mic Press, Inc.