Hartmann and Zimmermann (2004): Focus strategies in Chadic

This file formalizes Hartmann and Zimmermann's account of Tangale, which marks focus by four devices conditioned on subjecthood, aspect and transitivity: obligatory postverbal movement for subjects, the suffix -i for intransitive predicate focus, a prosodic boundary, audible as blocked vowel elision and left-line delinking, for perfective transitive foci, and nothing at all in the progressive. realize gives each configuration its reflexes, so focus marking is not obligatory, and the boundary underdetermines the focus extent (boundary_underdetermines_extent): verb, VP and object focus are string- and pitch-identical, and the particle núm 'only' associates with any of the three from one fixed DP-adjacent position, three contrast-set resolutions of one string (num_readings_injOn). The boundary itself is derived: focus alignment dominating phrasal economy, after Truckenbrodt, places the φ-edge exactly in the focused cells (focused_parse_separates), and Kidda's elision cascade makes it audible.

Implementation notes

Realisation uses the shared Reflex vocabulary, and the paper's strategy labels are read off the reflex shape where marking_matches_rows pins the configurations to the data rows. Configurations carry the fragment's tense–aspect type: the perfective rows are Kidda'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 the well-formedness predicate. The paper's fn. 6 notes that -i does not occur with all intransitive verbs; the realisation idealises it as the intransitive perfective strategy. The example numbers and sections were checked against the journal version of the paper.

TODO

• The interleaved elision-feeding-tone-shift derivations of Kidda's (34) on lexical forms.
• The paper's two solutions (§6): the prosodic-boundary account against the subjects-versus- non-subjects account as rival theories.

References

• [HZ04]
• [HZ07b]
• [Tru99]
• [Kid85]

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

@[instance_reducible]

instance HartmannZimmermann2004.instDecidableEqFocused : DecidableEq Focused

Equations

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

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

Equations

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

@[instance_reducible]

instance HartmannZimmermann2004.instReprFocused : Repr Focused

Equations

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

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.

@[instance_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.

@[instance_reducible]

instance HartmannZimmermann2004.instReprConfig : Repr Config

Equations

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

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

Equations

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

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

A configuration is in the paper's paradigm when object focus has a transitive predicate and the frame is perfective or continuous (the paper's progressive), the only two documented.

Equations

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

@[instance_reducible]

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

Equations

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

def HartmannZimmermann2004.realize : Config → Finset (Reflex Focused)

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

Equations

• HartmannZimmermann2004.realize { focused := HartmannZimmermann2004.Focused.subject, tam := tam, transitive := transitive } = {Reflex.displacement HartmannZimmermann2004.Focused.subject}
• HartmannZimmermann2004.realize { focused := f, tam := Tangale.TAM.perfective, transitive := false } = {Reflex.morpheme f [Tangale.focusSuffix]}
• HartmannZimmermann2004.realize { focused := focused, tam := Tangale.TAM.perfective, transitive := true } = {Reflex.boundary HartmannZimmermann2004.Focused.verb}
• HartmannZimmermann2004.realize x✝ = ∅

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

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 = ∅

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).Nonempty

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

theorem HartmannZimmermann2004.tangale_refutes_perceptibility : ¬∀ (c : Config), (realize c).Nonempty

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.FactorsThrough (fun (c : { c : Config // c.tam = Tangale.TAM.perfective ∧ c.transitive = true ∧ c.focused ≠ Focused.subject }) => (↑c).focused) fun (c : { c : Config // c.tam = Tangale.TAM.perfective ∧ c.transitive = true ∧ c.focused ≠ Focused.subject }) => realize ↑c

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

Deriving the boundary ([Tru99]-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).

def HartmannZimmermann2004.ω : Prosody.Tree

A minimal prosodic word.

Equations

• HartmannZimmermann2004.ω = RoseTree.node Prosody.Constituent.om [RoseTree.node Prosody.Constituent.syl []]

def HartmannZimmermann2004.wrapped : Prosody.Tree

V and O wrapped into one φ.

Equations

• HartmannZimmermann2004.wrapped = RoseTree.node Prosody.Constituent.iota [RoseTree.node Prosody.Constituent.ph [HartmannZimmermann2004.ω, HartmannZimmermann2004.ω]]

def HartmannZimmermann2004.separated : Prosody.Tree

O separated into its own φ.

Equations

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

def HartmannZimmermann2004.phSpans (t : Prosody.Tree) : List (ℕ × ℕ)

phSpans t lists the spans of the φ nodes of t in preorder, each as the number of leaves to its left and the number of its own leaves.

Equations

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

def HartmannZimmermann2004.alignFocus : OptimalityTheory.Constraint Prosody.Tree

ALIGN-Focus is violated when no φ-edge sits at the focus's left edge (leaf offset 1, the object).

Equations

• HartmannZimmermann2004.alignFocus = OptimalityTheory.Constraint.binary fun (t : Prosody.Tree) => ¬∃ s ∈ HartmannZimmermann2004.phSpans t, s.1 = 1

def HartmannZimmermann2004.starPhi : OptimalityTheory.Constraint Prosody.Tree

Phrasal economy assigns one violation per φ.

Equations

• HartmannZimmermann2004.starPhi t = (HartmannZimmermann2004.phSpans t).length

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

Under object focus alignment dominates economy and the separated parse wins, which derives the φ-edge after the verb.

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

In an all-new utterance economy decides alone and the wrapped parse wins, so there is no boundary and the elision cascade applies.

theorem HartmannZimmermann2004.separated_edge_wrapped_internal : (0, 2) ∉ phSpans separated ∧ (0, 2) ∈ phSpans 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, since 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 exclusion Exhaustification.excludes.

structure HartmannZimmermann2004.NumWorld : Type

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

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

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

Equations

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

@[instance_reducible]

instance HartmannZimmermann2004.instDecidableEqNumWorld : DecidableEq NumWorld

Equations

• HartmannZimmermann2004.instDecidableEqNumWorld = HartmannZimmermann2004.instDecidableEqNumWorld.decEq

@[instance_reducible]

instance HartmannZimmermann2004.instReprNumWorld : Repr NumWorld

Equations

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

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

Equations

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

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 : Exhaustification.Irredundant alt

The alternatives are irredundant, since each can hold while the others fail, with one world per free Boolean field.

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

extAlts x is the contrast set of the association extent x, for the object ((36a), alternatives to the book), the VP ((36b), 'I did nothing else') and the 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) reading of an extent is the exclusion asserted by only over the resolved contrast set, with 'bought the book' as prejacent.

Equations

• HartmannZimmermann2004.numReading x = Exhaustification.excludes (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 has three semantically distinct readings. Over an irredundant alternative family only is injective in its resolution (Irredundant.excludes_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, since 'I did nothing else' entails both 'I bought nothing else' and 'I did nothing else to the book', by excludes_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.

def HartmannZimmermann2004.strategyLabel (c : Config) : String

Equations

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

def HartmannZimmermann2004.focusedLabel : Focused → String

Equations

• HartmannZimmermann2004.focusedLabel HartmannZimmermann2004.Focused.subject = "subject"
• HartmannZimmermann2004.focusedLabel HartmannZimmermann2004.Focused.verb = "verb"
• HartmannZimmermann2004.focusedLabel HartmannZimmermann2004.Focused.vp = "vp"
• HartmannZimmermann2004.focusedLabel HartmannZimmermann2004.Focused.object = "object"

def HartmannZimmermann2004.aspectLabel : Tangale.TAM → String

Equations

• HartmannZimmermann2004.aspectLabel Tangale.TAM.perfective = "perfective"
• HartmannZimmermann2004.aspectLabel Tangale.TAM.continuous = "progressive"
• HartmannZimmermann2004.aspectLabel x✝ = ""

def HartmannZimmermann2004.configRows : List (Config × Datum)

The paradigm cells paired with their data rows.

Equations

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

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

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