A mathematical semantics for a nondeterministic typed λ-calculus

This paper is concerned with the problems encountered in defining the semantics of nondeterministic algorithms. A nondeterministic control structure is added to a typed λ-calculus and the usual operational semantics for the deterministic language is generalized to take into account the more complex behaviour of nondeterministic algorithms. A mathematical model is then given for the language and the relationship between the denotational and operational semantics is explored.