NONDETERMINISTIC EXTENSIONS OF UNTYPED LAMBDA-CALCULUS

The main concern of this paper is the interplay between functionality and nondeterminism. We ask whether the analysis of parallelism in term s of sequentiality and nondeterminism, which is usual in the algebraic treatment of concurrency, remains correct in the presence of function al application and abstraction, We argue in favour of a distinction be tween nondeterminism and parallelism, due to the conjunctive nature of the former in contrast to the disjunctive character of the latter. Th is is the basis of our analysis of the operational and denotational se mantics of the nondeterministic lambda-calculus, which is the classica l calculus plus a choice operator, and of our election of bounded inde terminacy as the semantic counterpart of conjunctive nondeterminism. T his leads to operational semantics based on the idea of must preorder, coming from the classical theory of solvability and from the theory o f process algebras. To characterize this relation, we build a model us ing the inverse limit construction over nondeterministic algebras, and we prove it fully abstract using a generalization of Bohm trees. We f urther prove conservativity theorems for the equational theory of the model and for other theories related to nondeterministic lambda-calcul us with respect to classical lambda-theories. (C) 1995 Academic Press, Inc.