Assmann, Büring, Jordanoska & Prüller 2023: morphosyntactic focus marking

In languages that mark focus morphosyntactically, each focal marking marks one constituent, possibly a phrase or the whole clause, which may then realize any focus within it, and Blocking chooses the most specific marking available. A language's focus syncretisms are thereby fixed by which constituents have a marking of their own: Gùrùntùm's VP marking serves verb, object and VP focus, a disjunctive syncretism, and its clausal marking only clausal focus, an exocentric one. Tangale, in the paper's footnotes, follows Hausa in the progressive and Gùrùntùm in the perfective, which agrees with Hartmann and Zimmermann's reflex analysis.

In English each branching node is a domain of focal marking: default weights mark the node, and prosodic reversal its default-weak daughter. Blocking within such a domain is Büring's weak restriction, and the restrictions of the domains accumulate by his Propagation, which predicts the readings of Kim ATE the yogurt.

Main definitions

• Node: the clause skeleton, a tree under constituent containment.
• Usable: a marking usable for a focus, minimal among the inventory's covers of it.
• marking: the usable marking an inventory assigns a focus, with the inventories guruntum, buli, hausa, wolof, aymara, awing and their syncretism tables.
• Exocentric, Disjunctive: the two patterns projection theories cannot express.
• tangale, overt_iff_marking_ne_default: the Tangale inventories and their agreement with the reflex analysis.
• notMem_excluded_iff: Blocking in an English domain is the restriction of its weights.
• rows_marking, rows_english: the paper's examples, each reading realized as predicted.

TODO

Two rows focus constituents below the skeleton and are not checked: the Gùrùntùm intra-VP phrase of footnote 4, whose own marking blocks the VP marking, and the Hausa part-of-subject focus of (15).

References

• [ABJP23]
• [Bur15] — unalternative semantics
• [HZ04] — the Tangale reflex analysis
• [Sch99b], [Sel95] — projection and AvoidF

The clause skeleton

inductive AssmannEtAl2023.Node : Type

Subject and VP within the clause; verb and object within VP.

• s : Node
• sbj : Node
• vp : Node
• v : Node
• obj : Node

@[instance_reducible]

instance AssmannEtAl2023.instDecidableEqNode : DecidableEq Node

Equations

• AssmannEtAl2023.instDecidableEqNode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def AssmannEtAl2023.instReprNode.repr : Node → ℕ → Std.Format

Equations

• AssmannEtAl2023.instReprNode.repr AssmannEtAl2023.Node.s prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AssmannEtAl2023.Node.s")).group prec✝
• AssmannEtAl2023.instReprNode.repr AssmannEtAl2023.Node.sbj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AssmannEtAl2023.Node.sbj")).group prec✝
• AssmannEtAl2023.instReprNode.repr AssmannEtAl2023.Node.vp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AssmannEtAl2023.Node.vp")).group prec✝
• AssmannEtAl2023.instReprNode.repr AssmannEtAl2023.Node.v prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AssmannEtAl2023.Node.v")).group prec✝
• AssmannEtAl2023.instReprNode.repr AssmannEtAl2023.Node.obj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AssmannEtAl2023.Node.obj")).group prec✝

@[instance_reducible]

instance AssmannEtAl2023.instReprNode : Repr Node

Equations

• AssmannEtAl2023.instReprNode = { reprPrec := AssmannEtAl2023.instReprNode.repr }

@[instance_reducible]

instance AssmannEtAl2023.instFintypeNode : Fintype Node

Equations

• AssmannEtAl2023.instFintypeNode = { elems := { val := ↑AssmannEtAl2023.Node.enumList, nodup := AssmannEtAl2023.Node.enumList_nodup }, complete := AssmannEtAl2023.instFintypeNode._proof_1 }

def AssmannEtAl2023.Node.parent : Node → Option Node

The constituent immediately containing each node other than the clause.

Equations

• AssmannEtAl2023.Node.s.parent = none
• AssmannEtAl2023.Node.sbj.parent = some AssmannEtAl2023.Node.s
• AssmannEtAl2023.Node.vp.parent = some AssmannEtAl2023.Node.s
• AssmannEtAl2023.Node.v.parent = some AssmannEtAl2023.Node.vp
• AssmannEtAl2023.Node.obj.parent = some AssmannEtAl2023.Node.vp

def AssmannEtAl2023.Node.depth : Node → ℕ

The depth of a node below the clause.

Equations

• AssmannEtAl2023.Node.s.depth = 0
• AssmannEtAl2023.Node.sbj.depth = 1
• AssmannEtAl2023.Node.vp.depth = 1
• AssmannEtAl2023.Node.v.depth = 2
• AssmannEtAl2023.Node.obj.depth = 2

@[instance_reducible]

instance AssmannEtAl2023.instPartialOrderNode : PartialOrder Node

Constituent containment, generated by the parent relation.

Equations

• AssmannEtAl2023.instPartialOrderNode = partialOrderOfCovers (fun (a b : AssmannEtAl2023.Node) => a.parent = some b) AssmannEtAl2023.Node.depth AssmannEtAl2023.instPartialOrderNode._proof_1

@[instance_reducible]

instance AssmannEtAl2023.instDecidableLENode : DecidableLE Node

Equations

• AssmannEtAl2023.instDecidableLENode = decidableLEOfCovers [AssmannEtAl2023.Node.s, AssmannEtAl2023.Node.vp] AssmannEtAl2023.instDecidableLENode._proof_1

theorem AssmannEtAl2023.isChain_Ici (f : Node) : IsChain (fun (x1 x2 : Node) => x1 ≤ x2) (Set.Ici f)

The constituents containing a focus form a chain, since each node has one parent.

@[instance_reducible]

instance AssmannEtAl2023.instDecidableIsMinNode (n : Node) : Decidable (IsMin n)

Equations

• AssmannEtAl2023.instDecidableIsMinNode n = { decide := decide (∀ a ∈ Finset.univ, (fun (x : AssmannEtAl2023.Node) => x ≤ n → n ≤ x) a), reflects_decide := ⋯ }

Usable markings

def AssmannEtAl2023.Usable {C : Type u_1} [PartialOrder C] (inv : List C) (m f : C) : Prop

A marking of constituent m is usable for focus f when m is minimal among the constituents of the inventory that contain f.

Equations

• AssmannEtAl2023.Usable inv m f = Minimal (fun (c : C) => c ∈ inv ∧ f ≤ c) m

theorem AssmannEtAl2023.usable_iff {C : Type u_1} [PartialOrder C] {inv : List C} {m f : C} : Usable inv m f ↔ m ∈ inv ∧ f ≤ m ∧ ∀ c ∈ inv, f ≤ c → c ≤ m → m = c

@[instance_reducible]

instance AssmannEtAl2023.instDecidableUsableOfDecidableEqOfDecidableLE {C : Type u_1} [PartialOrder C] {inv : List C} {m f : C} [DecidableEq C] [DecidableLE C] : Decidable (Usable inv m f)

Equations

• AssmannEtAl2023.instDecidableUsableOfDecidableEqOfDecidableLE = decidable_of_iff (m ∈ inv ∧ f ≤ m ∧ ∀ c ∈ inv, f ≤ c → c ≤ m → m = c) ⋯

theorem AssmannEtAl2023.Usable.of_le {C : Type u_1} [PartialOrder C] {inv : List C} {m f g : C} (h : Usable inv m f) (hfg : f ≤ g) (hgm : g ≤ m) : Usable inv m g

A marking usable for a focus is usable for every focus between it and the marked constituent, so the foci a marking is syncretic for form a continuous stretch of the tree.

theorem AssmannEtAl2023.Usable.unique {C : Type u_1} [PartialOrder C] {inv : List C} {m m' f : C} (hchain : IsChain (fun (x1 x2 : C) => x1 ≤ x2) (Set.Ici f)) (h : Usable inv m f) (h' : Usable inv m' f) : m = m'

When the constituents containing a focus form a chain, its usable marking is unique.

Markings

def AssmannEtAl2023.marking (inv : List Node) (f : Node) : Option Node

The marking an inventory uses for a focus is its usable constituent.

Equations

• AssmannEtAl2023.marking inv f = List.find? (fun (m : AssmannEtAl2023.Node) => decide (AssmannEtAl2023.Usable inv m f)) inv

theorem AssmannEtAl2023.marking_eq_some {inv : List Node} {m f : Node} (h : Usable inv m f) : marking inv f = some m

The usable marking is the one marking finds, since on a tree there is only one.

def AssmannEtAl2023.guruntum : List Node

Gùrùntùm marks the subject by a before it, the VP by a between verb and object, and the clause by clause-final á.

Equations

• AssmannEtAl2023.guruntum = [AssmannEtAl2023.Node.sbj, AssmannEtAl2023.Node.vp, AssmannEtAl2023.Node.s]

def AssmannEtAl2023.buli : List Node

Buli marks the clause by (à)lē after the subject, the VP by ká before the object, and the verb by kámā after the VP.

Equations

• AssmannEtAl2023.buli = [AssmannEtAl2023.Node.s, AssmannEtAl2023.Node.vp, AssmannEtAl2023.Node.v]

def AssmannEtAl2023.hausa : List Node

In Hausa the relative form marks the subject, and the absolute form, the default, marks the clause.

Equations

• AssmannEtAl2023.hausa = [AssmannEtAl2023.Node.sbj, AssmannEtAl2023.Node.s]

def AssmannEtAl2023.wolof : List Node

Wolof marks the subject by a, the object by la with fronting, the VP by da(fa), and the clause by na or ngi.

Equations

• AssmannEtAl2023.wolof = [AssmannEtAl2023.Node.sbj, AssmannEtAl2023.Node.obj, AssmannEtAl2023.Node.vp, AssmannEtAl2023.Node.s]

def AssmannEtAl2023.aymara : List Node

Aymara marks the subject and the object by -wa on them, and the clause by -wa on the verb.

Equations

• AssmannEtAl2023.aymara = [AssmannEtAl2023.Node.sbj, AssmannEtAl2023.Node.obj, AssmannEtAl2023.Node.s]

def AssmannEtAl2023.awing : List Node

Awing has no marking but that of the unmarked clause.

Equations

• AssmannEtAl2023.awing = [AssmannEtAl2023.Node.s]

theorem AssmannEtAl2023.marking_guruntum (f : Node) : marking guruntum f = some (match f with | Node.sbj => Node.sbj | Node.s => Node.s | x => Node.vp)

Verb, object and VP focus share the VP marking; the clausal marking serves clausal focus only.

theorem AssmannEtAl2023.marking_buli (f : Node) : marking buli f = some (match f with | Node.s => Node.s | Node.sbj => Node.s | Node.vp => Node.vp | Node.obj => Node.vp | Node.v => Node.v)

Subject focus is syncretic with clausal focus, object focus with VP focus.

theorem AssmannEtAl2023.marking_hausa (f : Node) : marking hausa f = some (match f with | Node.sbj => Node.sbj | x => Node.s)

Only subject focus has to be marked; the default serves every other focus.

theorem AssmannEtAl2023.marking_wolof (f : Node) : marking wolof f = some (match f with | Node.sbj => Node.sbj | Node.obj => Node.obj | Node.s => Node.s | x => Node.vp)

Verb and VP focus are syncretic; subject, object and clause each have their marking.

theorem AssmannEtAl2023.marking_aymara (f : Node) : marking aymara f = some (match f with | Node.sbj => Node.sbj | Node.obj => Node.obj | x => Node.s)

Verb, VP and clausal focus are syncretic.

theorem AssmannEtAl2023.marking_awing (f : Node) : marking awing f = some Node.s

Anything can be the focus of the unmarked clause.

Exocentric and disjunctive foci

def AssmannEtAl2023.Exocentric (inv : List Node) (m : Node) : Prop

An exocentric marking realizes no focus below the constituent it marks.

Equations

• AssmannEtAl2023.Exocentric inv m = (AssmannEtAl2023.Usable inv m m ∧ ∀ f ≤ m, f ≠ m → ¬AssmannEtAl2023.Usable inv m f)

@[instance_reducible]

instance AssmannEtAl2023.instDecidableExocentric (inv : List Node) (m : Node) : Decidable (Exocentric inv m)

Equations

• AssmannEtAl2023.instDecidableExocentric inv m = id inferInstance

def AssmannEtAl2023.Disjunctive (inv : List Node) (m : Node) : Prop

A disjunctive marking realizes foci on two disjoint constituents.

Equations

• AssmannEtAl2023.Disjunctive inv m = ∃ (a : AssmannEtAl2023.Node) (b : AssmannEtAl2023.Node), ¬a ≤ b ∧ ¬b ≤ a ∧ AssmannEtAl2023.Usable inv m a ∧ AssmannEtAl2023.Usable inv m b

@[instance_reducible]

instance AssmannEtAl2023.instDecidableDisjunctive (inv : List Node) (m : Node) : Decidable (Disjunctive inv m)

Equations

• AssmannEtAl2023.instDecidableDisjunctive inv m = id inferInstance

theorem AssmannEtAl2023.guruntum_exocentric_disjunctive : Exocentric guruntum Node.s ∧ Disjunctive guruntum Node.vp

Gùrùntùm's clausal marking is exocentric and its VP marking disjunctive.

theorem AssmannEtAl2023.not_downward_syncretism : ¬∀ m ∈ guruntum, ∃ (f : Node), IsMin f ∧ Usable guruntum m f

Downward Syncretism, that every marking of a phrase is syncretic with focus on some word, fails on Gùrùntùm.

theorem AssmannEtAl2023.usable_vp_of_v {inv : List Node} {m : Node} (h : Usable inv m Node.v) (hm : Node.vp ≤ m) : Usable inv m Node.vp

A marking that realizes narrow verb focus and reaches the VP realizes VP focus too, so the disjunctive syncretism predicts the broad focus.

Tangale and the reflex analysis

def AssmannEtAl2023.tangale : Tangale.TAM → Option (List Node)

Tangale follows Hausa in the progressive, where only subject focus must be marked, and Gùrùntùm in the perfective, where verb, VP and object focus share a marking.

Equations

• AssmannEtAl2023.tangale Tangale.TAM.continuous = some AssmannEtAl2023.hausa
• AssmannEtAl2023.tangale Tangale.TAM.perfective = some AssmannEtAl2023.guruntum
• AssmannEtAl2023.tangale x✝ = none

def AssmannEtAl2023.focusNode : HartmannZimmermann2004.Focused → Node

The focused constituent of a configuration as a node.

Equations

• AssmannEtAl2023.focusNode HartmannZimmermann2004.Focused.subject = AssmannEtAl2023.Node.sbj
• AssmannEtAl2023.focusNode HartmannZimmermann2004.Focused.verb = AssmannEtAl2023.Node.v
• AssmannEtAl2023.focusNode HartmannZimmermann2004.Focused.vp = AssmannEtAl2023.Node.vp
• AssmannEtAl2023.focusNode HartmannZimmermann2004.Focused.object = AssmannEtAl2023.Node.obj

theorem AssmannEtAl2023.overt_iff_marking_ne_default (c : HartmannZimmermann2004.Config) : c.WF → ∀ inv ∈ tangale c.tam, (HartmannZimmermann2004.realize c).Nonempty ↔ marking inv (focusNode c.focused) ≠ some Node.s

A configuration has an overt reflex on the reflex analysis exactly when its marking here is not the default clausal one.

English

def AssmannEtAl2023.Node.daughters : Node → Option (Node × Node)

The daughters of a branching node, the default-weak one first.

Equations

• AssmannEtAl2023.Node.s.daughters = some (AssmannEtAl2023.Node.sbj, AssmannEtAl2023.Node.vp)
• AssmannEtAl2023.Node.vp.daughters = some (AssmannEtAl2023.Node.v, AssmannEtAl2023.Node.obj)
• x✝.daughters = none

def AssmannEtAl2023.englishMarking (n w : Node) : Focus.Restriction → Node

The node that the weights of an English domain with mother n and default-weak daughter w mark as focal. Default weights, which impose a weak restriction, mark the mother, and reversal, which imposes a strong one, marks the daughter.

Equations

• AssmannEtAl2023.englishMarking n w Focus.Restriction.weak = n
• AssmannEtAl2023.englishMarking n w Focus.Restriction.strong = w

def AssmannEtAl2023.localFocus {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (n w w' : Node) (a : α) (b : β) (t : α × β) : Option Node

The constituent of a domain with mother n and daughters w and w' that a target focuses, relative to the daughters' literal meanings a and b, is the daughter that alone varies, or the mother when both do.

Equations

• AssmannEtAl2023.localFocus n w w' a b t = if t.1 = a then if t.2 = b then none else some w' else if t.2 = b then some w else some n

theorem AssmannEtAl2023.notMem_excluded_iff {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {n w w' : Node} (h : n.daughters = some (w, w')) (a : α) (b : β) (t : α × β) (ρ : Focus.Restriction) : t ∉ Focus.excluded Prod.mk a b Edge.left ρ ↔ (localFocus n w w' a b t).elim (ρ = Focus.Restriction.weak) (Usable [n, w] (englishMarking n w ρ))

In an English domain, whose inventory is the node and its default-weak daughter, the restriction of each metrical pattern excludes exactly the targets whose focus Blocking takes from the marking the pattern provides. The literal meaning, which focuses nothing, survives only default weights.

inductive AssmannEtAl2023.Ent : Type

Individuals.

• kim : Ent
• sam : Ent

@[instance_reducible]

instance AssmannEtAl2023.instDecidableEqEnt : DecidableEq Ent

Equations

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

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

Equations

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

@[instance_reducible]

instance AssmannEtAl2023.instReprEnt : Repr Ent

Equations

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

@[instance_reducible]

instance AssmannEtAl2023.instFintypeEnt : Fintype Ent

Equations

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

inductive AssmannEtAl2023.Rel : Type

Transitive-verb meanings.

• ate : Rel
• made : Rel

@[instance_reducible]

instance AssmannEtAl2023.instDecidableEqRel : DecidableEq Rel

Equations

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

@[instance_reducible]

instance AssmannEtAl2023.instReprRel : Repr Rel

Equations

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

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

Equations

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

@[instance_reducible]

instance AssmannEtAl2023.instFintypeRel : Fintype Rel

Equations

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

inductive AssmannEtAl2023.Obj : Type

Object meanings.

• yogurt : Obj
• pickles : Obj

@[instance_reducible]

instance AssmannEtAl2023.instDecidableEqObj : DecidableEq Obj

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• AssmannEtAl2023.instReprObj.repr AssmannEtAl2023.Obj.yogurt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AssmannEtAl2023.Obj.yogurt")).group prec✝

@[instance_reducible]

instance AssmannEtAl2023.instReprObj : Repr Obj

Equations

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

@[instance_reducible]

instance AssmannEtAl2023.instFintypeObj : Fintype Obj

Equations

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

def AssmannEtAl2023.kimAteTheYogurt (ρ ρ' : Focus.Restriction) : WithAlternatives (Ent × Rel × Obj)

Kim ate the yogurt with restriction ρ on the subject and ρ' on the verb.

Equations

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

theorem AssmannEtAl2023.alternatives_kimAteTheYogurt : (kimAteTheYogurt Focus.Restriction.weak Focus.Restriction.strong).alternatives = Set.univ ×ˢ {Rel.ate}ᶜ ×ˢ {Obj.yogurt}

Under default weights in the clause and reversal in the VP, Kim ATE the yogurt allows the propositions in which anyone stands in a relation other than eating to the yogurt.

def AssmannEtAl2023.englishTarget (F : List Node) : Ent × Rel × Obj

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

Equations

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

The paper's examples

def AssmannEtAl2023.Node.parse? : String → Option Node

A reading as the focused constituent.

Equations

• AssmannEtAl2023.Node.parse? "subject" = some AssmannEtAl2023.Node.sbj
• AssmannEtAl2023.Node.parse? "verb" = some AssmannEtAl2023.Node.v
• AssmannEtAl2023.Node.parse? "VP" = some AssmannEtAl2023.Node.vp
• AssmannEtAl2023.Node.parse? "object" = some AssmannEtAl2023.Node.obj
• AssmannEtAl2023.Node.parse? "clause" = some AssmannEtAl2023.Node.s
• AssmannEtAl2023.Node.parse? x✝ = none

def AssmannEtAl2023.focus? : String → Option (List Node)

The constituents a reading focuses.

Equations

• AssmannEtAl2023.focus? "subject and verb" = some [AssmannEtAl2023.Node.sbj, AssmannEtAl2023.Node.v]
• AssmannEtAl2023.focus? x✝ = Option.map (fun (x : AssmannEtAl2023.Node) => [x]) (AssmannEtAl2023.Node.parse? x✝)

def AssmannEtAl2023.inventory? (r : Datum) : Option (List Node)

The inventory of a row's language.

Equations

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

def AssmannEtAl2023.marked? (r : Datum) : Option Node

The constituent a row's marking marks as focal.

Equations

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

def AssmannEtAl2023.englishMarked? (r : Datum) : Option (Node × Node)

The nodes an English row's prosody marks in the clause and in the VP.

Equations

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

theorem AssmannEtAl2023.rows_marking (r : Datum) : r ∈ Examples.all → ∀ inv ∈ inventory? r, ∀ m ∈ marked? r, ∀ x ∈ r.readings, ∀ f ∈ Node.parse? x.1, x.2 = Judgment.acceptable ∧ marking inv f = some m

Every reading of a row is realized by the marking the row shows, which is the marking the inventory predicts for that focus.

theorem AssmannEtAl2023.rows_english (r : Datum) : r ∈ Examples.all → englishMarked? r = some (Node.s, Node.v) → ∀ x ∈ r.readings, ∀ F ∈ focus? x.1, x.2 = Judgment.acceptable ↔ englishTarget F ∈ (kimAteTheYogurt Focus.Restriction.weak Focus.Restriction.strong).alternatives

With the clause marked by default weights and the verb by reversal, a reading of the English row is acceptable exactly when its focal target survives the restrictions of Kim ATE the yogurt.