Untyped Lambda-Calculus with Input-Output

. We introduce an untyped -calculus with input-output, based on Gordon's continuation-passing model of input-output. This calculus is intended to allow the classification of possibly infinite input-output behaviors, such as those required for servers or distributed systems. We define two terms to be operationally approximate iff they have similar behaviors in any context. We then define a notion of applicative approximation and show that it coincides with operational approximation for these new behaviors. Last, we consider the theory of pure -terms under this notion of operational equivalence. 1 Introduction In the study of the operational behavior of languages, the standard paradigm for studying equivalence of terms begins by setting up some relatively weak notion of behavior (or immediate observation). For PCF [10], this is generally taken to be convergence to an integer constant; for the untyped -calculus, this can be taken to be reducibility to a head normal form (Bohm) or to an a..