Dependent case

Structural case read off the arrangement of NPs in a domain, under a disjunctive hierarchy: case a lexical head has valued is kept; otherwise an NP that c-commands a distinct caseless NP in the domain takes the domain's high case and one c-commanded by such an NP its low case, the two rules reading the same configuration, so a domain with both marks the higher NP and the lower NP at once; whatever remains takes the domain's elsewhere case. Which of the two dependent rules a clause has is its alignment: accusative, ergative, tripartite or neutral. The passes are generic in what an NP is, so a phase-cyclic grammar can run them domain by domain.

Main definitions

• Case.Mechanism: what valued a case, a lexical head, a dependent rule, Agree, or the elsewhere case, shared by every account of case assignment.
• Case.lexicalValuation: the valuation of NPs by lexical case.
• DependentCase.Rules: the high, low and elsewhere cases of one domain, and Rules.ofAlignment, the rules of an alignment.
• Rules.dependentPass, Rules.unmarkedPass: the passes, over the NPs a predicate selects.
• Rules.valuations: the valuations the rules can assign.
• Rules.assign, assignCases: the one-domain algorithm, and its form for an alignment.

Main results

• Rules.dependentPass_high, Rules.dependentPass_low, Rules.dependentPass_alone: what the dependent rules do to an NP with a caseless NP below it, above it, or neither.
• Rules.extends_dependentPass, Rules.extends_unmarkedPass, Rules.extends_assign: each pass extends the valuation by what the rules assign.
• Rules.assign_length: the algorithm is total.
• Rules.assign_getElem?_of_some: lexical case is kept, so it bleeds the dependent rules.
• Rules.case_mem_cases: a caseless NP is valued only with a case the rules mention.
• Rules.assign_singleton, Rules.assign_pair: the algorithm in closed form on domains of one and two NPs.
• Rules.classifies_marking_ofAlignment: the rules of an alignment mark S, A and P with that alignment.

Implementation notes

List position encodes structural height: earlier is higher, and c-commands everything later. The NPs are of any type, identified by that type rather than by a label; a study's NPs are its own positions, and Valuation.valueOf reads off the case of one. The passes are Valuation.fill, so what they share (totality, persistence of values) comes from Case.Valuation.Extends.

References

• [Mar91]
• [Bak15]

Mechanisms

inductive Case.Mechanism : Type

What valued a case: a lexical head, a dependent rule, Agree with a functional head, or the elsewhere case of its domain.

• lexical : Mechanism
• dependent : Mechanism
• agree : Mechanism
• unmarked : Mechanism

@[instance_reducible]

instance Case.instDecidableEqMechanism : DecidableEq Mechanism

Equations

• Case.instDecidableEqMechanism x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Case.instReprMechanism : Repr Mechanism

Equations

• Case.instReprMechanism = { reprPrec := Case.instReprMechanism.repr }

def Case.instReprMechanism.repr : Mechanism → ℕ → Std.Format

Equations

• Case.instReprMechanism.repr Case.Mechanism.lexical prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.Mechanism.lexical")).group prec✝
• Case.instReprMechanism.repr Case.Mechanism.dependent prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.Mechanism.dependent")).group prec✝
• Case.instReprMechanism.repr Case.Mechanism.agree prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.Mechanism.agree")).group prec✝
• Case.instReprMechanism.repr Case.Mechanism.unmarked prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.Mechanism.unmarked")).group prec✝

The lexical valuation

def Case.lexicalValuation {α : Type u_1} (lexicalCase : α → Option Case) (xs : List α) : Valuation α (Case × Mechanism)

Every NP with its lexical case valued and nothing else.

Equations

• Case.lexicalValuation lexicalCase xs = Case.Valuation.initial (fun (x : α) => Option.map (fun (x : Case) => (x, Case.Mechanism.lexical)) (lexicalCase x)) xs

theorem Case.lexicalValuation_getElem?_of_some {α : Type u_1} (lexicalCase : α → Option Case) {xs : List α} {i : ℕ} {x : α} {c : Case} (hx : xs[i]? = some x) (hc : lexicalCase x = some c) : (lexicalValuation lexicalCase xs)[i]? = some (x, some (c, Mechanism.lexical))

theorem Case.lexicalValuation_getElem? {α : Type u_1} {lexicalCase : α → Option Case} {xs : List α} {i : ℕ} {x : α} {v : Case × Mechanism} (h : (lexicalValuation lexicalCase xs)[i]? = some (x, some v)) : lexicalCase x = some v.1 ∧ v.2 = Mechanism.lexical

Rules

structure DependentCase.Rules : Type

The rules of one domain: the case of an NP c-commanding a distinct caseless NP in it, the case of one c-commanded by such an NP, and the elsewhere case.

• high : Option Case
• low : Option Case
• unmarked : Option Case

def DependentCase.instDecidableEqRules.decEq (x✝ x✝¹ : Rules) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance DependentCase.instDecidableEqRules : DecidableEq Rules

Equations

• DependentCase.instDecidableEqRules = DependentCase.instDecidableEqRules.decEq

def DependentCase.instReprRules.repr : Rules → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DependentCase.instReprRules : Repr Rules

Equations

• DependentCase.instReprRules = { reprPrec := DependentCase.instReprRules.repr }

def DependentCase.Rules.cases (r : Rules) : List Case

The cases the rules can value a caseless NP with.

Equations

• r.cases = List.filterMap id [r.high, r.low, r.unmarked]

theorem DependentCase.Rules.high_mem_cases {r : Rules} {c : Case} (h : r.high = some c) : c ∈ r.cases

theorem DependentCase.Rules.low_mem_cases {r : Rules} {c : Case} (h : r.low = some c) : c ∈ r.cases

theorem DependentCase.Rules.unmarked_mem_cases {r : Rules} {c : Case} (h : r.unmarked = some c) : c ∈ r.cases

def DependentCase.Rules.ofAlignment : Alignment.AlignmentType → Rules

The clausal rules of an alignment: accusative on the lower NP, ergative on the higher, both, or neither, with the elsewhere case nominative where the lower NP is marked and absolutive otherwise. A split-S system is not a dependent-case setting and gets the neutral rules.

Equations

• DependentCase.Rules.ofAlignment Alignment.AlignmentType.accusative = { low := some Case.acc, unmarked := some Case.nom }
• DependentCase.Rules.ofAlignment Alignment.AlignmentType.ergative = { high := some Case.erg, unmarked := some Case.abs }
• DependentCase.Rules.ofAlignment Alignment.AlignmentType.tripartite = { high := some Case.erg, low := some Case.acc, unmarked := some Case.abs }
• DependentCase.Rules.ofAlignment Alignment.AlignmentType.neutral = { unmarked := some Case.nom }
• DependentCase.Rules.ofAlignment Alignment.AlignmentType.active = { unmarked := some Case.nom }

The passes

def DependentCase.Rules.dependentPass {α : Type u_1} (r : Rules) (P : α → Bool) (s : Case.Valuation α (Case × Case.Mechanism)) : Case.Valuation α (Case × Case.Mechanism)

The dependent rules over the NPs P selects: the high case goes to those c-commanding another and the low case to those c-commanded by another, both read off the same configuration; an NP in both positions takes the high case.

Equations

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

def DependentCase.Rules.unmarkedPass {α : Type u_1} (r : Rules) (P : α → Bool) (s : Case.Valuation α (Case × Case.Mechanism)) : Case.Valuation α (Case × Case.Mechanism)

The elsewhere case to the unvalued NPs P selects.

Equations

• r.unmarkedPass P s = Case.Valuation.fill (fun (x : ℕ) (x_1 : α) => if P x_1 = true then Option.map (fun (x : Case) => (x, Case.Mechanism.unmarked)) r.unmarked else none) s

def DependentCase.Rules.assign {α : Type u_1} (r : Rules) (lex : α → Option Case) (xs : List α) : Case.Valuation α (Case × Case.Mechanism)

Case for every NP of one domain, lex giving the case a lexical head has valued: the dependent rules, then the elsewhere case.

Equations

• r.assign lex xs = r.unmarkedPass (fun (x : α) => true) (r.dependentPass (fun (x : α) => true) (Case.lexicalValuation lex xs))

def DependentCase.assignCases {α : Type u_1} (a : Alignment.AlignmentType) (lex : α → Option Case) (xs : List α) : Case.Valuation α (Case × Case.Mechanism)

The one-domain algorithm of an alignment.

Equations

• DependentCase.assignCases a lex xs = (DependentCase.Rules.ofAlignment a).assign lex xs

What the passes assign

def DependentCase.Rules.valuations (r : Rules) : Set (Case × Case.Mechanism)

The valuations the rules can assign: a dependent case, or the elsewhere case.

Equations

• r.valuations = {v : Case × Case.Mechanism | v.2 = Case.Mechanism.dependent ∧ (r.high = some v.1 ∨ r.low = some v.1) ∨ v.2 = Case.Mechanism.unmarked ∧ r.unmarked = some v.1}

theorem DependentCase.Rules.fst_mem_cases {r : Rules} {v : Case × Case.Mechanism} (h : v ∈ r.valuations) : v.1 ∈ r.cases

theorem DependentCase.Rules.extends_dependentPass {α : Type u_1} (r : Rules) (P : α → Bool) (s : Case.Valuation α (Case × Case.Mechanism)) : Case.Valuation.Extends (fun (x : Case × Case.Mechanism) => x ∈ r.valuations) s (r.dependentPass P s)

theorem DependentCase.Rules.extends_unmarkedPass {α : Type u_1} (r : Rules) (P : α → Bool) (s : Case.Valuation α (Case × Case.Mechanism)) : Case.Valuation.Extends (fun (x : Case × Case.Mechanism) => x ∈ r.valuations) s (r.unmarkedPass P s)

theorem DependentCase.Rules.extends_assign {α : Type u_1} (r : Rules) (lex : α → Option Case) (xs : List α) : Case.Valuation.Extends (fun (x : Case × Case.Mechanism) => x ∈ r.valuations) (Case.lexicalValuation lex xs) (r.assign lex xs)

Assignment extends the lexical valuation by what the rules assign.

@[simp]

theorem DependentCase.Rules.assign_length {α : Type u_1} (r : Rules) (lex : α → Option Case) (xs : List α) : List.length (r.assign lex xs) = xs.length

The algorithm is total: one valuation per NP.

theorem DependentCase.Rules.assign_getElem?_of_some {α : Type u_1} (r : Rules) {lex : α → Option Case} {xs : List α} {i : ℕ} {x : α} {c : Case} (hx : xs[i]? = some x) (hc : lex x = some c) : (r.assign lex xs)[i]? = some (x, some (c, Case.Mechanism.lexical))

Lexical case is kept, so it bleeds the dependent rules.

theorem DependentCase.Rules.case_mem_cases {α : Type u_1} (r : Rules) {lex : α → Option Case} {xs : List α} {i : ℕ} {x : α} {c : Case} {m : Case.Mechanism} (hlex : lex x = none) (h : (r.assign lex xs)[i]? = some (x, some (c, m))) : c ∈ r.cases

A caseless NP is valued only with a case the rules mention.

What the dependent rules do

theorem DependentCase.Rules.dependentPass_high {α : Type u_1} (r : Rules) (P : α → Bool) {s : Case.Valuation α (Case × Case.Mechanism)} {i j : ℕ} {x : α} {c : Case} (hx : s[i]? = some (x, none)) (hP : P x = true) (hj : j ∈ Case.Valuation.unvalued P s) (hij : i < j) (hc : r.high = some c) : (r.dependentPass P s)[i]? = some (x, some (c, Case.Mechanism.dependent))

A caseless NP with a caseless NP below it in the domain takes the high case.

theorem DependentCase.Rules.dependentPass_low {α : Type u_1} (r : Rules) (P : α → Bool) {s : Case.Valuation α (Case × Case.Mechanism)} {i j : ℕ} {x : α} {c : Case} (hx : s[i]? = some (x, none)) (hP : P x = true) (hj : j ∈ Case.Valuation.unvalued P s) (hji : j < i) (hhigh : r.high = none ∨ ∀ k ∈ Case.Valuation.unvalued P s, ¬i < k) (hc : r.low = some c) : (r.dependentPass P s)[i]? = some (x, some (c, Case.Mechanism.dependent))

A caseless NP with a caseless NP above it in the domain, and none below it that the high rule could mark it for, takes the low case.

theorem DependentCase.Rules.dependentPass_alone {α : Type u_1} (r : Rules) (P : α → Bool) {s : Case.Valuation α (Case × Case.Mechanism)} {i : ℕ} {x : α} (hx : s[i]? = some (x, none)) (halone : ∀ j ∈ Case.Valuation.unvalued P s, j = i) : (r.dependentPass P s)[i]? = some (x, none)

A caseless NP alone in its domain is untouched by the dependent rules.

theorem DependentCase.Rules.unmarkedPass_of_none {α : Type u_1} (r : Rules) (P : α → Bool) (h : r.unmarked = none) (s : Case.Valuation α (Case × Case.Mechanism)) : r.unmarkedPass P s = s

With no elsewhere case the pass does nothing.

theorem DependentCase.Rules.dependentPass_of_none {α : Type u_1} (r : Rules) (P : α → Bool) (hh : r.high = none) (hl : r.low = none) (s : Case.Valuation α (Case × Case.Mechanism)) : r.dependentPass P s = s

With neither dependent case the pass does nothing.

Domains of one and two NPs

def DependentCase.Rules.elsewhere (r : Rules) (lexical : Option Case) : Option (Case × Case.Mechanism)

The valuation of an NP no dependent rule reaches: its lexical case, or the elsewhere case.

Equations

• r.elsewhere lexical = (Option.map (fun (x : Case) => (x, Case.Mechanism.lexical)) lexical).or (Option.map (fun (x : Case) => (x, Case.Mechanism.unmarked)) r.unmarked)

theorem DependentCase.Rules.assign_singleton {α : Type u_1} (r : Rules) (lex : α → Option Case) (x : α) : r.assign lex [x] = [(x, r.elsewhere (lex x))]

A sole NP is never reached by a dependent rule.

theorem DependentCase.Rules.assign_pair {α : Type u_1} (r : Rules) (lex : α → Option Case) (x y : α) : r.assign lex [x, y] = [(x, if lex x = none ∧ lex y = none ∧ r.high.isSome = true then Option.map (fun (x : Case) => (x, Case.Mechanism.dependent)) r.high else r.elsewhere (lex x)), (y, if lex x = none ∧ lex y = none ∧ r.low.isSome = true then Option.map (fun (x : Case) => (x, Case.Mechanism.dependent)) r.low else r.elsewhere (lex y))]

Of two NPs the dependent rules reach both or neither: when neither has lexical case, the higher takes the high case and the lower the low case, where the rules have one.

Alignment

def DependentCase.Rules.marking (r : Rules) (x : ArgumentRole) : Option Case

The marking the rules give the core roles: S alone in its domain, and A above P in theirs.

Equations

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

theorem DependentCase.Rules.classifies_marking_ofAlignment {a : Alignment.AlignmentType} (ha : a ≠ Alignment.AlignmentType.active) : a.Classifies (ofAlignment a).marking

The rules of an alignment mark the core roles with that alignment.

Alignments on a transitive and an intransitive clause

theorem DependentCase.assignCases_transitive : have xs := [0, 1]; List.map (fun (x : Fin 2 × Option (Case × Case.Mechanism)) => Option.map (fun (x : Case × Case.Mechanism) => x.1) x.2) (assignCases Alignment.AlignmentType.accusative (fun (x : Fin 2) => none) xs) = [some Case.nom, some Case.acc] ∧ List.map (fun (x : Fin 2 × Option (Case × Case.Mechanism)) => Option.map (fun (x : Case × Case.Mechanism) => x.1) x.2) (assignCases Alignment.AlignmentType.ergative (fun (x : Fin 2) => none) xs) = [some Case.erg, some Case.abs] ∧ List.map (fun (x : Fin 2 × Option (Case × Case.Mechanism)) => Option.map (fun (x : Case × Case.Mechanism) => x.1) x.2) (assignCases Alignment.AlignmentType.tripartite (fun (x : Fin 2) => none) xs) = [some Case.erg, some Case.acc]

Two caseless NPs: the accusative rules value the lower accusative and leave the higher nominative, the ergative rules mirror this, and the tripartite rules do both.

theorem DependentCase.assignCases_intransitive (a : Alignment.AlignmentType) : Option.map (fun (x : Case × Case.Mechanism) => x.2) (Case.Valuation.valueOf () (assignCases a (fun (x : Unit) => none) [()])) = some Case.Mechanism.unmarked

A sole caseless NP takes the elsewhere case under every alignment.