Unalternative Semantics: the prosodic origin

Formalises [buring-2015]: calculating focus alternatives without F-markers, from metrical structure alone. A branching node's stress pattern restricts its focal targets — under the default weak–strong pattern the Weak Restriction (his (1)) bans targets that vary the weak daughter while the strong stays at its ordinary value; under prosodic reversal the Strong Restriction (his (9)) allows only targets varying the accented daughter non-trivially.

The worked example is his ordered BREAKfast vs ORDERED breakfast: default stress bans exactly the verb-focus targets ('R breakfast') and permits object and VP focus; reversal permits exactly the non-trivial verb-focus targets. The rules live in Semantics/Focus/Unalternatives.lean, shared with the morphosyntactic extension of [assmann-etal-2023].

inductive Buring2015.Rel : Type

Transitive-verb meanings.

• ordered : Rel
• paidFor : Rel

@[implicit_reducible]

instance Buring2015.instDecidableEqRel : DecidableEq Rel

Equations

• Buring2015.instDecidableEqRel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Buring2015.instReprRel.repr : Rel → ℕ → Std.Format

Equations

• Buring2015.instReprRel.repr Buring2015.Rel.ordered prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Buring2015.Rel.ordered")).group prec✝
• Buring2015.instReprRel.repr Buring2015.Rel.paidFor prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Buring2015.Rel.paidFor")).group prec✝

@[implicit_reducible]

instance Buring2015.instReprRel : Repr Rel

Equations

• Buring2015.instReprRel = { reprPrec := Buring2015.instReprRel.repr }

inductive Buring2015.Obj : Type

Object meanings.

• breakfast : Obj
• lunch : Obj

@[implicit_reducible]

instance Buring2015.instDecidableEqObj : DecidableEq Obj

Equations

• Buring2015.instDecidableEqObj x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Buring2015.instReprObj.repr : Obj → ℕ → Std.Format

Equations

• Buring2015.instReprObj.repr Buring2015.Obj.breakfast prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Buring2015.Obj.breakfast")).group prec✝
• Buring2015.instReprObj.repr Buring2015.Obj.lunch prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Buring2015.Obj.lunch")).group prec✝

@[implicit_reducible]

instance Buring2015.instReprObj : Repr Obj

Equations

• Buring2015.instReprObj = { reprPrec := Buring2015.instReprObj.repr }

def Buring2015.vt (r : Rel) : Obj → Rel × Obj

VP meanings as verb–object applications, modelled as pairs.

Equations

• Buring2015.vt r o = (r, o)

def Buring2015.orderedM : Alternatives.AltMeaning (Obj → Rel × Obj)

ordered, with its transitive alternatives.

Equations

• Buring2015.orderedM = { oValue := Buring2015.vt Buring2015.Rel.ordered, aValue := [Buring2015.vt Buring2015.Rel.ordered, Buring2015.vt Buring2015.Rel.paidFor] }

def Buring2015.breakfastM : Alternatives.AltMeaning Obj

breakfast, with its object alternatives.

Equations

• Buring2015.breakfastM = { oValue := Buring2015.Obj.breakfast, aValue := [Buring2015.Obj.breakfast, Buring2015.Obj.lunch] }

theorem Buring2015.default_bans_verb_focus : (Rel.paidFor, Obj.breakfast) ∈ Semantics.Focus.weakBanned orderedM breakfastM

Default ordered BREAKfast bans the verb-focus target 'paid for breakfast': it varies the weak daughter over given breakfast.

theorem Buring2015.default_permits_object_focus : (Rel.ordered, Obj.lunch) ∉ Semantics.Focus.weakBanned orderedM breakfastM

Default ordered BREAKfast permits the object-focus target 'ordered lunch': no way to compose it holding breakfast fixed.

theorem Buring2015.reversal_allows_verb_focus : (Rel.paidFor, Obj.breakfast) ∈ Semantics.Focus.strongAllowed orderedM breakfastM

Reversed ORDERED breakfast allows the non-trivial verb-focus target 'paid for breakfast'.

theorem Buring2015.reversal_excludes_trivial : (Rel.ordered, Obj.breakfast) ∉ Semantics.Focus.strongAllowed orderedM breakfastM

Reversed ORDERED breakfast excludes the trivial target 'ordered breakfast' itself: the accented daughter must vary.

theorem Buring2015.reversal_excludes_object_focus : (Rel.ordered, Obj.lunch) ∉ Semantics.Focus.strongAllowed orderedM breakfastM

Reversal also excludes object-focus targets: only the accented verb may vary.

theorem Buring2015.licensed_eq : Semantics.Focus.licensedFocusValue orderedM breakfastM = {p : Rel × Obj | p.2 = Obj.lunch}

The licensed focal targets of default ordered BREAKfast compute to exactly the breakfast-free compositions: object focus with a new object survives; everything about breakfast is banned. The licensed set is the focus value the prosody derives — the pipeline the squiggle consumes at propositional type.