Meanings with alternatives

A meaning in alternative semantics is a pair: an ordinary denotation, and a set of alternatives that focus features and operators manipulate while leaving the ordinary denotation alone. WithAlternatives is that pair. It is the product of the identity monad and the set monad, so the two-dimensional recursion of alternative semantics is <$> and <*> of a lawful Monad, and the two dimensions are its two monad morphisms.

Symmetry-based refinements live in Symmetric.lean, structural alternatives in Structural.lean, and the semantics of the focus and givenness features in Semantics/Focus/.

Main definitions

• WithAlternatives — an ordinary value together with the alternatives it evokes
• WithAlternatives.WellFormed — the containment constraint: the alternatives include the ordinary value
• WithAlternatives.Given — the alternatives have collapsed to a singleton

Main results

• ordinary_seq, mem_alternatives_seq — the two dimensions of Hamblin composition
• alternatives_seq — the alternatives of an application are those of the Set applicative
• Given.alternatives_seq — a Given function contributes only its ordinary value

References

• [rooth-1985]
• [rooth-1992]
• [kratzer-selkirk-2020]

structure WithAlternatives (α : Type u_1) : Type u_1

An ordinary denotation together with the alternatives the expression evokes ([rooth-1992]).

• ordinary : α

  The denotation the expression would have with no focus on it.

• alternatives : Set α

  The alternatives, which by Rooth's containment constraint include the ordinary value — see WellFormed, kept a predicate rather than a field so that the composition engine below is a Monad.

theorem WithAlternatives.ext_iff {α : Type u_1} {x y : WithAlternatives α} : x = y ↔ x.ordinary = y.ordinary ∧ x.alternatives = y.alternatives

theorem WithAlternatives.ext {α : Type u_1} {x y : WithAlternatives α} (ordinary : x.ordinary = y.ordinary) (alternatives : x.alternatives = y.alternatives) : x = y

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

The meaning of an expression bearing no focus feature: unfeatured x has ordinary value x and evokes only {x}.

Equations

• WithAlternatives.unfeatured x = { ordinary := x, alternatives := {x} }

@[simp]

theorem WithAlternatives.unfeatured_ordinary {α : Type u_1} (x : α) : (unfeatured x).ordinary = x

@[simp]

theorem WithAlternatives.unfeatured_alternatives {α : Type u_1} (x : α) : (unfeatured x).alternatives = {x}

The composition engine

Alternative semantics composes pointwise: the ordinary values apply to each other while the alternatives collect applications of alternative functions to alternative arguments (Hamblin functional application). pure is unfeatured and <$>/<*> are the recursive clauses of the two-dimensional semantics.

@[instance_reducible]

instance WithAlternatives.instMonad : Monad WithAlternatives

Equations

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

instance WithAlternatives.instLawfulMonad : LawfulMonad WithAlternatives

@[simp]

theorem WithAlternatives.ordinary_pure {α : Type u} (x : α) : (pure x).ordinary = x

The ordinary dimension is a monad morphism onto Id.

@[simp]

theorem WithAlternatives.ordinary_bind {α β : Type u} (m : WithAlternatives α) (f : α → WithAlternatives β) : (m >>= f).ordinary = (f m.ordinary).ordinary

@[simp]

theorem WithAlternatives.ordinary_map {α β : Type u} (f : α → β) (m : WithAlternatives α) : (f <$> m).ordinary = f m.ordinary

@[simp]

theorem WithAlternatives.ordinary_seq {α β : Type u} (mf : WithAlternatives (α → β)) (ma : WithAlternatives α) : (mf <*> ma).ordinary = mf.ordinary ma.ordinary

@[simp]

theorem WithAlternatives.mem_alternatives_map {α β : Type u} {f : α → β} {m : WithAlternatives α} {b : β} : b ∈ (f <$> m).alternatives ↔ ∃ a ∈ m.alternatives, f a = b

The alternatives of f <$> m are the images of m's alternatives.

@[simp]

theorem WithAlternatives.mem_alternatives_seq {α β : Type u} {mf : WithAlternatives (α → β)} {ma : WithAlternatives α} {b : β} : b ∈ (mf <*> ma).alternatives ↔ ∃ g ∈ mf.alternatives, ∃ a ∈ ma.alternatives, g a = b

Hamblin functional application: alternative functions apply to alternative arguments.

The alternatives as a morphism into the Set applicative

With the laws above these exhibit the monad as a span Id ⟵ WithAlternatives ⟶ Set: ordinary denotation and alternative set are its two structure-preserving projections.

theorem WithAlternatives.alternatives_pure {α : Type u} (a : α) : (pure a).alternatives = {a}

theorem WithAlternatives.alternatives_seq {α β : Type u} (mf : WithAlternatives (α → β)) (ma : WithAlternatives α) : (mf <*> ma).alternatives = mf.alternatives.seq ma.alternatives

theorem WithAlternatives.alternatives_bind {α β : Type u} (m : WithAlternatives α) (f : α → WithAlternatives β) : (m >>= f).alternatives = {b : β | ∃ a ∈ m.alternatives, b ∈ (f a).alternatives}

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

Rooth's containment constraint: the alternatives contain the ordinary value.

Equations

• m.WellFormed = (m.ordinary ∈ m.alternatives)

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

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

Composition preserves well-formedness.

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

Givenness

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

Given with respect to a: the alternatives have collapsed to the singleton {a}.

Equations

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

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

Unfeatured meanings are Given with respect to their value.

theorem WithAlternatives.Given.alternatives_seq {α β : Type u} {mf : WithAlternatives (α → β)} {f : α → β} (h : mf.Given f) (ma : WithAlternatives α) : (mf <*> ma).alternatives = f '' ma.alternatives

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