A Non-Deterministic Call-by-Need Lambda Calculus

Abstract

In this paper we present a non-deterministic call-by-need (untyped) lambda calculus X,d with a constant choice and a let-syntax that models sharing. Our main result is that Xnd has the nice operational properties of the standard lambda calculus: confluence on sets of expressions, and normal or-der reduction is sufficient to reach head normal form. Us-ing a strong contextual equivalence we show correctness of several program transformations. In particular of lambda-lifting using deterministic maximal free expressions. These results show that And is a new and also natural combination of non-determinism and lambda-calculus, which has a lot of opportunities for parallel evaluation. An intended application of And is as a foundation for compil-ing lazy functional programming languages with I/O based on direct calls. The set of correct program transformations can be rigorously distinguished from non-correct ones. All program transformations are permitted with the slight ex-ception that for transformations like common subexpression elimination and lambda-lifting with maximal free expres-sions the involved subexpressions have to be deterministic ones. 1