Dependent case by phase

The configurational rules of Syntax/Case/Dependent.lean run domain by domain: each phase head's spell-out domain has its own high, low and elsewhere cases, the domains spell out innermost first, and a case valued in an inner domain — or by a lexical head — is never overwritten, so a dative valued in the verb phrase survives the clause. Functional heads may also value case under Agree, each probing the highest caseless NP of the domain it agrees into. A grammar is the table of domain rules together with the Agree cases, so a purely configurational grammar, a purely Agree-based one, and the hybrids are points in one space. Which functional heads a derivation contains is a fact about it, so assignment takes the probes present with the domain each agrees into.

Main definitions

• PhasedNP: an NP with the phase head whose domain merges it, and whether it has shifted to the clause edge.
• CaseGrammar: the phase heads in spell-out order with their rules, and the Agree cases.
• CaseGrammar.assign: case for every NP of a derivation.

Main results

• CaseGrammar.assign_length: assignment is total.
• CaseGrammar.assign_getElem?_of_some: lexical case is kept.
• CaseGrammar.case_mem_cases: a caseless NP is valued only with a case the grammar mentions.

References

• [baker-vinokurova-2010]
• [baker-2015]
• [chomsky-2000], [chomsky-2001]

structure Minimalist.PhasedNPextends Case.NP : Type

An NP with its position: the phase head whose spell-out domain merges it, and whether it has shifted to the clause edge, where C's domain spells it out.

• label : String
• lexicalCase : Option Case
• phase : Cat
• shifted : Bool

def Minimalist.instDecidableEqPhasedNP.decEq (x✝ x✝¹ : PhasedNP) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Minimalist.instDecidableEqPhasedNP : DecidableEq PhasedNP

Equations

• Minimalist.instDecidableEqPhasedNP = Minimalist.instDecidableEqPhasedNP.decEq

def Minimalist.instReprPhasedNP.repr : PhasedNP → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Minimalist.instReprPhasedNP : Repr PhasedNP

Equations

• Minimalist.instReprPhasedNP = { reprPrec := Minimalist.instReprPhasedNP.repr }

def Minimalist.PhasedNP.visible (np : PhasedNP) (c : Cat) : Bool

Whether the NP is in the domain of c when it spells out.

Equations

• np.visible c = (np.phase == c || np.shifted && c == Minimalist.Cat.C)

def Minimalist.PhasedNP.spellOut (np : PhasedNP) : Cat

The phase head whose elsewhere case the NP falls back on.

Equations

• np.spellOut = if np.shifted = true then Minimalist.Cat.C else np.phase

structure Minimalist.CaseGrammar : Type

A grammar of structural case: the phase heads in spell-out order with the rules of their domains, and the case each functional head values under Agree.

• domains : List (Cat × Case.Rules)
• agree : List (Cat × Case)

@[instance_reducible]

instance Minimalist.instDecidableEqCaseGrammar : DecidableEq CaseGrammar

Equations

• Minimalist.instDecidableEqCaseGrammar = Minimalist.instDecidableEqCaseGrammar.decEq

def Minimalist.instDecidableEqCaseGrammar.decEq (x✝ x✝¹ : CaseGrammar) : Decidable (x✝ = x✝¹)

Equations

• Minimalist.instDecidableEqCaseGrammar.decEq { domains := a, agree := a_1 } { domains := b, agree := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Minimalist.instReprCaseGrammar.repr : CaseGrammar → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Minimalist.instReprCaseGrammar : Repr CaseGrammar

Equations

• Minimalist.instReprCaseGrammar = { reprPrec := Minimalist.instReprCaseGrammar.repr }

def Minimalist.CaseGrammar.rules (g : CaseGrammar) (c : Cat) : Case.Rules

The rules of the domain of c.

Equations

• g.rules c = (Option.map (fun (x : Minimalist.Cat × Case.Rules) => x.2) (List.find? (fun (x : Minimalist.Cat × Case.Rules) => x.1 == c) g.domains)).getD { }

def Minimalist.CaseGrammar.agreeCase (g : CaseGrammar) (h : Cat) : Option Case

The case h values under Agree, if any.

Equations

• g.agreeCase h = Option.map (fun (x : Minimalist.Cat × Case) => x.2) (List.find? (fun (x : Minimalist.Cat × Case) => x.1 == h) g.agree)

def Minimalist.CaseGrammar.cases (g : CaseGrammar) : List Case

The cases the grammar can value a caseless NP with.

Equations

• g.cases = List.flatMap (fun (x : Minimalist.Cat × Case.Rules) => x.2.cases) g.domains ++ List.map (fun (x : Minimalist.Cat × Case) => x.2) g.agree

def Minimalist.CaseGrammar.alignment (g : CaseGrammar) : Alignment.AlignmentType

The alignment the clausal rules show.

Equations

• g.alignment = (g.rules Minimalist.Cat.C).alignment

def Minimalist.agreePass (c : Case) (P : PhasedNP → Bool) (states : List (PhasedNP × Case.Valuation)) : List (PhasedNP × Case.Valuation)

A head valuing c under Agree in the domain P selects values its highest unvalued NP.

Equations

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

def Minimalist.probePass (g : CaseGrammar) (c h : Cat) (states : List (PhasedNP × Case.Valuation)) : List (PhasedNP × Case.Valuation)

The head h probing the domain of c: it values what the grammar lets it.

Equations

• Minimalist.probePass g c h states = match g.agreeCase h with | some k => Minimalist.agreePass k (fun (x : Minimalist.PhasedNP) => x.visible c) states | none => states

def Minimalist.domainPass (g : CaseGrammar) (probes : List (Cat × Cat)) (c : Cat) (states : List (PhasedNP × Case.Valuation)) : List (PhasedNP × Case.Valuation)

One spell-out domain: its dependent rules, then its probes in order, then its elsewhere case.

Equations

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

def Minimalist.CaseGrammar.assign (g : CaseGrammar) (probes : List (Cat × Cat)) (nps : List PhasedNP) : List (Case.NP × Case.Valuation)

Case for every NP, the domains spelling out in the grammar's order. probes lists the functional heads present with the phase head whose domain each agrees into.

Equations

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

Totality

@[simp]

theorem Minimalist.agreePass_length (c : Case) (P : PhasedNP → Bool) (states : List (PhasedNP × Case.Valuation)) : (agreePass c P states).length = states.length

@[simp]

theorem Minimalist.probePass_length (g : CaseGrammar) (c h : Cat) (states : List (PhasedNP × Case.Valuation)) : (probePass g c h states).length = states.length

@[simp]

theorem Minimalist.domainPass_length (g : CaseGrammar) (probes : List (Cat × Cat)) (c : Cat) (states : List (PhasedNP × Case.Valuation)) : (domainPass g probes c states).length = states.length

@[simp]

theorem Minimalist.CaseGrammar.assign_length (g : CaseGrammar) (probes : List (Cat × Cat)) (nps : List PhasedNP) : (g.assign probes nps).length = nps.length

Assignment is total: one valuation per NP.

Valued NPs persist

theorem Minimalist.agreePass_getElem?_of_some (c : Case) (P : PhasedNP → Bool) {states : List (PhasedNP × Case.Valuation)} {i : ℕ} {np : PhasedNP} {v : Case × Case.Mechanism} (h : states[i]? = some (np, some v)) : (agreePass c P states)[i]? = some (np, some v)

theorem Minimalist.probePass_getElem?_of_some (g : CaseGrammar) (c hd : Cat) {states : List (PhasedNP × Case.Valuation)} {i : ℕ} {np : PhasedNP} {v : Case × Case.Mechanism} (h : states[i]? = some (np, some v)) : (probePass g c hd states)[i]? = some (np, some v)

theorem Minimalist.domainPass_getElem?_of_some (g : CaseGrammar) (probes : List (Cat × Cat)) (c : Cat) {states : List (PhasedNP × Case.Valuation)} {i : ℕ} {np : PhasedNP} {v : Case × Case.Mechanism} (h : states[i]? = some (np, some v)) : (domainPass g probes c states)[i]? = some (np, some v)

theorem Minimalist.CaseGrammar.assign_getElem?_of_some (g : CaseGrammar) (probes : List (Cat × Cat)) {nps : List PhasedNP} {i : ℕ} {np : PhasedNP} {c : Case} (hnp : nps[i]? = some np) (hc : np.lexicalCase = some c) : (g.assign probes nps)[i]? = some (np.toNP, some (c, Case.Mechanism.lexical))

Lexical case is kept through every domain.

The cases a grammar values

theorem Minimalist.CaseGrammar.rules_cases_subset (g : CaseGrammar) (c : Cat) : (g.rules c).cases ⊆ g.cases

theorem Minimalist.CaseGrammar.agreeCase_mem_cases {g : CaseGrammar} {h : Cat} {c : Case} (hc : g.agreeCase h = some c) : c ∈ g.cases

theorem Minimalist.CaseGrammar.case_mem_cases (g : CaseGrammar) (probes : List (Cat × Cat)) {nps : List PhasedNP} {i : ℕ} {np : Case.NP} {c : Case} {m : Case.Mechanism} (hlex : np.lexicalCase = none) (h : (g.assign probes nps)[i]? = some (np, some (c, m))) : c ∈ g.cases

A caseless NP is valued only with a case the grammar mentions.

A grammar without an elsewhere case

theorem Minimalist.CaseGrammar.rules_unmarked_of (g : CaseGrammar) (hg : ∀ d ∈ g.domains, d.2.unmarked = none) (c : Cat) : (g.rules c).unmarked = none

theorem Minimalist.CaseGrammar.mechanism_ne_unmarked (g : CaseGrammar) (probes : List (Cat × Cat)) (hg : ∀ d ∈ g.domains, d.2.unmarked = none) {nps : List PhasedNP} {i : ℕ} {np : Case.NP} {c : Case} {m : Case.Mechanism} (h : (g.assign probes nps)[i]? = some (np, some (c, m))) : m ≠ Case.Mechanism.unmarked

A grammar with no elsewhere case in any domain never values an NP as unmarked: an NP that no rule and no head reaches stays caseless.