Nondeterministic Extensions of Untyped λ-Calculus

The main concern of this paper is the study of the interplay between functionality and non determinism. Indeed the first question we ask is whether the analysis of parallelism in terms of sequentiality and non determinism which is usual in the algebraic treatment of concurrency remains correct in presence of functional application and abstraction We identify non determinism in the setting of lambda-calculus with the absence of the Church-Rosser property plus the inconsistency of the equational theory obtained by the symmetric closure of the reduction relation. We argue in favour of a distinction between non determinism and parallelism due to the conjunctive nature of the former in contrast to the disjunctive character of the latter. This is the basis of our analysis of the operational and denotational semantics of non deterministic lambda-calculus, which is the classical calculus plus a choice operator, and of our election of bounded indeterminacy as the semantical counterpart of conjunctive non determinism. This leads to operational semantics based on the idea of must preorder, coming from the the classical theory of solvability and from the theory of process algebras. To characterize this relation, we build a model using the inverse limit construction over non deterministic algebras, and we prove it fully abstract using a generalization of Boehm trees. We further prove conservativity theorems for the equational theory of the model and for other theories related to non deterministic lambda-calculus, with respect to classical lambda-heories.