Distributive semantics for nondeterministic typed λ-calculi

AbstractIn this paper we present a semantics for nondeterministic applicative languages based on the typed λ-calculus with a binary choice operator. It provides a natural interpretation of the choice operation and shows its relation with abstraction and application. A distinguishing feature of the semantics, that can also be considered as one of its motivations, is the preservation of deterministic equivalences, in a sense to be made precise in the paper.On the operational side, the semantics relies on a rewriting system, which follows an outermost strategy with sharing of arguments. The denotational counterpart is the distributivity of application with respect to the union operation.We present a full technical treatment of the case when sharing/distributivity is assumed with respect to ground arguments only and we have exemplified the approach on the language NDPCF, for which we show that a denotational semantics exists which is fully abstract with respect to the operational one. It is based on a construction of an intrinsically fully abstract model w.r.t. an interpretation of basic constant and function symbols