Unalternative semantics

In Büring's unalternative semantics the focal targets of a constituent play the part of its focus value, so a meaning is a WithAlternatives whose alternatives are its focal targets. What a constituent excludes are its unalternatives. A terminal excludes nothing, so it is focused. A branching node excludes whatever is composed from an unalternative of a daughter (Propagation), and whatever its own restriction on one daughter excludes: a weak restriction excludes narrow focus on her, and a strong restriction everything else. Default metrical weights put a weak restriction on the weak daughter, and prosodic reversal a strong restriction on the daughter it promotes. Focus Reset leaves a constituent only its literal meaning, as unfeatured does.

Main definitions

• Focus.narrow: the targets of narrow focus on one daughter of a node.
• Focus.Restriction, Focus.excluded: the weak and the strong restriction, and what each excludes.
• Focus.propagated: the targets a node excludes by Propagation.
• WithAlternatives.node: a branching node of unalternative semantics.

Main results

• WithAlternatives.alternatives_node: under a bijective composition, the targets of a node are the alternatives of the Roothian composition map₂ of its daughters, minus what its restriction excludes.
• WithAlternatives.not_wellFormed_node_strong: a strong restriction excludes the literal meaning of its node, against Rooth's containment constraint.
• WithAlternatives.alternatives_node_left_strong_eq_empty: a strong restriction over a sister that excludes her own literal meaning leaves no target.

Implementation notes

Büring restricts the alternatives of a constituent to the natural meanings of its type. Here the alternatives are all values of the type, so a model chooses types of natural meanings, and a node composes its daughters by a fixed operation op. Büring's pointwise combination ⊗ is Set.image2 op, the alternatives of WithAlternatives.map₂ op.

References

• [Bur15]

def Focus.narrow {α : Type u_1} {β : Type u_2} {γ : Type u_3} (op : α → β → γ) (a : α) (b : β) : Edge → Set γ

The targets of narrow focus on daughter e of a node whose daughters have ordinary values a and b vary that daughter and hold her sister at her ordinary value.

Equations

• Focus.narrow op a b Edge.left = Set.image2 op {a}ᶜ {b}
• Focus.narrow op a b Edge.right = Set.image2 op {a} {b}ᶜ

inductive Focus.Restriction : Type

A restriction on a daughter is weak or strong.

• weak : Restriction
• strong : Restriction

@[instance_reducible]

instance Focus.instDecidableEqRestriction : DecidableEq Restriction

Equations

• Focus.instDecidableEqRestriction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Focus.instReprRestriction.repr : Restriction → ℕ → Std.Format

Equations

• Focus.instReprRestriction.repr Focus.Restriction.weak prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Focus.Restriction.weak")).group prec✝
• Focus.instReprRestriction.repr Focus.Restriction.strong prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Focus.Restriction.strong")).group prec✝

@[instance_reducible]

instance Focus.instReprRestriction : Repr Restriction

Equations

• Focus.instReprRestriction = { reprPrec := Focus.instReprRestriction.repr }

@[instance_reducible]

instance Focus.instFintypeRestriction : Fintype Restriction

Equations

• Focus.instFintypeRestriction = { elems := { val := ↑Focus.Restriction.enumList, nodup := Focus.Restriction.enumList_nodup }, complete := Focus.instFintypeRestriction._proof_1 }

def Focus.excluded {α : Type u_1} {β : Type u_2} {γ : Type u_3} (op : α → β → γ) (a : α) (b : β) (e : Edge) : Restriction → Set γ

A weak restriction on daughter e excludes narrow focus on her, and a strong restriction excludes every other target.

Equations

• Focus.excluded op a b e Focus.Restriction.weak = Focus.narrow op a b e
• Focus.excluded op a b e Focus.Restriction.strong = (Focus.narrow op a b e)ᶜ

def Focus.propagated {α : Type u_1} {β : Type u_2} {γ : Type u_3} (op : α → β → γ) (u : Set α) (v : Set β) : Set γ

Propagation excludes every target composed from an unalternative of either daughter.

Equations

• Focus.propagated op u v = Set.image2 op Set.univ v ∪ Set.image2 op u Set.univ

@[simp]

theorem Focus.narrow_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {op : α → β → γ} {a : α} {b : β} : narrow op a b Edge.left = Set.image2 op {a}ᶜ {b}

@[simp]

theorem Focus.narrow_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {op : α → β → γ} {a : α} {b : β} : narrow op a b Edge.right = Set.image2 op {a} {b}ᶜ

@[simp]

theorem Focus.excluded_weak {α : Type u_1} {β : Type u_2} {γ : Type u_3} {op : α → β → γ} {a : α} {b : β} (e : Edge) : excluded op a b e Restriction.weak = narrow op a b e

@[simp]

theorem Focus.excluded_strong {α : Type u_1} {β : Type u_2} {γ : Type u_3} {op : α → β → γ} {a : α} {b : β} (e : Edge) : excluded op a b e Restriction.strong = (narrow op a b e)ᶜ

theorem Focus.notMem_narrow {α : Type u_1} {β : Type u_2} {γ : Type u_3} {op : α → β → γ} {a : α} {b : β} (hop : Function.Injective2 op) (e : Edge) : op a b ∉ narrow op a b e

Narrow focus on a daughter excludes the literal meaning of the node.

theorem Focus.disjoint_narrow_left_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {op : α → β → γ} {a : α} {b : β} (hop : Function.Injective2 op) : Disjoint (narrow op a b Edge.left) (narrow op a b Edge.right)

theorem Focus.narrow_swap_subset_excluded_strong {α : Type u_1} {β : Type u_2} {γ : Type u_3} {op : α → β → γ} {a : α} {b : β} (hop : Function.Injective2 op) (e : Edge) : narrow op a b e.swap ⊆ excluded op a b e Restriction.strong

A strong restriction on a daughter excludes narrow focus on her sister.

theorem Focus.compl_propagated {α : Type u_1} {β : Type u_2} {γ : Type u_3} {op : α → β → γ} (hop : Function.Bijective (Function.uncurry op)) (u : Set α) (v : Set β) : (propagated op u v)ᶜ = Set.image2 op uᶜ vᶜ

Under a bijective composition, the targets Propagation leaves are composed from targets of both daughters.

def WithAlternatives.node {α : Type u_1} {β : Type u_2} {γ : Type u_3} (op : α → β → γ) (e : Edge) (r : Focus.Restriction) (d₁ : WithAlternatives α) (d₂ : WithAlternatives β) : WithAlternatives γ

A branching node of unalternative semantics composes its daughters by op, and its targets are those that neither Propagation nor its restriction r on daughter e excludes.

Equations

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

@[simp]

theorem WithAlternatives.ordinary_node {α : Type u_1} {β : Type u_2} {γ : Type u_3} {op : α → β → γ} {e : Edge} {r : Focus.Restriction} {d₁ : WithAlternatives α} {d₂ : WithAlternatives β} : (node op e r d₁ d₂).ordinary = op d₁.ordinary d₂.ordinary

theorem WithAlternatives.compl_alternatives_node {α : Type u_1} {β : Type u_2} {γ : Type u_3} {op : α → β → γ} {e : Edge} {r : Focus.Restriction} {d₁ : WithAlternatives α} {d₂ : WithAlternatives β} : (node op e r d₁ d₂).alternativesᶜ = Focus.propagated op d₁.alternativesᶜ d₂.alternativesᶜ ∪ Focus.excluded op d₁.ordinary d₂.ordinary e r

The unalternatives of a node are those Propagation and its restriction exclude.

theorem WithAlternatives.alternatives_node {α : Type u_1} {β : Type u_2} {γ : Type u_3} {op : α → β → γ} {e : Edge} {r : Focus.Restriction} {d₁ : WithAlternatives α} {d₂ : WithAlternatives β} (hop : Function.Bijective (Function.uncurry op)) : (node op e r d₁ d₂).alternatives = (map₂ op d₁ d₂).alternatives \ Focus.excluded op d₁.ordinary d₂.ordinary e r

Under a bijective composition, the targets of a node are the alternatives of the Roothian composition of its daughters, less what the node's restriction excludes.

theorem WithAlternatives.alternatives_node_weak_union_strong {α : Type u_1} {β : Type u_2} {γ : Type u_3} {op : α → β → γ} {e : Edge} {d₁ : WithAlternatives α} {d₂ : WithAlternatives β} : (node op e Focus.Restriction.weak d₁ d₂).alternatives ∪ (node op e Focus.Restriction.strong d₁ d₂).alternatives = (Focus.propagated op d₁.alternativesᶜ d₂.alternativesᶜ)ᶜ

The weak and the strong restriction on a daughter divide between them the targets that Propagation leaves.

theorem WithAlternatives.disjoint_alternatives_node_weak_strong {α : Type u_1} {β : Type u_2} {γ : Type u_3} {op : α → β → γ} {e : Edge} {d₁ : WithAlternatives α} {d₂ : WithAlternatives β} : Disjoint (node op e Focus.Restriction.weak d₁ d₂).alternatives (node op e Focus.Restriction.strong d₁ d₂).alternatives

theorem WithAlternatives.WellFormed.node_weak {α : Type u_1} {β : Type u_2} {γ : Type u_3} {op : α → β → γ} {e : Edge} {d₁ : WithAlternatives α} {d₂ : WithAlternatives β} (hop : Function.Injective2 op) (h₁ : d₁.WellFormed) (h₂ : d₂.WellFormed) : (node op e Focus.Restriction.weak d₁ d₂).WellFormed

A weak restriction keeps the literal meaning of a node whose daughters keep theirs.

theorem WithAlternatives.not_wellFormed_node_strong {α : Type u_1} {β : Type u_2} {γ : Type u_3} {op : α → β → γ} {e : Edge} {d₁ : WithAlternatives α} {d₂ : WithAlternatives β} (hop : Function.Injective2 op) : ¬(node op e Focus.Restriction.strong d₁ d₂).WellFormed

A strong restriction excludes the literal meaning of its node.

theorem WithAlternatives.alternatives_node_left_strong_eq_empty {α : Type u_1} {β : Type u_2} {γ : Type u_3} {op : α → β → γ} {d₁ : WithAlternatives α} {d₂ : WithAlternatives β} (h : ¬d₂.WellFormed) : (node op Edge.left Focus.Restriction.strong d₁ d₂).alternatives = ∅

A strong restriction on the left daughter leaves no target when her sister excludes her own literal meaning.

theorem WithAlternatives.alternatives_node_right_strong_eq_empty {α : Type u_1} {β : Type u_2} {γ : Type u_3} {op : α → β → γ} {d₁ : WithAlternatives α} {d₂ : WithAlternatives β} (h : ¬d₁.WellFormed) : (node op Edge.right Focus.Restriction.strong d₁ d₂).alternatives = ∅

A strong restriction on the right daughter leaves no target when her sister excludes her own literal meaning.