Nondeterminism Effect: Plural/Choice Alternatives

@cite{charlow-2019}

The nondeterminism effect models indefinites as introducing sets of alternatives rather than single values. This underlies:

• Indefinites as choice functions
• Plural/cumulative readings
• Set-valued update (pointwise lifting)

The key type is Set α (or List α for computational purposes) — meanings are sets of possible values rather than single values.

Submodules

• PointwiseUpdate: Charlow's ↑/↓ bridge between pointwise and collectivized update
• Charlow2019: StateCCP, distributivity for nondeterministic dynamic semantics

def Semantics.Dynamic.Nondeterminism.NDMeaning (α : Type u_1) (β : Type u_2) : Type (max u_1 u_2)

A nondeterministic meaning: produces a set of possible outputs.

This is the semantic type for indefinites — "a man" denotes the set of all men, and the nondeterminism effect handles choice.

Equations

• Semantics.Dynamic.Nondeterminism.NDMeaning α β = (α → Set β)

def Semantics.Dynamic.Nondeterminism.NDMeaning.bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} (m : NDMeaning α β) (f : β → Set γ) : NDMeaning α γ

Bind for the nondeterminism monad (Set).

Sequencing nondeterministic computations: for each possible value from the first computation, run the second and collect all results.

Equations

• m.bind f a = {c : γ | ∃ (b : β), b ∈ m a ∧ c ∈ f b}

def Semantics.Dynamic.Nondeterminism.NDMeaning.pure {α : Type u_1} {β : Type u_2} (b : β) : NDMeaning α β

Pure/return for nondeterminism: a single deterministic value.

Equations

• Semantics.Dynamic.Nondeterminism.NDMeaning.pure b x✝ = {b}

def Semantics.Dynamic.Nondeterminism.NDMeaning.alt {α : Type u_1} {β : Type u_2} (m₁ m₂ : NDMeaning α β) : NDMeaning α β

Alternative/choice: union of two nondeterministic meanings.

Equations

• m₁.alt m₂ a = m₁ a ∪ m₂ a

def Semantics.Dynamic.Nondeterminism.NDMeaning.maximize {α : Type u_1} {β : Type u_2} (m : NDMeaning α β) (better : β → β → Prop) : NDMeaning α β

Maximization: select maximal elements from a nondeterministic meaning with respect to some ordering. Used for cumulative readings.

Equations

• m.maximize better a = {b : β | b ∈ m a ∧ ∀ (b' : β), b' ∈ m a → ¬better b b'}