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. The monad lives in one universe; binary composition across universes is WithAlternatives.map₂, the same composition with Set.image2 as its alternatives.

Main definitions

• WithAlternatives — an ordinary value together with the alternatives it evokes
• WithAlternatives.unfeatured, WithAlternatives.focused — the meanings of an unfocused and of an F-marked expression, evoking only their own value and every value respectively
• WithAlternatives.WellFormed — the containment constraint: the alternatives include the ordinary value
• WithAlternatives.Given — the alternatives have collapsed to a singleton
• WithAlternatives.map₂ — binary composition, alternatives composed pointwise

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
• CommApplicative WithAlternatives, seq_eq_bind_seq_pure — composition does not depend on the order of the daughters, so an application can bind its argument first
• Given.alternatives_seq — a Given function contributes only its ordinary value

References

• [Roo85]
• [Roo92]
• [KS20]

structure WithAlternatives (α : Type u_1) : Type u_1

An ordinary denotation together with the alternatives the expression evokes ([Roo92]).

• 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 unfeatured x of an expression bearing no focus feature 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}

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

The meaning of an F-marked expression whose alternatives are its whole type: focused x has ordinary value x and evokes every value ([Roo92]'s focus semantic value of a constant).

Equations

• WithAlternatives.focused x = { ordinary := x, alternatives := Set.univ }

@[simp]

theorem WithAlternatives.focused_ordinary {α : Type u_1} (x : α) : (focused x).ordinary = x

@[simp]

theorem WithAlternatives.focused_alternatives {α : Type u_1} (x : α) : (focused x).alternatives = Set.univ

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

In Hamblin functional application alternative functions apply to alternative arguments.

theorem WithAlternatives.alternatives_map_focused {α β : Type u} (f : α → β) (x : α) : (f <$> focused x).alternatives = Set.range f

Mapping over an F-marked constituent evokes the whole range of the function.

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}

instance WithAlternatives.instCommApplicative : CommApplicative WithAlternatives

Hamblin composition does not depend on the order in which the daughters are composed, since both dimensions, Id and Set, are commutative.

theorem WithAlternatives.seq_eq_bind_seq_pure {α β : Type u} (mf : WithAlternatives (α → β)) (mx : WithAlternatives α) : mf <*> mx = do let x ← mx mf <*> pure x

By commutativity an application can run its argument first, binding the argument into the function applied to it.

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

Rooth's containment constraint says that 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.focused {α : Type u} (x : α) : (WithAlternatives.focused 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

theorem WithAlternatives.WellFormed.seq {α β : Type u} {mf : WithAlternatives (α → β)} {ma : WithAlternatives α} (hf : mf.WellFormed) (ha : ma.WellFormed) : (mf <*> ma).WellFormed

Givenness

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

A meaning is Given with respect to a when its alternatives have collapsed to {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.alternatives_seq_eq_univ {α β : Type u} {mf : WithAlternatives (α → β)} {ma : WithAlternatives α} (hf : mf.alternatives = Set.univ) (ha : ma.alternatives.Nonempty) : (mf <*> ma).alternatives = Set.univ

A function evoking every function, applied to an argument that evokes something, evokes every 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.

Binary composition

theorem WithAlternatives.not_given_of_nontrivial {α : Type u_1} {m : WithAlternatives α} (h : m.alternatives.Nontrivial) (x : α) : ¬m.Given x

A meaning whose alternatives are nontrivial is Given with respect to nothing.

def WithAlternatives.map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : WithAlternatives α) (b : WithAlternatives β) : WithAlternatives γ

Binary composition by f composes the ordinary values, and its alternatives are the compositions of an alternative of each daughter.

Equations

• WithAlternatives.map₂ f a b = { ordinary := f a.ordinary b.ordinary, alternatives := Set.image2 f a.alternatives b.alternatives }

@[simp]

theorem WithAlternatives.ordinary_map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : WithAlternatives α) (b : WithAlternatives β) : (map₂ f a b).ordinary = f a.ordinary b.ordinary

@[simp]

theorem WithAlternatives.alternatives_map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : WithAlternatives α) (b : WithAlternatives β) : (map₂ f a b).alternatives = Set.image2 f a.alternatives b.alternatives

theorem WithAlternatives.WellFormed.map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {a : WithAlternatives α} {b : WithAlternatives β} (ha : a.WellFormed) (hb : b.WellFormed) : (WithAlternatives.map₂ f a b).WellFormed

theorem WithAlternatives.map₂_eq_seq {α β γ : Type u} (f : α → β → γ) (a : WithAlternatives α) (b : WithAlternatives β) : map₂ f a b = f <$> a <*> b

Within a universe, binary composition is the monad's f <$> a <*> b.