Lazy Lambda Calculus: Theories, Models and Local Structure Characterisation

Lambda Calculus is commonly thought to be the basis for functional programming. However, there is a fundamental mismatch between the "standard" theory of sensible Lambda Calculus (as in e.g. [Bar84]) and the practice of lazy evaluation which is a distinctive feature of functional programming. This paper proposes modification of a number of key notions in the sensible theory along the lines of laziness. Starting from the strongly unsolvables as the meaningless terms, we define and investigate properties of lazy (or weakly sensible) λ-theories, lazy λ-models and a number of lazy behavioural preorders on λ-terms. In the second part, we show that all these notions have a natural place in a class of lazy pse-models. A major result of this paper is a new local structure theorem for lazy pse-models. This characterizes the ordering between denotations of λ-terms in the model by a new lazy behavioural preorder