Halpert (2012): Argument Licensing and Agreement in Zulu

Halpert argues that Zulu has structural licensing, but by heads other than the familiar ones. A Licensing head L⁰ above vP probes every phrase in vP and licenses the highest, and the verb V⁰ licenses its complement when a causative or applicative head has passed it a case feature, the pattern Halpert relates to Burzio's generalization. Nominals with the augment vowel and clauses headed by ukuthi are licensed intrinsically, while augmentless nominals and clauses headed by sengathi must be local to a licensing head in whichever vP they end up, and augmented nominals still intervene. An augmentless embedded subject may thus stay in the embedded vP or raise into the matrix vP, but not stop between. The verb shows L⁰'s probing, conjoint when it finds a goal and disjoint when it fails, and A-movement out of vP precedes the probing, the one order Chomsky's Activity Condition leaves.

Main definitions

• Halpert2012.Clause: a clause after A-movement, its vP split at V⁰'s c-command domain.
• Halpert2012.Clause.Converges: every phrase needing licensing is reached by L⁰ or V⁰.
• Halpert2012.Clause.spellout: the verb form L⁰'s probing determines.

Main results

• Halpert2012.Clause.converges_iff: the licensing generalization of §3.3.3.
• Halpert2012.Clause.countP_le_one, Halpert2012.Clause.countP_le_two: one phrase needing licensing in a vP without extensions, two with them.
• Halpert2012.Clause.spellout_eq_disjoint_iff: the verb is disjoint iff vP is empty.
• Halpert2012.search_eq_search_evacuate: under Activity, probing before A-movement reaches the goal probing after it reaches.
• Halpert2012.Clause.rows: the paradigms of chapters 3 and 4.

Implementation notes

Phrases that left vP or attach above it are listed in Clause.outside without positions. A row records the clause it is about and, when that clause is embedded, the clause embedding it, each licensed by its own L⁰; a raised phrase is recorded where it lands, and temporal adverbs whose position the source leaves open are not recorded. A prefixed oblique enters as the nominal inside it (§4.4.2), and noun class, which plays no role in licensing, is not recorded. Every row with an augmentless nominal is in a downward-entailing context, the semantic condition of §3.2.

TODO

That fisa 'wish' does not raise its embedded subject for most speakers ((152b)) is a lexical fact outside the model. Some speakers accept (141b) (footnote 8).

References

• [Hal12]
• [Bur86]
• [Cho00]
• [Cho01]

Goals

inductive Halpert2012.Goal : Type

A goal is a phrase that L⁰ can probe, and every phrase inside vP is one (§4.4).

• nominal (augment : Bool) : Goal

  The goal is a nominal, with or without the augment vowel.

• clause (c : Option Complementizer) : Goal

  The goal is a clause, headed by a complementizer or by none.

• adverb : Goal

  The goal is an adverb, such as kahle 'well'.

@[instance_reducible]

instance Halpert2012.instDecidableEqGoal : DecidableEq Goal

Equations

• Halpert2012.instDecidableEqGoal = Halpert2012.instDecidableEqGoal.decEq

def Halpert2012.instDecidableEqGoal.decEq (x✝ x✝¹ : Goal) : Decidable (x✝ = x✝¹)

Equations

• Halpert2012.instDecidableEqGoal.decEq (Halpert2012.Goal.nominal a) (Halpert2012.Goal.nominal b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Halpert2012.instDecidableEqGoal.decEq (Halpert2012.Goal.nominal augment) (Halpert2012.Goal.clause c) = isFalse ⋯
• Halpert2012.instDecidableEqGoal.decEq (Halpert2012.Goal.nominal augment) Halpert2012.Goal.adverb = isFalse ⋯
• Halpert2012.instDecidableEqGoal.decEq (Halpert2012.Goal.clause c) (Halpert2012.Goal.nominal augment) = isFalse ⋯
• Halpert2012.instDecidableEqGoal.decEq (Halpert2012.Goal.clause a) (Halpert2012.Goal.clause b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Halpert2012.instDecidableEqGoal.decEq (Halpert2012.Goal.clause c) Halpert2012.Goal.adverb = isFalse ⋯
• Halpert2012.instDecidableEqGoal.decEq Halpert2012.Goal.adverb (Halpert2012.Goal.nominal augment) = isFalse ⋯
• Halpert2012.instDecidableEqGoal.decEq Halpert2012.Goal.adverb (Halpert2012.Goal.clause c) = isFalse ⋯
• Halpert2012.instDecidableEqGoal.decEq Halpert2012.Goal.adverb Halpert2012.Goal.adverb = isTrue ⋯

def Halpert2012.instReprGoal.repr : Goal → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Halpert2012.instReprGoal : Repr Goal

Equations

• Halpert2012.instReprGoal = { reprPrec := Halpert2012.instReprGoal.repr }

def Halpert2012.Goal.NeedsL : Goal → Prop

A phrase needs structural licensing when it has no intrinsic licenser, that is, when it is a nominal without the augment or a clause headed by sengathi (Table 4.1).

Equations

• (Halpert2012.Goal.nominal augment).NeedsL = (augment = false)
• (Halpert2012.Goal.clause c).NeedsL = (c = some Zulu.sengathi)
• Halpert2012.Goal.adverb.NeedsL = False

@[instance_reducible]

instance Halpert2012.instDecidablePredGoalNeedsL : DecidablePred Goal.NeedsL

Equations

• Halpert2012.instDecidablePredGoalNeedsL (Halpert2012.Goal.nominal augment) = Halpert2012.instDecidablePredGoalNeedsL._aux_1 augment
• Halpert2012.instDecidablePredGoalNeedsL (Halpert2012.Goal.clause c) = Halpert2012.instDecidablePredGoalNeedsL._aux_3 c
• Halpert2012.instDecidablePredGoalNeedsL Halpert2012.Goal.adverb = { decide := false, reflects_decide := Halpert2012.instDecidablePredGoalNeedsL._proof_5 }

Licensing

inductive Halpert2012.Extension : Type

An extension is a verbal suffix that introduces an argument and a case feature, the causative -is- or the applicative -el- (§3.3.2).

• caus : Extension
• appl : Extension

@[instance_reducible]

instance Halpert2012.instDecidableEqExtension : DecidableEq Extension

Equations

• Halpert2012.instDecidableEqExtension x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Halpert2012.instReprExtension : Repr Extension

Equations

• Halpert2012.instReprExtension = { reprPrec := Halpert2012.instReprExtension.repr }

def Halpert2012.instReprExtension.repr : Extension → ℕ → Std.Format

Equations

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

structure Halpert2012.Clause : Type

A clause after A-movement (§4.5) records the phrases outside vP, the phrases in vP above V⁰'s c-command domain from the top, V⁰'s c-command domain with its complement first, and the verb's extensions.

• outside : List Goal
• above : List Goal
• vDomain : List Goal
• extensions : List Extension

@[instance_reducible]

instance Halpert2012.instDecidableEqClause : DecidableEq Clause

Equations

• Halpert2012.instDecidableEqClause = Halpert2012.instDecidableEqClause.decEq

def Halpert2012.instDecidableEqClause.decEq (x✝ x✝¹ : Clause) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Halpert2012.instReprClause : Repr Clause

Equations

• Halpert2012.instReprClause = { reprPrec := Halpert2012.instReprClause.repr }

def Halpert2012.instReprClause.repr : Clause → ℕ → Std.Format

Equations

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

def Halpert2012.Clause.vP (c : Clause) : List Goal

c.vP lists the phrases in vP from the top, L⁰'s search domain.

Equations

• c.vP = c.above ++ c.vDomain

def Halpert2012.Clause.L : Minimalist.Probe Goal

L⁰ is the indiscriminate probe, which every phrase satisfies, so that its search ends at the highest phrase in vP (pp. 168, 174).

Equations

• Halpert2012.Clause.L = Minimalist.Probe.indiscriminate

def Halpert2012.Clause.V : Minimalist.Probe Goal

V⁰ probes its c-command domain indiscriminately (142b).

Equations

• Halpert2012.Clause.V = Minimalist.Probe.indiscriminate

def Halpert2012.Clause.Inherits (c : Clause) : Prop

V⁰ licenses when an extension has passed it its case feature (142). There is one V⁰ however many extensions the verb carries, so a causative and an applicative together add one licenser, not two ((140), (141)).

Equations

• c.Inherits = (c.extensions ≠ [])

@[instance_reducible]

instance Halpert2012.Clause.instDecidablePredInherits : DecidablePred Inherits

Equations

• c.instDecidablePredInherits = { decide := !decide (c.extensions = []), reflects_decide := ⋯ }

def Halpert2012.Clause.Converges (c : Clause) : Prop

A clause converges when no phrase outside vP needs licensing and every phrase in vP that does is reached by L⁰'s search or, when V⁰ has inherited case, by V⁰'s search of its domain ((113), (122)). L⁰'s search reaches into V⁰'s domain only when nothing is above it, and then it reaches the phrase V⁰'s search reaches, so with case inheritance L⁰ licenses above V⁰'s domain and V⁰ within it.

Equations

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

@[instance_reducible]

instance Halpert2012.Clause.instDecidablePredConverges : DecidablePred Converges

Equations

• c.instDecidablePredConverges = id inferInstance

theorem Halpert2012.Clause.converges_iff {c : Clause} : c.Converges ↔ (∀ g ∈ c.outside, ¬g.NeedsL) ∧ (∀ g ∈ c.above.tail, ¬g.NeedsL) ∧ (∀ g ∈ c.vDomain.tail, ¬g.NeedsL) ∧ ∀ g ∈ c.vDomain.head?, g.NeedsL → c.above = [] ∨ c.Inherits

A clause converges iff each phrase needing licensing is the highest phrase of vP or of V⁰'s domain, the latter only when it is also highest in vP or V⁰ has inherited case, so that no phrase outside vP, between the two, or below either needs licensing (§3.3.3, p. 112).

theorem Halpert2012.Clause.countP_le_one {c : Clause} (h : c.Converges) (hc : c.extensions = []) : List.countP (fun (x : Goal) => decide x.NeedsL) c.vP ≤ 1

Without an extension one phrase in vP at most needs licensing (p. 93, (127)).

theorem Halpert2012.Clause.countP_le_two {c : Clause} (h : c.Converges) : List.countP (fun (x : Goal) => decide x.NeedsL) c.vP ≤ 2

Two phrases in vP at most need licensing, whatever extensions the verb carries (p. 105, (135), (141)).

The conjoint and disjoint verb forms

inductive Halpert2012.VerbForm : Type

A present-tense verb is conjoint, with ∅-, or disjoint, with ya- (§4.2).

• conjoint : VerbForm
• disjoint : VerbForm

@[instance_reducible]

instance Halpert2012.instDecidableEqVerbForm : DecidableEq VerbForm

Equations

• Halpert2012.instDecidableEqVerbForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Halpert2012.instReprVerbForm : Repr VerbForm

Equations

• Halpert2012.instReprVerbForm = { reprPrec := Halpert2012.instReprVerbForm.repr }

def Halpert2012.instReprVerbForm.repr : VerbForm → ℕ → Std.Format

Equations

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

def Halpert2012.Clause.spellout (c : Clause) : VerbForm

The verb is conjoint when L⁰'s search finds a goal in vP and disjoint, the overt member, when it fails, a failure that does not crash the derivation (§4.3, p. 166).

Equations

• c.spellout = match Halpert2012.Clause.L.outcome c.vP with | Minimalist.Probe.Outcome.valued => Halpert2012.VerbForm.conjoint | Minimalist.Probe.Outcome.unvalued => Halpert2012.VerbForm.disjoint

theorem Halpert2012.Clause.spellout_eq_disjoint_iff {c : Clause} : c.spellout = VerbForm.disjoint ↔ c.vP = []

The verb is disjoint iff vP is empty after A-movement, the generalization (180).

Timing

def Halpert2012.evacuate (base : List (Goal × Bool)) : List Goal

evacuate base is the vP left after A-movement, where base lists the phrases of vP from the top, each marked with whether it moves out (§4.5).

Equations

• Halpert2012.evacuate base = List.map Prod.fst (List.filter (fun (x : Halpert2012.Goal × Bool) => !x.2) base)

theorem Halpert2012.search_eq_search_evacuate {base : List (Goal × Bool)} (h : ∀ x ∈ base.head?, x.2 = false) : Clause.L.search (List.map Prod.fst base) = Clause.L.search (evacuate base)

Under the Activity Condition (270) L⁰'s goal cannot move once L⁰ has probed it, and then L⁰ probing before A-movement reaches the goal it reaches after, so ordering the two freely derives nothing that movement first does not (§4.5.1).

The paradigms

def Halpert2012.Goal.ofCode : String → Option Goal

Goal.ofCode s is the phrase that a row's code s names.

Equations

• Halpert2012.Goal.ofCode "+aug" = some (Halpert2012.Goal.nominal true)
• Halpert2012.Goal.ofCode "-aug" = some (Halpert2012.Goal.nominal false)
• Halpert2012.Goal.ofCode "cp" = some (Halpert2012.Goal.clause none)
• Halpert2012.Goal.ofCode "ukuthi" = some (Halpert2012.Goal.clause (some Zulu.ukuthi))
• Halpert2012.Goal.ofCode "sengathi" = some (Halpert2012.Goal.clause (some Zulu.sengathi))
• Halpert2012.Goal.ofCode "adverb" = some Halpert2012.Goal.adverb
• Halpert2012.Goal.ofCode x✝ = none

def Halpert2012.Extension.ofCode : String → Option Extension

Extension.ofCode s is the extension that a row's code s names.

Equations

• Halpert2012.Extension.ofCode "caus" = some Halpert2012.Extension.caus
• Halpert2012.Extension.ofCode "appl" = some Halpert2012.Extension.appl
• Halpert2012.Extension.ofCode x✝ = none

def Halpert2012.Clause.ofKeys (row : Datum) (outside above vDomain extension : String) : Option Clause

Clause.ofKeys row outside above vDomain extension is the clause whose phrases and extensions the row lists under the four keys.

Equations

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

def Halpert2012.Clause.ofRow (row : Datum) : Option Clause

Clause.ofRow row is the clause the row is about.

Equations

• Halpert2012.Clause.ofRow row = Halpert2012.Clause.ofKeys row "outside" "above" "vDomain" "extension"

def Halpert2012.Clause.matrixOfRow (row : Datum) : Option Clause

Clause.matrixOfRow row is the clause embedding it, empty when the row records none.

Equations

• Halpert2012.Clause.matrixOfRow row = Halpert2012.Clause.ofKeys row "matrixOutside" "matrixAbove" "matrixVDomain" "matrixExtension"

def Halpert2012.VerbForm.ofRow (row : Datum) : Option VerbForm

VerbForm.ofRow row is the verb form the row records, where the alternation shows.

Equations

• Halpert2012.VerbForm.ofRow row = row.parse? "verbForm" [("conjoint", Halpert2012.VerbForm.conjoint), ("disjoint", Halpert2012.VerbForm.disjoint)]

theorem Halpert2012.Clause.rows (row : Datum) : row ∈ Examples.all → ∀ c ∈ ofRow row, ∀ m ∈ matrixOfRow row, row.judgment = Judgment.acceptable ↔ m.Converges ∧ c.Converges ∧ ∀ f ∈ VerbForm.ofRow row, c.spellout = f

A sentence of the paradigms of chapters 3 and 4 is acceptable exactly when its clause and the clause embedding it converge, each licensed by its own L⁰, and its verb form, where recorded, spells out L⁰'s probing.