Baker & Vinokurova 2010: two modalities of case assignment in Sakha

Sakha's four structural cases split in half. Accusative and dative are dependent cases: an NP is valued accusative when a distinct caseless NP c-commands it in the clause, and dative when it c-commands one in the verb phrase, where there is no accusative rule. Nominative and genitive are assigned by T and D under agreement, and there is no elsewhere case: an NP that no rule and no head reaches must be pseudo-incorporated into the verb — an unshifted VP-internal NP adjacent to it — or the structure is out. Object shift makes differential object marking a phase effect; the causee of a causative is dative exactly when the base verb is transitive; a passive theme is accusative exactly when a covert agent is present; the object of an agentive nominalization is accusative though no v is present; a subject raised into an impersonal clause stays unmarked; and a finite verb agrees with an NP exactly when it values that NP nominative. A purely configurational grammar with elsewhere cases overgenerates the Case-filter and agreement violations, and a purely Agree-based grammar never values a dative, and an accusative only where a v probes.

Main definitions

• grammar: the two-modality grammar of Sakha.
• pureMarantz, pureChomsky: the two pure grammars beside it.
• subject, internal, possessor, pro, finite: the NP positions and the finite probe the paper's derivations use.
• Slot, candidates: the NPs of a row's domain from the slots the rows name, highest first; the covert agent and object shift are the free choices where the paper leaves them free.
• derive, Licensed, Agrees, Derivable: assignment with the probes a row's morphology shows, the Case filter, the case–agreement link, and derivability under some choice.

Main results

• dom, ditransitive, causative, passive, agentive_nominal, raising, promise, possessed: the paper's constructions.
• no_elsewhere_case, pureChomsky_no_dative, pureChomsky_v_of_acc: Sakha values nothing as unmarked, and an Agree-only grammar values nothing dative and an accusative only where a v probes, whatever the domain.
• rows_case: acceptability is derivability under the two-modality grammar.
• pure_marantz_overgenerates: without the Case filter and the agreement link, the configurational grammar derives rejected examples.

References

• [BV10]
• [Mar91] — dependent case
• [Cho00], [Cho01] — case under Agree and phases
• [Die92] — object shift of specific objects
• [Vin05] — the source of much of the data

The grammars

def BakerVinokurova2010.grammar : Minimalist.CaseAssigners

The Sakha grammar of structural case values dative on the higher of two NPs in the verb phrase, accusative on the lower of two in the clause, and nominative from T and genitive from D under Agree, with no elsewhere case in any domain.

Equations

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

def BakerVinokurova2010.pureMarantz : Minimalist.CaseAssigners

A purely configurational grammar has the dependent dative and accusative, elsewhere nominative in the clause and verb phrase and elsewhere genitive in the noun phrase, and no Agree.

Equations

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

def BakerVinokurova2010.pureChomsky : Minimalist.CaseAssigners

A purely Agree-based grammar values nominative from T, accusative from v and genitive from D, and has no dependent rule.

Equations

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

theorem BakerVinokurova2010.no_elsewhere_case {α : Type u_1} (np : α → Minimalist.PhasedNP) (probes : List (Minimalist.Cat × Minimalist.Cat)) {xs : List α} {i : ℕ} {x : α} {c : Case} {m : Case.Mechanism} (h : (grammar.assign np probes xs)[i]? = some (x, some (c, m))) : m ≠ Case.Mechanism.unmarked

Sakha values nothing as unmarked: an NP no rule and no head reaches stays caseless.

theorem BakerVinokurova2010.pureChomsky_no_dative {α : Type u_1} (np : α → Minimalist.PhasedNP) (probes : List (Minimalist.Cat × Minimalist.Cat)) {xs : List α} {i : ℕ} {x : α} {m : Case.Mechanism} (hx : xs[i]? = some x) (h : (pureChomsky.assign np probes xs)[i]? = some (x, some (Case.dat, m))) : (np x).lexicalCase = some Case.dat

The Agree-based grammar values nothing dative: a dative NP brought it from the lexicon.

theorem BakerVinokurova2010.pureChomsky_v_of_acc {α : Type u_1} (np : α → Minimalist.PhasedNP) (probes : List (Minimalist.Cat × Minimalist.Cat)) {xs : List α} {i : ℕ} {x : α} {m : Case.Mechanism} (hlex : (np x).lexicalCase = none) (h : (pureChomsky.assign np probes xs)[i]? = some (x, some (Case.acc, m))) : ∃ (d : Minimalist.Cat), (Minimalist.Cat.v, d) ∈ probes

The Agree-based grammar values an NP accusative only where a v probes: in a derivation without one, an accusative NP brought its case from the lexicon.

Positions

def BakerVinokurova2010.subject : Minimalist.PhasedNP

A caseless NP merged in the clause.

Equations

• BakerVinokurova2010.subject = { }

def BakerVinokurova2010.internal (shifted : Bool) : Minimalist.PhasedNP

A caseless NP merged in the verb phrase, shifted to the clause edge or not.

Equations

• BakerVinokurova2010.internal shifted = { phase := Minimalist.Cat.v, shifted := shifted }

def BakerVinokurova2010.possessor : Minimalist.PhasedNP

A caseless NP inside a noun phrase.

Equations

• BakerVinokurova2010.possessor = { phase := Minimalist.Cat.D }

def BakerVinokurova2010.pro : Minimalist.PhasedNP

The covert agent, merged in the clause.

Equations

• BakerVinokurova2010.pro = { }

def BakerVinokurova2010.finite : List (Minimalist.Cat × Minimalist.Cat)

Finite T probing the clause.

Equations

• BakerVinokurova2010.finite = [(Minimalist.Cat.T, Minimalist.Cat.C)]

def BakerVinokurova2010.cases (g : Minimalist.CaseAssigners) (probes : List (Minimalist.Cat × Minimalist.Cat)) (nps : List Minimalist.PhasedNP) : List (Option Case)

The cases of a derivation, positionally.

Equations

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

The constructions

theorem BakerVinokurova2010.dom (shifted : Bool) : cases grammar finite [subject, internal shifted] = [some Case.nom, if shifted = true then some Case.acc else none]

In differential object marking a shifted object is accusative and an unshifted one caseless, the subject nominative from T either way.

theorem BakerVinokurova2010.ditransitive (shifted : Bool) : cases grammar finite [subject, internal false, internal shifted] = [some Case.nom, some Case.dat, if shifted = true then some Case.acc else none]

In a ditransitive the goal is dative on the verb-phrase cycle whether or not the theme shifts, and the theme accusative exactly when it does; a causative of a transitive base is the same configuration, with the causee the higher of the two.

theorem BakerVinokurova2010.causative (shifted : Bool) : cases grammar finite [subject, internal false, internal shifted] = [some Case.nom, some Case.dat, if shifted = true then some Case.acc else none] ∧ cases grammar finite [subject, internal shifted] = [some Case.nom, if shifted = true then some Case.acc else none]

In a causative the causee of a transitive base is dative, c-commanding the theme in the verb phrase, and the causee of an intransitive base, alone there, is accusative once it shifts and never dative.

theorem BakerVinokurova2010.passive : cases grammar finite [pro, internal true] = [some Case.nom, some Case.acc] ∧ cases grammar finite [internal true] = [some Case.nom] ∧ cases grammar finite [pro, internal false, internal true] = [some Case.nom, some Case.dat, some Case.acc] ∧ cases grammar finite [internal false, internal true] = [some Case.dat, some Case.nom]

In a passive the shifted theme is accusative exactly when a covert agent is present, and nominative from T otherwise; a goal is dative either way.

theorem BakerVinokurova2010.agentive_nominal : cases grammar [] [pro, internal true] = [none, some Case.acc] ∧ cases grammar [] [internal true] = [none]

An agentive nominalization has no T, but its covert agent makes the shifted object accusative; without the agent the object is caseless.

theorem BakerVinokurova2010.raising : cases grammar finite [subject, internal true] = [some Case.nom, some Case.acc] ∧ cases grammar finite [internal true] = [some Case.nom]

A subject raised to the clause edge is accusative exactly when the matrix clause has another NP; into an impersonal clause it is valued by T alone.

theorem BakerVinokurova2010.promise : cases grammar finite [subject, internal false, internal true] = [some Case.nom, some Case.dat, some Case.acc] ∧ cases grammar finite [subject, internal true] = [some Case.nom, some Case.acc]

Under promise the goal is dative once the raised subject is below it in the verb phrase, and accusative when nothing is.

theorem BakerVinokurova2010.possessed : cases grammar (finite ++ [(Minimalist.Cat.D, Minimalist.Cat.D)]) [subject, possessor, internal true] = [some Case.nom, some Case.gen, some Case.acc]

A possessor is genitive from its D, and invisible to the clause.

theorem BakerVinokurova2010.elsewhere_contrast : cases grammar finite [subject, internal false] = [some Case.nom, none] ∧ cases grammar [] [subject] = [none] ∧ cases pureMarantz finite [subject, internal false] = [some Case.nom, some Case.nom] ∧ cases pureMarantz [] [subject] = [some Case.nom]

Without an elsewhere case, a caseless NP left in the verb phrase or a subject without an agreeing head stays caseless — the Case filter's bite — where the configurational grammar values both.

The rows

inductive BakerVinokurova2010.Slot : Type

The NP slots the rows name, in c-command order.

• subject : Slot
• causee : Slot
• goal : Slot
• raised : Slot
• object : Slot
• pObject : Slot
• possessor : Slot

@[instance_reducible]

instance BakerVinokurova2010.instDecidableEqSlot : DecidableEq Slot

Equations

• BakerVinokurova2010.instDecidableEqSlot x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance BakerVinokurova2010.instReprSlot : Repr Slot

Equations

• BakerVinokurova2010.instReprSlot = { reprPrec := BakerVinokurova2010.instReprSlot.repr }

def BakerVinokurova2010.instReprSlot.repr : Slot → ℕ → Std.Format

Equations

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

def BakerVinokurova2010.Slot.key : Slot → String

The prefix of a slot's feature keys.

Equations

• BakerVinokurova2010.Slot.subject.key = "subject"
• BakerVinokurova2010.Slot.causee.key = "causee"
• BakerVinokurova2010.Slot.goal.key = "goal"
• BakerVinokurova2010.Slot.raised.key = "raised"
• BakerVinokurova2010.Slot.object.key = "object"
• BakerVinokurova2010.Slot.pObject.key = "pObject"
• BakerVinokurova2010.Slot.possessor.key = "possessor"

def BakerVinokurova2010.Slot.all : List Slot

The slots highest first.

Equations

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

def BakerVinokurova2010.parseCase? : String → Option (Option Case)

The case a gloss shows, or nothing for a bare NP.

Equations

• BakerVinokurova2010.parseCase? "NOM" = some (some Case.nom)
• BakerVinokurova2010.parseCase? "bare" = some none
• BakerVinokurova2010.parseCase? "ACC" = some (some Case.acc)
• BakerVinokurova2010.parseCase? "DAT" = some (some Case.dat)
• BakerVinokurova2010.parseCase? "GEN" = some (some Case.gen)
• BakerVinokurova2010.parseCase? x✝ = none

def BakerVinokurova2010.Realizes (v : Option (Case × Case.Mechanism)) : Option Case → Prop

A valuation realizes a gloss: the case it shows, or, for a bare NP, no case or the nominative, which is unmarked.

Equations

• BakerVinokurova2010.Realizes v (some c) = (Option.map (fun (x : Case × Case.Mechanism) => x.1) v = some c)
• BakerVinokurova2010.Realizes v none = (Option.map (fun (x : Case × Case.Mechanism) => x.1) v = none ∨ Option.map (fun (x : Case × Case.Mechanism) => x.1) v = some Case.nom)

@[instance_reducible]

instance BakerVinokurova2010.instDecidableRealizes (v : Option (Case × Case.Mechanism)) (o : Option Case) : Decidable (Realizes v o)

Equations

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

def BakerVinokurova2010.yes (r : Datum) (k : String) : Bool

A row states a yes/no property.

Equations

• BakerVinokurova2010.yes r k = decide (r.feature? k = some "yes")

structure BakerVinokurova2010.Occupant : Type

An NP of a row's domain has its position, whether it is covert, whether it is adjacent to the verb, and the case its gloss shows.

• np : Minimalist.PhasedNP
• slot : Option Slot
• covert : Bool
• adjacent : Bool
• observed : Option Case

@[instance_reducible]

instance BakerVinokurova2010.instDecidableEqOccupant : DecidableEq Occupant

Equations

• BakerVinokurova2010.instDecidableEqOccupant = BakerVinokurova2010.instDecidableEqOccupant.decEq

def BakerVinokurova2010.instDecidableEqOccupant.decEq (x✝ x✝¹ : Occupant) : Decidable (x✝ = x✝¹)

Equations

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

def BakerVinokurova2010.instReprOccupant.repr : Occupant → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance BakerVinokurova2010.instReprOccupant : Repr Occupant

Equations

• BakerVinokurova2010.instReprOccupant = { reprPrec := BakerVinokurova2010.instReprOccupant.repr }

def BakerVinokurova2010.Slot.phase (r : Datum) : Slot → Minimalist.Cat

A possessor is merged in the noun phrase, the objects, goal, causee and raised subject in the verb phrase, and the subject in the clause unless the predicate is unaccusative or takes a dative subject.

Equations

• One or more equations did not get rendered due to their size.
• BakerVinokurova2010.Slot.phase r BakerVinokurova2010.Slot.causee = Minimalist.Cat.v
• BakerVinokurova2010.Slot.phase r BakerVinokurova2010.Slot.goal = Minimalist.Cat.v
• BakerVinokurova2010.Slot.phase r BakerVinokurova2010.Slot.raised = Minimalist.Cat.v
• BakerVinokurova2010.Slot.phase r BakerVinokurova2010.Slot.object = Minimalist.Cat.v
• BakerVinokurova2010.Slot.phase r BakerVinokurova2010.Slot.pObject = Minimalist.Cat.C
• BakerVinokurova2010.Slot.phase r BakerVinokurova2010.Slot.possessor = Minimalist.Cat.D

def BakerVinokurova2010.Slot.shifts (r : Datum) (s : Slot) : List Bool

A VP-merged NP shifts to the clause edge if it is specific and not if it is nonspecific, a raised subject always shifts, and the paper leaves the rest free.

Equations

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

def BakerVinokurova2010.Slot.occupants (r : Datum) (s : Slot) : Option (List Occupant)

The occupants a stated slot contributes, one per shift option.

Equations

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

def BakerVinokurova2010.agentOptions (r : Datum) : List (List Occupant)

The covert agent is forced in a passive with an agent-oriented adverb and in an agentive nominalization, excluded when the subject is overt or the predicate unaccusative, and otherwise free in a passive or event nominalization.

Equations

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

def BakerVinokurova2010.candidates (r : Datum) : List (List Occupant)

The domains a row may have are the covert agent, then each stated slot under each of its shift options.

Equations

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

def BakerVinokurova2010.probes (r : Datum) : List (Minimalist.Cat × Minimalist.Cat)

The probes a row's morphology shows are finite T where the verb agrees, the head noun's D reaching into the clause where it agrees with the subject, and the possessed noun's D where it agrees with its possessor.

Equations

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

def BakerVinokurova2010.derive (g : Minimalist.CaseAssigners) (r : Datum) (d : List Occupant) : Case.Valuation Occupant (Case × Case.Mechanism)

The valuations of a domain's occupants.

Equations

• BakerVinokurova2010.derive g r d = g.assign BakerVinokurova2010.Occupant.np (BakerVinokurova2010.probes r) d

def BakerVinokurova2010.Licensed (o : Occupant) (v : Option (Case × Case.Mechanism)) : Prop

The Case filter requires a caseless overt NP to be pseudo-incorporated, an unshifted VP-internal NP adjacent to the verb.

Equations

• BakerVinokurova2010.Licensed o v = (o.covert = true ∨ v.isSome = true ∨ o.np.phase = Minimalist.Cat.v ∧ o.np.shifted = false ∧ o.adjacent = true)

@[instance_reducible]

instance BakerVinokurova2010.instDecidableLicensed (o : Occupant) (v : Option (Case × Case.Mechanism)) : Decidable (Licensed o v)

Equations

• BakerVinokurova2010.instDecidableLicensed o v = id inferInstance

def BakerVinokurova2010.Agrees (r : Datum) (out : Case.Valuation Occupant (Case × Case.Mechanism)) : Prop

T agrees with the NP it values nominative: where a row states the verb's agreement target, an overt NP is nominative by Agree exactly when it is that target, so default agreement means no NP is.

Equations

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

@[instance_reducible]

instance BakerVinokurova2010.instDecidableAgrees (r : Datum) (out : Case.Valuation Occupant (Case × Case.Mechanism)) : Decidable (Agrees r out)

Equations

• BakerVinokurova2010.instDecidableAgrees r out = id inferInstance

def BakerVinokurova2010.Derives (g : Minimalist.CaseAssigners) (chomskian : Bool) (r : Datum) (d : List Occupant) : Prop

A domain derives the row under a grammar: every overt NP gets the case its gloss shows, and under the Chomskian half — the Case filter and the case–agreement link — is licensed and agreed with accordingly.

Equations

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

@[instance_reducible]

instance BakerVinokurova2010.instDecidableDerives (g : Minimalist.CaseAssigners) (chomskian : Bool) (r : Datum) (d : List Occupant) : Decidable (Derives g chomskian r d)

Equations

• BakerVinokurova2010.instDecidableDerives g chomskian r d = id inferInstance

def BakerVinokurova2010.Derivable (g : Minimalist.CaseAssigners) (chomskian : Bool) (r : Datum) : Prop

Some choice of structure derives the row.

Equations

• BakerVinokurova2010.Derivable g chomskian r = ∃ d ∈ BakerVinokurova2010.candidates r, BakerVinokurova2010.Derives g chomskian r d

@[instance_reducible]

instance BakerVinokurova2010.instDecidableDerivable (g : Minimalist.CaseAssigners) (chomskian : Bool) (r : Datum) : Decidable (Derivable g chomskian r)

Equations

• BakerVinokurova2010.instDecidableDerivable g chomskian r = id inferInstance

theorem BakerVinokurova2010.rows_case (r : Datum) : r ∈ Examples.all → (r.judgment = Judgment.acceptable ↔ Derivable grammar true r)

Each of the paper's Sakha examples is acceptable exactly when some structure derives the cases it shows under the two-modality grammar with the Case filter and the case–agreement link.

theorem BakerVinokurova2010.pure_marantz_overgenerates : ∃ r ∈ Examples.all, r.judgment ≠ Judgment.acceptable ∧ Derivable pureMarantz false r

Without the Case filter and the case–agreement link, the configurational grammar derives a rejected example — a bare object separated from the verb, an unagreed-with subject of a participial clause, a passive whose verb agrees with nothing though its theme is nominative.