Büring 2015

Büring derives focal targets from metrical structure, without F-markers. This file runs his calculus on Smith ordered breakfast, with Jones, paid for and lunch the only alternatives to its words. Default stress on the object allows exactly the foci containing the object (Figure 2); reversal on the verb allows the foci containing the verb but not the object, and reversal on the subject only narrow subject focus (Figure 4). Reversal inside the demoted VP of a reversed clause leaves no target (Figure 5), and after Focus Reset at the VP the clause allows only its literal meaning (Figure 6).

References

• [Bur15]

inductive Buring2015.Ent : Type

Individuals.

• smith : Ent
• jones : Ent

@[instance_reducible]

instance Buring2015.instDecidableEqEnt : DecidableEq Ent

Equations

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

def Buring2015.instReprEnt.repr : Ent → ℕ → Std.Format

Equations

• Buring2015.instReprEnt.repr Buring2015.Ent.smith prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Buring2015.Ent.smith")).group prec✝
• Buring2015.instReprEnt.repr Buring2015.Ent.jones prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Buring2015.Ent.jones")).group prec✝

@[instance_reducible]

instance Buring2015.instReprEnt : Repr Ent

Equations

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

@[instance_reducible]

instance Buring2015.instFintypeEnt : Fintype Ent

Equations

• Buring2015.instFintypeEnt = { elems := { val := ↑Buring2015.Ent.enumList, nodup := Buring2015.Ent.enumList_nodup }, complete := Buring2015.instFintypeEnt._proof_1 }

inductive Buring2015.Rel : Type

Transitive-verb meanings.

• ordered : Rel
• paidFor : Rel

@[instance_reducible]

instance Buring2015.instDecidableEqRel : DecidableEq Rel

Equations

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

@[instance_reducible]

instance Buring2015.instReprRel : Repr Rel

Equations

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

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✝

@[instance_reducible]

instance Buring2015.instFintypeRel : Fintype Rel

Equations

• Buring2015.instFintypeRel = { elems := { val := ↑Buring2015.Rel.enumList, nodup := Buring2015.Rel.enumList_nodup }, complete := Buring2015.instFintypeRel._proof_1 }

inductive Buring2015.Obj : Type

Object meanings.

• breakfast : Obj
• lunch : Obj

@[instance_reducible]

instance Buring2015.instDecidableEqObj : DecidableEq Obj

Equations

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

@[instance_reducible]

instance Buring2015.instReprObj : Repr Obj

Equations

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

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✝

@[instance_reducible]

instance Buring2015.instFintypeObj : Fintype Obj

Equations

• Buring2015.instFintypeObj = { elems := { val := ↑Buring2015.Obj.enumList, nodup := Buring2015.Obj.enumList_nodup }, complete := Buring2015.instFintypeObj._proof_1 }

def Buring2015.vp (r : Focus.Restriction) : WithAlternatives (Rel × Obj)

The VP ordered breakfast with restriction r on the verb, weak under default stress on the object and strong under reversal.

Equations

• Buring2015.vp r = WithAlternatives.node Prod.mk Edge.left r (WithAlternatives.focused Buring2015.Rel.ordered) (WithAlternatives.focused Buring2015.Obj.breakfast)

def Buring2015.clause (r r' : Focus.Restriction) : WithAlternatives (Ent × Rel × Obj)

The clause Smith ordered breakfast with restriction r on the subject and r' on the verb.

Equations

• Buring2015.clause r r' = WithAlternatives.node Prod.mk Edge.left r (WithAlternatives.focused Buring2015.Ent.smith) (Buring2015.vp r')

The VP

theorem Buring2015.compl_alternatives_vp_weak : (vp Focus.Restriction.weak).alternativesᶜ = {Rel.ordered}ᶜ ×ˢ {Obj.breakfast}

Default ordered BREAKfast excludes the VP meanings composed of a relation other than ordered and breakfast, Büring's (5).

theorem Buring2015.alternatives_vp_strong : (vp Focus.Restriction.strong).alternatives = {Rel.ordered}ᶜ ×ˢ {Obj.breakfast}

Reversed ORDERED breakfast allows only the VP meanings composed of a relation other than ordered and breakfast, Büring's (10).

theorem Buring2015.isCompl_alternatives_vp : IsCompl (vp Focus.Restriction.weak).alternatives (vp Focus.Restriction.strong).alternatives

Default and reversed weights on the VP divide its focal targets between them.

The clause

inductive Buring2015.Word : Type

The words of the clause.

• subj : Word
• verb : Word
• obj : Word

@[instance_reducible]

instance Buring2015.instDecidableEqWord : DecidableEq Word

Equations

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

def Buring2015.instReprWord.repr : Word → ℕ → Std.Format

Equations

• Buring2015.instReprWord.repr Buring2015.Word.subj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Buring2015.Word.subj")).group prec✝
• Buring2015.instReprWord.repr Buring2015.Word.verb prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Buring2015.Word.verb")).group prec✝
• Buring2015.instReprWord.repr Buring2015.Word.obj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Buring2015.Word.obj")).group prec✝

@[instance_reducible]

instance Buring2015.instReprWord : Repr Word

Equations

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

@[instance_reducible]

instance Buring2015.instFintypeWord : Fintype Word

Equations

• Buring2015.instFintypeWord = { elems := { val := ↑Buring2015.Word.enumList, nodup := Buring2015.Word.enumList_nodup }, complete := Buring2015.instFintypeWord._proof_1 }

def Buring2015.target (F : Finset Word) : Ent × Rel × Obj

The focal target of a focus on the words F replaces each of them by its alternative.

Equations

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

theorem Buring2015.wellFormed_clause_weak_weak : (clause Focus.Restriction.weak Focus.Restriction.weak).WellFormed

Default weights keep the literal meaning of Smith ordered breakfast, which is why Büring's Weak Restriction subtracts the weak daughter's ordinary value.

theorem Buring2015.compl_alternatives_clause_weak_weak : (clause Focus.Restriction.weak Focus.Restriction.weak).alternativesᶜ = {t : Ent × Rel × Obj | t.2.2 = Obj.breakfast} \ {(Ent.smith, Rel.ordered, Obj.breakfast)}

Default Smith ordered BREAKfast excludes the propositions composed of an individual, a relation and breakfast, other than Smith ordered breakfast itself (Figure 2).

theorem Buring2015.target_mem_clause_weak_weak (F : Finset Word) : target F ∈ (clause Focus.Restriction.weak Focus.Restriction.weak).alternatives ↔ Word.obj ∈ F ∨ F = ∅

Default stress on the object allows exactly the foci containing the object, and the literal meaning (Figure 2).

theorem Buring2015.alternatives_clause_weak_strong : (clause Focus.Restriction.weak Focus.Restriction.strong).alternatives = Set.univ ×ˢ {Rel.ordered}ᶜ ×ˢ {Obj.breakfast}

Smith ORDERED breakfast allows the propositions in which any individual stands in a relation other than ordered to breakfast (Figure 4).

theorem Buring2015.target_mem_clause_weak_strong (F : Finset Word) : target F ∈ (clause Focus.Restriction.weak Focus.Restriction.strong).alternatives ↔ Word.verb ∈ F ∧ Word.obj ∉ F

Reversal on the verb allows the foci containing the verb but not the object (Figure 4).

theorem Buring2015.alternatives_clause_strong_weak : (clause Focus.Restriction.strong Focus.Restriction.weak).alternatives = {Ent.smith}ᶜ ×ˢ {(Rel.ordered, Obj.breakfast)}

SMITH ordered breakfast allows the propositions in which an individual other than Smith ordered breakfast (Figure 4).

theorem Buring2015.target_mem_clause_strong_weak (F : Finset Word) : target F ∈ (clause Focus.Restriction.strong Focus.Restriction.weak).alternatives ↔ F = {Word.subj}

Reversal on the subject allows only narrow subject focus (Figure 4).

theorem Buring2015.alternatives_clause_strong_strong : (clause Focus.Restriction.strong Focus.Restriction.strong).alternatives = ∅

Reversal inside the demoted VP of a reversed clause leaves no focal target (Figure 5).

theorem Buring2015.alternatives_reset_vp : (WithAlternatives.node Prod.mk Edge.left Focus.Restriction.weak (WithAlternatives.focused Ent.smith) (WithAlternatives.unfeatured (vp Focus.Restriction.weak).ordinary)).alternatives = {(Ent.smith, Rel.ordered, Obj.breakfast)}

After Focus Reset at the VP, Propagation and the weak restriction on the subject leave the clause only its literal meaning, as Büring's condition on root nodes demands (Figure 6).