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.
CITATION STYLE
Tiuryn, J., & Wand, M. (1996). Untyped lambda-calculus with input-output. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1059, pp. 317–329). Springer Verlag. https://doi.org/10.1007/3-540-61064-2_46
Mendeley helps you to discover research relevant for your work.