Two-Dimensional Alternative Meanings

[Roo85] [Roo92] [KS20]

The O-value / A-value pair from Rooth-style alternative semantics. Every expression has an ordinary denotation (oValue) and an alternatives set (aValue); focus features and operators manipulate the latter while typically preserving the former.

This file isolates the bare data structure. Symmetry-based refinements ([FK11]) live in Symmetric.lean; structural alternatives ([Kat07]) live in Structural.lean; [FoC]/[G] feature semantics live in Semantics/Focus/.

structure Alternatives.AltMeaning (α : Type u_1) : Type u_1

Two-dimensional meaning in [Roo92]-style alternative semantics. Every expression has an O-value and an A-value.

[KS20] §3, §8.

• oValue : α

  O(rdinary)-value: the actual denotation

• aValue : List α

  A(lternatives)-value: the set of alternatives (including oValue)

def Alternatives.AltMeaning.unfeatured {α : Type u_1} (x : α) : AltMeaning α

The O-value of a non-featured expression equals its ordinary denotation. The A-value of a non-featured expression is a singleton containing its O-value (no alternatives evoked).

Equations

• Alternatives.AltMeaning.unfeatured x = { oValue := x, aValue := [x] }

@[simp]

theorem Alternatives.AltMeaning.unfeatured_oValue {α : Type u_1} (x : α) : (unfeatured x).oValue = x

@[simp]

theorem Alternatives.AltMeaning.unfeatured_aValue {α : Type u_1} (x : α) : (unfeatured x).aValue = [x]

def Alternatives.AltMeaning.aSet {α : Type u_1} (m : AltMeaning α) : Set α

The alternative set as a Set — the theory-side carrier; aValue is its list presentation.

Equations

• m.aSet = {a : α | a ∈ m.aValue}

@[simp]

theorem Alternatives.AltMeaning.mem_aSet {α : Type u_1} {m : AltMeaning α} {a : α} : a ∈ m.aSet ↔ a ∈ m.aValue

@[simp]

theorem Alternatives.AltMeaning.unfeatured_aSet {α : Type u_1} (x : α) : (unfeatured x).aSet = {x}

The composition engine

Alternative semantics composes pointwise ([Roo85]): the O-value applies ordinarily while the A-value collects applications of alternative functions to alternative arguments (Hamblin functional application). AltMeaning is the product of the identity and list monads, so the engine is a lawful Monad: pure is unfeatured, <$>/<*> are the recursive clauses of the two-dimensional semantics, and oValue is a monad morphism onto the ordinary dimension.

@[implicit_reducible]

instance Alternatives.AltMeaning.instMonad : Monad AltMeaning

Equations

• One or more equations did not get rendered due to their size.

instance Alternatives.AltMeaning.instLawfulMonad : LawfulMonad AltMeaning

@[simp]

theorem Alternatives.AltMeaning.oValue_pure {α : Type u} (x : α) : (pure x).oValue = x

The O-projection is a monad morphism: composition preserves the ordinary dimension.

@[simp]

theorem Alternatives.AltMeaning.oValue_bind {α β : Type u} (m : AltMeaning α) (f : α → AltMeaning β) : (m >>= f).oValue = (f m.oValue).oValue

@[simp]

theorem Alternatives.AltMeaning.oValue_map {α β : Type u} (f : α → β) (m : AltMeaning α) : (f <$> m).oValue = f m.oValue

@[simp]

theorem Alternatives.AltMeaning.oValue_seq {α β : Type u} (mf : AltMeaning (α → β)) (ma : AltMeaning α) : (mf <*> ma).oValue = mf.oValue ma.oValue

@[simp]

theorem Alternatives.AltMeaning.mem_aSet_map {α β : Type u} {f : α → β} {m : AltMeaning α} {b : β} : b ∈ (f <$> m).aSet ↔ ∃ (a : α), a ∈ m.aSet ∧ f a = b

Membership in a mapped A-set: the image law of the engine.

@[simp]

theorem Alternatives.AltMeaning.mem_aSet_seq {α β : Type u} {mf : AltMeaning (α → β)} {ma : AltMeaning α} {b : β} : b ∈ (mf <*> ma).aSet ↔ ∃ (g : α → β), g ∈ mf.aSet ∧ ∃ (a : α), a ∈ ma.aSet ∧ g a = b

Membership in an applied A-set: Hamblin functional application.

aSet as a morphism into the Set applicative

Together with the oValue monad-morphism laws above, these exhibit the alternatives monad as a span Id ⟵ AltMeaning ⟶ Set: ordinary meaning and focal-target set are its two structure-preserving projections. Hamblin application is the image of <*> under aSet.

theorem Alternatives.AltMeaning.aSet_pure {α : Type u} (a : α) : (pure a).aSet = {a}

theorem Alternatives.AltMeaning.aSet_seq {α β : Type u} (mf : AltMeaning (α → β)) (ma : AltMeaning α) : (mf <*> ma).aSet = mf.aSet.seq ma.aSet

theorem Alternatives.AltMeaning.aSet_bind {α β : Type u} (m : AltMeaning α) (f : α → AltMeaning β) : (m >>= f).aSet = {b : β | ∃ (a : α), a ∈ m.aSet ∧ b ∈ (f a).aSet}

def Alternatives.AltMeaning.WellFormed {α : Type u} (m : AltMeaning α) : Prop

Rooth's containment constraint: the A-value contains the O-value.

Equations

• m.WellFormed = (m.oValue ∈ m.aValue)

theorem Alternatives.AltMeaning.WellFormed.unfeatured {α : Type u} (x : α) : (AltMeaning.unfeatured x).WellFormed

theorem Alternatives.AltMeaning.WellFormed.bind {α β : Type u} {m : AltMeaning α} {f : α → AltMeaning β} (hm : m.WellFormed) (hf : ∀ (a : α), (f a).WellFormed) : (m >>= f).WellFormed

Composition preserves well-formedness.

theorem Alternatives.AltMeaning.WellFormed.map {α β : Type u} {f : α → β} {m : AltMeaning α} (hm : m.WellFormed) : (f <$> m).WellFormed

Givenness

def Alternatives.AltMeaning.Given {α : Type u} (m : AltMeaning α) (a : α) : Prop

Given with respect to a: the alternatives have collapsed to the singleton {a} ([KS20] (46)).

Equations

• m.Given a = (m.aSet = {a})

theorem Alternatives.AltMeaning.Given.unfeatured {α : Type u} (x : α) : (AltMeaning.unfeatured x).Given x

Unfeatured meanings are Given with respect to their value.

theorem Alternatives.AltMeaning.Given.aSet_seq {α β : Type u} {mf : AltMeaning (α → β)} {f : α → β} (h : mf.Given f) (ma : AltMeaning α) : (mf <*> ma).aSet = f '' ma.aSet

A Given function collapses Hamblin composition to application on the argument's alternatives — deaccented material contributes exactly its ordinary value.