Coinductive characterizations of applicative structures

We discuss new ways of characterizing, as maximal fixed points of monotone operators, observational congruences on λ-terms and, more generally, equivalences on applicative structures. These characterizations naturally induce new forms of coinduction principles for reasoning on program equivalences, which are not based on Abramsky's applicative bisimulation. We discuss, in particular, what we call the cartesian coinduction principle, which arises when we exploit the elementary observation that functional behaviours can be expressed as cartesian graphs. Using the paradigm of final semantics, the soundness of this principle over an applicative structure can be expressed easily by saying that the applicative structure can be construed as a strongly extensional coalgebra for the functor ([Pscr ](- × -))[oplus ]([Pscr ](- × -)). In this paper we present two general methods for showing the soundness of this principle. The first applies to approximable applicative structures – many CPO λ-models in the literature and the corresponding quotient models of indexed terms turn out to be approximable applicative structures. The second method is based on Howe's congruence candidates, which applies to many observational equivalences. Structures satisfying cartesian coinduction are precisely those applicative structures that can be modelled using the standard set-theoretic application in non-wellfounded theories of sets, where the Foundation Axiom is replaced by the Axiom X1 of Forti and Honsell.