Nondeterminism Effect: Plural / Choice Alternatives

@cite{charlow-2019} @cite{charlow-2021} @cite{muskens-1996}

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.

This file consolidates two former modules:

• NDMeaning (Set monad on meanings) — was Dynamic/Nondeterminism/Basic.lean
• liftPW / lowerPW (Charlow's ↑ / ↓ pointwise/collectivized bridge) — was Dynamic/Nondeterminism/PointwiseUpdate.lean

The companion paper-level study (Charlow 2019's StateCCP, distributivity, destructive-update theorems) lives in Dynamic/Nondeterminism/Charlow2019.lean pending Phase 4e of the discourse restructure (where it migrates to Phenomena/Anaphora/Studies/Charlow2019.lean).

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'}

Connects the pointwise DRS S := S → S → Prop type (Dynamic Ty2, @cite{muskens-1996}) to the update-theoretic StateCCP W E := State W E → State W E type.

The key operations are @cite{charlow-2021}'s ↑ (lift) and ↓ (lower):

• liftPW: promotes a pointwise DRS to a context-level update
• lowerPW: extracts a pointwise relation from a context update

The central result: liftPW D is always distributive, meaning pointwise meanings can never produce irreducibly context-level effects. Cumulative readings require non-distributive M_v, which lives only in StateCCP.

def Semantics.Dynamic.Core.PointwiseUpdate.liftPW {W : Type u_1} {E : Type u_2} (D : DRS (Assignment E)) : StateCCP W E

Charlow's ↑ (equation 76): lift a pointwise DRS to an update on states. liftPW D s = {⟨w, h⟩ | ∃ ⟨w, g⟩ ∈ s, D g h} Each world-assignment pair in the output comes from applying D to some input assignment in s, preserving the world.

Equations

• Semantics.Dynamic.Core.PointwiseUpdate.liftPW D s = {p : W × Core.Assignment E | ∃ (q : W × Core.Assignment E), q ∈ s ∧ p.fst = q.fst ∧ D q.snd p.snd}

def Semantics.Dynamic.Core.PointwiseUpdate.lowerPW {W : Type u_1} {E : Type u_2} (K : StateCCP W E) (w₀ : W) : DRS (Assignment E)

Charlow's ↓ (equation 77): extract a pointwise DRS from a state update. Evaluates K on a singleton context at an arbitrary world.

Equations

• Semantics.Dynamic.Core.PointwiseUpdate.lowerPW K w₀ g h = ((w₀, h) ∈ K {(w₀, g)})

theorem Semantics.Dynamic.Core.PointwiseUpdate.lowerPW_liftPW {W : Type u_1} {E : Type u_2} (D : DRS (Assignment E)) (w₀ : W) : lowerPW (liftPW D) w₀ = D

Round-trip identity: lowering a lifted DRS recovers the original.

↓(↑D) = D because the singleton context {(w₀, g)} passes through ↑ with only (w₀, g) as witness, leaving exactly the pairs h with D g h.

theorem Semantics.Dynamic.Core.PointwiseUpdate.liftPW_injective {W : Type u_1} {E : Type u_2} [Nonempty W] (D₁ D₂ : DRS (Assignment E)) (h : liftPW D₁ = liftPW D₂) : D₁ = D₂

↑ is injective: distinct DRSs yield distinct state updates.

Follows from the round-trip: D = ↓(↑D), so ↑D₁ = ↑D₂ implies D₁ = ↓(↑D₁) = ↓(↑D₂) = D₂. Requires W to be nonempty for the lowering witness world.

theorem Semantics.Dynamic.Core.PointwiseUpdate.liftPW_preserves_distributive {W : Type u_1} {E : Type u_2} (D : DRS (Assignment E)) : IsDistributive (liftPW D)

Lifted pointwise DRSs are always distributive (@cite{charlow-2021}, §6, key lemma).

↑D processes each element of the input state independently — the output at p depends only on whether some q ∈ s satisfies D q.2 p.2 with matching world p.1 = q.1. This is exactly the singleton decomposition (↑D)(s) = ⋃_{i∈s} (↑D)({i}), which is the definition of distributivity.

theorem Semantics.Dynamic.Core.PointwiseUpdate.liftPW_lowerPW_not_id {W : Type u_1} {E : Type u_2} [Nonempty W] [Nonempty E] : ∃ (K : StateCCP W E), ∃ (w₀ : W), liftPW (lowerPW K w₀) ≠ K

↑↓ ≠ id: there exist irreducibly update-theoretic meanings K such that liftPW (lowerPW K w₀) ≠ K.

The simplest witness is K _ = {(w₀, g₀)} (constant function ignoring input). Then K ∅ = {(w₀, g₀)}, but liftPW (lowerPW K w₀) ∅ = ∅ because ↑ has no input pairs to draw.

Requires Nonempty W and Nonempty E to construct the witness.