Distributive semantics for nondeterministic typed \(\lambda\)-calculi (Q760418)

The paper presents a treatment of applicative languages based on the typed lambda-calculus enriched with a nondeterministic binary choice operator. The main aim of the paper is to give a semantics for the nondeterministic typed lambda-calculus which preserves the corresponding deterministic equivalences from the calculus without the nondeterministic choice operator. This aim is realized via giving an operational semantics of the calculus, using sharing technique preventing undesired duplicating of nondeterministic redexes, and the corresponding fully abstract (in the sense of Milner) denotational semantics, developing a theory of distributive models with the distributivity as the denotational counterpart of the sharing. The paper provides extensive motivations and the approach is exemplified on the language NDPCF.