Unalternative morphosyntactic focus marking

Formalises [assmann-etal-2023]: focus marking without [F]-features. Each construction focally marks exactly one constituent; No Projection (§2.2) lets it realize any focus within that constituent (the marked constituent and the pragmatic focus need not coincide); Blocking (§2.3) preempts a marking wherever a strictly more specific one would do — Usable is minimality among inventory covers. Syncretism is containment minus blocking: disjoint-constituent syncretisms (V with Obj, §4.2.1) — which "directly contradict Uniform Marking" — fall out by focally marking the common mother (§4.2.3).

Case studies: Gùrùntùm (§2), where the clausal marking is blocked for every smaller focus, and Hausa (§3.2), where the relative form focally marks the subject and the absolute form is a default marking the clause. Their fn. 13 extends the Hausa pattern to the Tangale progressive and fn. 18 treats the Tangale perfective triple as the V/VP/O syncretism, so ua_agrees_with_hz_on_overtness proves cell-by-cell agreement with [HZ04]'s reflex analysis (HartmannZimmermann2004.realize) while the two accounts disagree about what "marking the focus" means: what the reflex analysis states as focus without overt reflex is, here, a default marking whose focally marked constituent properly contains the focus. Their fn. 17 hedges on the placement of the Tangale markers; the marking-to-constituent assignment below follows their fn. 13 and fn. 18.

The constituent skeleton of the case studies

inductive AssmannEtAl2023.Node : Type

Clause skeleton: subject and VP within S; verb and object within VP.

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

@[implicit_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✝

@[implicit_reducible]

instance AssmannEtAl2023.instReprNode : Repr Node

Equations

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

@[implicit_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.nle : Node → Node → Bool

Constituent containment.

Equations

• AssmannEtAl2023.nle x✝ AssmannEtAl2023.Node.s = true
• AssmannEtAl2023.nle AssmannEtAl2023.Node.v AssmannEtAl2023.Node.vp = true
• AssmannEtAl2023.nle AssmannEtAl2023.Node.obj AssmannEtAl2023.Node.vp = true
• AssmannEtAl2023.nle AssmannEtAl2023.Node.vp AssmannEtAl2023.Node.vp = true
• AssmannEtAl2023.nle AssmannEtAl2023.Node.sbj AssmannEtAl2023.Node.sbj = true
• AssmannEtAl2023.nle AssmannEtAl2023.Node.v AssmannEtAl2023.Node.v = true
• AssmannEtAl2023.nle AssmannEtAl2023.Node.obj AssmannEtAl2023.Node.obj = true
• AssmannEtAl2023.nle x✝¹ x✝ = false

@[implicit_reducible]

instance AssmannEtAl2023.instPartialOrderNode : PartialOrder Node

Equations

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

@[implicit_reducible]

instance AssmannEtAl2023.instDecidableLENode : DecidableLE Node

Equations

• AssmannEtAl2023.instDecidableLENode x✝¹ x✝ = instDecidableEqBool (AssmannEtAl2023.nle x✝¹ x✝) true

Case study I: Gùrùntùm (§2)

def AssmannEtAl2023.guruntumInv : List Node

The Gùrùntùm inventory: a before the subject, a before the object marking VP, clausal á ((4a–c)).

Equations

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

theorem AssmannEtAl2023.guruntum_vp_syncretism : Semantics.Focus.Usable guruntumInv Node.vp Node.v ∧ Semantics.Focus.Usable guruntumInv Node.vp Node.vp ∧ Semantics.Focus.Usable guruntumInv Node.vp Node.obj

(4b): focally marking VP is syncretic for V, VP and Obj focus — No Projection in action.

theorem AssmannEtAl2023.guruntum_clausal_blocked : Semantics.Focus.Usable guruntumInv Node.s Node.s ∧ ¬Semantics.Focus.Usable guruntumInv Node.s Node.sbj ∧ ¬Semantics.Focus.Usable guruntumInv Node.s Node.vp ∧ ¬Semantics.Focus.Usable guruntumInv Node.s Node.obj

(4c)/(5): the clausal marking realizes only clausal focus — every smaller focus is blocked by a specialized marking.

Case study: Hausa (§3.2)

def AssmannEtAl2023.hausaInv : List Node

The Hausa canonical-order inventory: the relative form of the PAC focally marks the subject ((10)); the absolute form is the default, "the absence of a specific marking", focally marking the clause.

Equations

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

theorem AssmannEtAl2023.hausa_default_syncretism : Semantics.Focus.Usable hausaInv Node.s Node.v ∧ Semantics.Focus.Usable hausaInv Node.s Node.vp ∧ Semantics.Focus.Usable hausaInv Node.s Node.obj ∧ Semantics.Focus.Usable hausaInv Node.s Node.s

(11): the absolute form answers any non-subject constituent question and all-new contexts — one default, syncretic for V, VP, Obj and clausal focus.

theorem AssmannEtAl2023.hausa_subject_needs_relative : ¬Semantics.Focus.Usable hausaInv Node.s Node.sbj ∧ Semantics.Focus.Usable hausaInv Node.sbj Node.sbj

Only subject focus has to be marked (their fn. 13): the default is blocked for subject focus by the relative form.

The Tangale rivalry (their fn. 13, 17, 18)

Their fn. 13 extends the Hausa pattern to the Tangale progressive; fn. 18 treats the Tangale perfective V/VP/O triple as the disjoint-constituent syncretism, focally marking VP (§4.2.3). The resulting marking assignment agrees with [HZ04]'s reflex analysis on every cell of the paradigm — the accounts differ not on the data but on what "marking the focus" means.

def AssmannEtAl2023.uaTangale : HartmannZimmermann2004.Config → Node

The UA marking of each Tangale configuration: subjects take the specific subject marking (postposing); perfective non-subject foci the VP-marking (the prosodic boundary, fn. 18); other frames fall to the default clause marking — fn. 13's progressive among them, mirroring realize's guard-zone default.

Equations

• AssmannEtAl2023.uaTangale { focused := HartmannZimmermann2004.Focused.subject, tam := tam, transitive := transitive } = AssmannEtAl2023.Node.sbj
• AssmannEtAl2023.uaTangale { focused := focused, tam := Tangale.TAM.perfective, transitive := transitive } = AssmannEtAl2023.Node.vp
• AssmannEtAl2023.uaTangale { focused := focused, tam := tam, transitive := transitive } = AssmannEtAl2023.Node.s

theorem AssmannEtAl2023.ua_agrees_with_hz_on_overtness (c : HartmannZimmermann2004.Config) : (HartmannZimmermann2004.realize c).IsOvert ↔ uaTangale c ≠ Node.s

Cell-by-cell agreement with the reflex analysis: a configuration has an overt reflex iff its UA marking is not the default. What focus_marking_not_obligatory states as focus without reflex is, for UA, the default marking whose focally marked constituent properly contains the focus.