Nondeterministic Extensions of Untyped λ-Calculus

AbstractThe main concern of this paper is the interplay between functionality and nondeterminism. We ask whether the analysis of parallelism in terms of sequentiality and nondeterminism, which is usual in the algebraic treatment of concurrency, remains correct in the presence of functional application and abstraction, We argue in favour of a distinction between nondeterminism 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 the nondeterministic λ-calculus, which is the classical calculus plus a choice operator, and of our election of bounded indeterminacy as the semantic counterpart of conjunctive nondeterminism. This leads to operational semantics based on the idea of must preorder, coming from 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 nondeterministic algebras, and we prove it fully abstract using a generalization of Böhm trees. We further prove conservativity theorems for the equational theory of the model and for other theories related to nondeterministic λ-calculus with respect to classical λ-theories