Semantical Analysis Of Perpetual Strategies In Lambda-Calculus

Perpetual strategies in lambda-calculus are analyzed from a semantical perspective. This is achieved using suitable denotational models, computationally adequate with respect to the observational (operational) equivalence, approximate to(p), induced by perpetual strategies. A necessary and sufficient condition is given for an omega-algebraic lattice, isomorphic to the space of its strict continuous self-maps, to be computationally adequate w.r.t. approximate to(p). While many such models exist, it is shown, however, that none is fully abstract w.r.t. approximate to(p). The computationally adequate lattice model D-p is studied in detail. It is used to give a semantical proof of the Conservation Theorem for the lambda-calculus, and to provide coinductive and mixed inductive-coinductive characterizations of approximate to(p). The coinductive characterization allows to show that the term model of approximate to(p) is a denotational model; this yields a new characterization of perpetual redexes in lambda-calculus.