Tangale focus strategies

Formalises [HZ04]: Tangale marks focus by four different devices conditioned on subjecthood, aspect, and transitivity — obligatory postverbal movement for subjects, the suffix -i for intransitive predicate focus, a prosodic boundary (vowel elision and left-line delinking blocked) for perfective transitive foci, and nothing at all in the progressive. The boundary underdetermines the focus extent (V-, VP-, and OBJ-focus are string- and pitch-identical), and the particle núm 'only' associates with any of the three extents from one fixed DP-adjacent position — association is anaphoric, not structural. The boundary itself is derived: [truckenbrodt-1999]-style focus alignment dominating phrasal economy places the φ-edge exactly in the focused cells, and [Kid85]'s elision cascade makes it audible.

Implementation notes

Realisation uses the shared Semantics.Focus.Realization vocabulary (reflex lists; the paper's strategy labels are read off the reflex shape in the data linkage). Configurations carry the fragment's tense–aspect type directly (Tangale.TAM): the perfective rows are [Kid85]'s singular perfective and the paper's progressive is the fragment's continuous (preposed né, transcribed n by the paper), with the paradigm restriction in Config.WF; marking_matches_rows pins the identification to the data rows. The núm readings use the strong-theory Semantics.Focus.onlyVia: one string, three contrast-set resolutions.

The paper's fn. 6 notes the suffix -i does not occur with all intransitive verbs; realize idealises it as the intransitive perfective strategy. The boundary diagnosis is grounded in Fragments/Tangale/Phonology.lean: prosodic_reflex_audible cites [Kid85]'s elision cascade as what makes the boundary reflex perceptible.

TODO

• The interleaved elision-feeding-tone-shift derivations of [Kid85] (34) on lexical forms.
• The paper's two solutions (§6): the prosodic-boundary account vs the subjects-vs-non-subjects account as rival Predict-style theories.

The marking system (§4.1, §5.2, §6.2)

inductive HartmannZimmermann2004.Focused : Type

The focused constituent in the paper's paradigm.

• subject : Focused
• verb : Focused
• vp : Focused
• object : Focused

@[implicit_reducible]

instance HartmannZimmermann2004.instDecidableEqFocused : DecidableEq Focused

Equations

• HartmannZimmermann2004.instDecidableEqFocused x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance HartmannZimmermann2004.instReprFocused : Repr Focused

Equations

• HartmannZimmermann2004.instReprFocused = { reprPrec := HartmannZimmermann2004.instReprFocused.repr }

def HartmannZimmermann2004.instReprFocused.repr : Focused → ℕ → Std.Format

Equations

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

structure HartmannZimmermann2004.Config : Type

A focus configuration of the paper's paradigm.

• focused : Focused

  The focused constituent.

• tam : Tangale.TAM

  The tense–aspect frame, from [Kid85]'s inventory.

• transitive : Bool

  Whether the predicate is transitive.

@[implicit_reducible]

instance HartmannZimmermann2004.instDecidableEqConfig : DecidableEq Config

Equations

• HartmannZimmermann2004.instDecidableEqConfig = HartmannZimmermann2004.instDecidableEqConfig.decEq

def HartmannZimmermann2004.instDecidableEqConfig.decEq (x✝ x✝¹ : Config) : Decidable (x✝ = x✝¹)

Equations

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

def HartmannZimmermann2004.instReprConfig.repr : Config → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HartmannZimmermann2004.instReprConfig : Repr Config

Equations

• HartmannZimmermann2004.instReprConfig = { reprPrec := HartmannZimmermann2004.instReprConfig.repr }

def HartmannZimmermann2004.Config.WF (c : Config) : Prop

The paper's paradigm: object focus needs a transitive predicate, and only the perfective and continuous (the paper's progressive) frames are documented.

Equations

• c.WF = ((c.focused = HartmannZimmermann2004.Focused.object → c.transitive = true) ∧ (c.tam = Tangale.TAM.perfective ∨ c.tam = Tangale.TAM.continuous))

@[implicit_reducible]

instance HartmannZimmermann2004.instDecidableWF (c : Config) : Decidable c.WF

Equations

• HartmannZimmermann2004.instDecidableWF c = HartmannZimmermann2004.instDecidableWF._aux_1 c

def HartmannZimmermann2004.realize : Config → Semantics.Focus.Realization Focused

The overt reflexes: subjects surface displaced ((17b)); intransitive predicate focus bears -i ((24b)); transitive perfective foci get the boundary after the verb ((25a–c)); progressive foci receive nothing ((31)/(32a–c)). Untested frames fall to the unmarked default, guarded by Config.WF.

Equations

• One or more equations did not get rendered due to their size.
• HartmannZimmermann2004.realize { focused := f, tam := Tangale.TAM.perfective, transitive := false } = { focus := f, reflexes := [Semantics.Focus.Reflex.morpheme f] }
• HartmannZimmermann2004.realize { focused := f, tam := tam, transitive := transitive } = { focus := f, reflexes := [] }

theorem HartmannZimmermann2004.subject_always_marked (c : Config) : c.focused = Focused.subject → (realize c).IsOvert

Focused subjects are overtly marked in every aspect — the paper's §6 subjects-vs-non-subjects generalization, shared with Hausa.

theorem HartmannZimmermann2004.progressive_nonsubject_unmarked (c : Config) (hs : c.focused ≠ Focused.subject) (ha : c.tam = Tangale.TAM.continuous) : (realize c).reflexes = []

Progressive non-subject foci are wholly unmarked ((31)/(32a–c), contra Kidda 1993).

theorem HartmannZimmermann2004.focus_marking_not_obligatory : ∃ (c : Config), c.WF ∧ ¬(realize c).IsOvert

Focus marking is not obligatory: a well-formed focus configuration with no overt reflex — (32a), object focus in the progressive.

theorem HartmannZimmermann2004.tangale_refutes_perceptibility : ¬Semantics.Focus.EveryFocusPerceptible realize

Tangale refutes the universalist claim that every focus receives an overt reflex — the Tangale side of the counterexample the Hausa chapter states against the Basic Focus Rule.

theorem HartmannZimmermann2004.boundary_underdetermines_extent : ¬Function.FactorsThroughOn Config.focused (fun (c : Config) => (realize c).reflexes) {c : Config | c.tam = Tangale.TAM.perfective ∧ c.transitive = true ∧ c.focused ≠ Focused.subject}

The boundary underdetermines the focus extent: on the transitive perfective non-subject cells, focused does not factor through the reflexes — (25a–c) are string- and pitch-identical.

Deriving the boundary ([truckenbrodt-1999]-style alignment)

The perfective boundary is not primitive. Candidate parses wrap the V–O string into one φ or separate the object into its own φ; a focus-alignment constraint (the focus's left edge coincides with a φ-edge) dominates phrasal economy exactly when the object is focused. The winning parse's φ-edge is the Reflex.boundary of realize, and its audibility is the blocked elision cascade (prosodic_reflex_audible).

theorem HartmannZimmermann2004.focused_parse_separates : (OptimalityTheory.Tableau.ofRanking [HartmannZimmermann2004.wrapped✝, HartmannZimmermann2004.separated✝] [HartmannZimmermann2004.alignFocus✝, HartmannZimmermann2004.starPhi✝] ⋯).optimal = {HartmannZimmermann2004.separated✝}

Object focus: alignment dominates economy, and the separated parse wins — the derived φ-edge after the verb.

theorem HartmannZimmermann2004.neutral_parse_wraps : (OptimalityTheory.Tableau.ofRanking [HartmannZimmermann2004.wrapped✝, HartmannZimmermann2004.separated✝] [HartmannZimmermann2004.starPhi✝] ⋯).optimal = {HartmannZimmermann2004.wrapped✝}

All-new: economy decides alone and the wrapped parse wins — no boundary, the elision cascade applies.

theorem HartmannZimmermann2004.separated_edge_wrapped_internal : (0, 2) ∉ RoseTree.spansOf Prosody.Constituent.isPh HartmannZimmermann2004.separated✝ ∧ (0, 2) ∈ RoseTree.spansOf Prosody.Constituent.isPh HartmannZimmermann2004.wrapped✝

No φ spans the V–O juncture in the separated parse — elision is blocked there and applies in the wrapped one.

theorem HartmannZimmermann2004.prosodic_reflex_audible : Tangale.blockedForm ≠ Tangale.elidedForm

The prosodic reflex is audible: the boundary-blocked perfective form differs from the phrase-medial elided form — [Kid85]'s elision cascade is what makes Reflex.boundary perceptible in the (25) cells.

The núm readings (§6.3)

núm 'only' is syntactically fixed to DP expressions, yet associates with object, VP, or verb focus — identical structure and identical pitch across (36a–c). Three contrast-set resolutions of one string, through the strong-theory onlyVia.

structure HartmannZimmermann2004.NumWorld : Type

Worlds tracking what the speaker did with the book and the rest.

• boughtBook : Bool
• boughtShirt : Bool
• readBook : Bool

@[implicit_reducible]

instance HartmannZimmermann2004.instDecidableEqNumWorld : DecidableEq NumWorld

Equations

• HartmannZimmermann2004.instDecidableEqNumWorld = HartmannZimmermann2004.instDecidableEqNumWorld.decEq

def HartmannZimmermann2004.instDecidableEqNumWorld.decEq (x✝ x✝¹ : NumWorld) : Decidable (x✝ = x✝¹)

Equations

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

def HartmannZimmermann2004.instReprNumWorld.repr : NumWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HartmannZimmermann2004.instReprNumWorld : Repr NumWorld

Equations

• HartmannZimmermann2004.instReprNumWorld = { reprPrec := HartmannZimmermann2004.instReprNumWorld.repr }

def HartmannZimmermann2004.boughtBookP : Set NumWorld

'I bought the book.'

Equations

• HartmannZimmermann2004.boughtBookP = {w : HartmannZimmermann2004.NumWorld | w.boughtBook = true}

def HartmannZimmermann2004.boughtShirtP : Set NumWorld

'I bought the shirt.'

Equations

• HartmannZimmermann2004.boughtShirtP = {w : HartmannZimmermann2004.NumWorld | w.boughtShirt = true}

def HartmannZimmermann2004.readBookP : Set NumWorld

'I read the book.'

Equations

• HartmannZimmermann2004.readBookP = {w : HartmannZimmermann2004.NumWorld | w.readBook = true}

def HartmannZimmermann2004.alt : Fin 3 → Set NumWorld

The alternative facts, as an indexed family.

Equations

• HartmannZimmermann2004.alt = ![HartmannZimmermann2004.boughtBookP, HartmannZimmermann2004.boughtShirtP, HartmannZimmermann2004.readBookP]

theorem HartmannZimmermann2004.alt_irredundant : Semantics.Focus.Irredundant alt

The alternatives are irredundant: each can hold while the others fail — one world per free Boolean field.

def HartmannZimmermann2004.extAlts : Focused → Finset (Fin 3)

The contrast sets by association extent: object ((36a), alternatives to the book), VP ((36b), 'I did nothing else'), verb ((36c), 'but I have not read it yet'). Subjects are outside the (36) paradigm; the arm shares the verb value and is never queried.

Equations

• HartmannZimmermann2004.extAlts HartmannZimmermann2004.Focused.object = {0, 1}
• HartmannZimmermann2004.extAlts HartmannZimmermann2004.Focused.vp = {0, 1, 2}
• HartmannZimmermann2004.extAlts x✝ = {0, 2}

def HartmannZimmermann2004.numReading (x : Focused) : Set NumWorld

The (36) readings: strong-theory only over the resolved contrast set, with 'bought the book' as prejacent.

Equations

• HartmannZimmermann2004.numReading x = Semantics.Focus.onlyVia (HartmannZimmermann2004.alt '' ↑(HartmannZimmermann2004.extAlts x)) (HartmannZimmermann2004.alt 0)

theorem HartmannZimmermann2004.num_readings_injOn : Set.InjOn numReading {Focused.verb, Focused.vp, Focused.object}

One surface string, three semantically distinct readings: over a irredundant alternative family, only is injective in its resolution (Irredundant.onlyVia_injOn), and the three extents resolve to three different contrast sets.

theorem HartmannZimmermann2004.vp_reading_strongest : numReading Focused.vp ⊆ numReading Focused.object ∧ numReading Focused.vp ⊆ numReading Focused.verb

The VP association is the strongest reading: 'I did nothing else' entails both 'I bought nothing else' and 'I did nothing else to the book' — onlyVia_antitone over the contrast-set inclusions.

Data linkage

realize is pinned to the paperFeatures of every focus row in Data.Examples.HartmannZimmermann2004; the paper's strategy label is read off the reflex shape.

theorem HartmannZimmermann2004.marking_matches_rows (p : Config × Data.Examples.LinguisticExample) : p ∈ HartmannZimmermann2004.configRows✝ → p.2.feature? "strategy" = some (HartmannZimmermann2004.strategyLabel✝ p.1) ∧ p.2.feature? "focused" = some (HartmannZimmermann2004.focusedLabel✝ p.1.focused) ∧ p.2.feature? "aspect" = some (HartmannZimmermann2004.aspectLabel✝ p.1.tam)

Every focus row's strategy label is read off realize's reflexes: the conditioning function is derived from the data, not stipulated beside it.