Poole (2024): Dependent-case assignment could be Agree

This file formalizes [Poo24]'s argument that dependent case, the innovation of [Mar91]'s configurational model, can be assigned by Agree. A head carries the probe stack (8): a φ-probe relativized to unmarked case, which values on the closest caseless DP and so records that a second DP is present, followed by a case-assigning probe with the same relativization, active only once the first is valued and, by the Principle of Minimal Compliance, blind to the first probe's goal ([RR05]). Low dependent case comes from a stack on a head above both DPs, which meets them in c-command order; high dependent case from a stack on the head that introduces the higher DP, which searches its complement and then, by specifier–head Agree ([BR09]), the specifier it merges with. Either way the stack assigns nothing with fewer than two caseless DPs in its domain and never marks the DP that unlocked it (stack_eq_none_of_subsingleton, stack_ne_unlocker).

On a two-DP domain the stack assigns exactly what the dependent rule of the configurational model assigns, low or high, whatever lexical case the DPs carry (low_eq_dependentPass, high_eq_dependentPass); this is the paper's translation of any configurational account into an Agree account. The two mechanisms part on a third caseless DP, which the configurational rule also marks and a single stack, discharged once, does not (stack_marks_once). The Sakha illustration of §5 puts a dative stack on V and an accusative stack on T; on every clause shape of table (19) the two stacks assign the cases that the dative and accusative rules of [BV10] assign (sakha_eq_bakerVinokurova), and accusative appears on a DP exactly when it is accessible to T and another caseless DP unlocks the stack, as in (15), (18) and (20) (accusative_rows).

Implementation notes

Probes are the substrate's Probe.search over goals paired with their positions, so that minimal compliance is the removal of the unlocking position and case is assigned by position; the two-DP theorems then hold for arbitrary DPs and lexical cases by computation. What the stack assigns is recorded as valued by Agree, the configurational rule as valued by a dependent rule, and the theorems compare the cases, which is the extensional equivalence the paper argues for; the provenance is where the two models differ by design. Unmarked case, case discrimination below the unmarked setting, and the negative c-command rules of §6.1 are not formalized.

References

• [Poo24]
• [Mar91]
• [BV10]
• [RR05]
• [BR09]

The dependent-case probe stack (8)

@[reducible, inline]

abbrev Poole2024.Goal (α : Type u_2) : Type u_2

A goal as a head sees it: an NP with its current valuation, at its position among the goals the head encounters.

Equations

• Poole2024.Goal α = ((α × Option (Case × Case.Mechanism)) × ℕ)

def Poole2024.unmarkedProbe {α : Type u_1} : Minimalist.Probe (Goal α)

The φ-probe relativized to unmarked case: it sees exactly the caseless DPs.

Equations

• Poole2024.unmarkedProbe = Minimalist.Probe.relativized fun (g : Poole2024.Goal α) => g.1.2.isNone

def Poole2024.stack {α : Type u_1} (goals : Case.Valuation α (Case × Case.Mechanism)) : Option ℕ

The stack (8) over the goals a head encounters in order: the position of the DP assigned dependent case, if the first probe finds a caseless DP to unlock the second and the second, ignoring that DP, finds another.

Equations

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

def Poole2024.assignDep {α : Type u_1} (c : Case) (goals : Case.Valuation α (Case × Case.Mechanism)) : Case.Valuation α (Case × Case.Mechanism)

The stack assigning the case c: the DP it finds is valued c by Agree, every other goal is left as it was.

Equations

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

def Poole2024.surface {α : Type u_1} (out : Case.Valuation α (Case × Case.Mechanism)) : List (Option Case)

The cases a list of valued NPs carries.

Equations

• Poole2024.surface out = List.map (fun (x : α × Option (Case × Case.Mechanism)) => Option.map (fun (x : Case × Case.Mechanism) => x.1) x.2) out

theorem Poole2024.stack_eq_none_of_subsingleton {α : Type u_1} {goals : Case.Valuation α (Case × Case.Mechanism)} (h : ∀ (i j : ℕ), ∀ g ∈ List.zipIdx goals, ∀ g' ∈ List.zipIdx goals, g.2 = i → g'.2 = j → g.1.2 = none → g'.1.2 = none → i = j) : stack goals = none

With fewer than two caseless DPs among its goals the stack assigns nothing: the first probe is never valued, or the second finds no DP.

theorem Poole2024.stack_ne_unlocker {α : Type u_1} {goals : Case.Valuation α (Case × Case.Mechanism)} {g : Goal α} {j : ℕ} (hs : unmarkedProbe.search (List.zipIdx goals) = some g) (hj : stack goals = some j) : j ≠ g.2

Minimal compliance: the DP that unlocks the stack is not the one it marks.

Low and high dependent case against the configurational rules

theorem Poole2024.low_eq_dependentPass {α : Type u_1} (c : Case) (lex : α → Option Case) (a b : α) : surface (assignDep c (Case.lexicalValuation lex [a, b])) = surface ({ low := some c }.dependentPass (fun (x : α) => true) (Case.lexicalValuation lex [a, b]))

Low dependent case (10): a stack on a head above two DPs meets them in c-command order and assigns the lower one what the low dependent rule assigns, whatever lexical case either carries.

theorem Poole2024.high_eq_dependentPass {α : Type u_1} (c : Case) (lex : α → Option Case) (spec comp : α) : (surface (assignDep c (Case.lexicalValuation lex [comp, spec]))).reverse = surface ({ high := some c }.dependentPass (fun (x : α) => true) (Case.lexicalValuation lex [spec, comp]))

High dependent case (11): a stack on the head introducing the higher DP searches its complement first and its specifier last, and assigns the specifier what the high dependent rule assigns, whatever lexical case either carries.

theorem Poole2024.stack_marks_once {α : Type u_1} (c : Case) (lex : α → Option Case) (a b d : α) (ha : lex a = none) (hb : lex b = none) (hd : lex d = none) : surface (assignDep c (Case.lexicalValuation lex [a, b, d])) = [none, some c, none] ∧ surface ({ low := some c }.dependentPass (fun (x : α) => true) (Case.lexicalValuation lex [a, b, d])) = [none, some c, some c]

One stack, one dependent case: on three caseless DPs the stack marks only the second, whereas the low dependent rule marks every DP c-commanded by a caseless one.

Sakha (§5)

structure Poole2024.Shape : Type

A Sakha clause shape of table (19): whether it has an external argument, an indirect object in the specifier of VP, and a direct object in the complement of VP, the last either shifted out of the VP phase or not.

• ea : Bool
• io : Bool
• dobj : Option Bool

@[instance_reducible]

instance Poole2024.instDecidableEqShape : DecidableEq Shape

Equations

• Poole2024.instDecidableEqShape = Poole2024.instDecidableEqShape.decEq

def Poole2024.instDecidableEqShape.decEq (x✝ x✝¹ : Shape) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Poole2024.instReprShape : Repr Shape

Equations

• Poole2024.instReprShape = { reprPrec := Poole2024.instReprShape.repr }

def Poole2024.instReprShape.repr : Shape → ℕ → Std.Format

Equations

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

inductive Poole2024.Arg : Type

The three arguments: the external argument, the indirect object and the direct object.

• EA : Arg
• IO : Arg
• DO : Arg

@[instance_reducible]

instance Poole2024.instDecidableEqArg : DecidableEq Arg

Equations

• Poole2024.instDecidableEqArg x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Poole2024.instReprArg.repr : Arg → ℕ → Std.Format

Equations

• Poole2024.instReprArg.repr Poole2024.Arg.EA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Poole2024.Arg.EA")).group prec✝
• Poole2024.instReprArg.repr Poole2024.Arg.IO prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Poole2024.Arg.IO")).group prec✝
• Poole2024.instReprArg.repr Poole2024.Arg.DO prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Poole2024.Arg.DO")).group prec✝

@[instance_reducible]

instance Poole2024.instReprArg : Repr Arg

Equations

• Poole2024.instReprArg = { reprPrec := Poole2024.instReprArg.repr }

def Poole2024.Shape.vGoals (s : Shape) : Case.Valuation Arg (Case × Case.Mechanism)

The goals V meets: its complement, the direct object, then its specifier, the indirect object.

Equations

• s.vGoals = (Option.map (fun (x : Bool) => (Poole2024.Arg.DO, none)) s.dobj).toList ++ if s.io = true then [(Poole2024.Arg.IO, none)] else []

def Poole2024.Shape.tGoals (s : Shape) (vp : Case.Valuation Arg (Case × Case.Mechanism)) : Case.Valuation Arg (Case × Case.Mechanism)

The goals T meets after V's stack has run: the external argument, then the direct object if it has shifted out of VP; the indirect object stays in the VP phase.

Equations

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

def Poole2024.Shape.agree (s : Shape) : Option Case × Option Case × Option Case

The cases of the external argument, the indirect object, and the direct object after the dative stack on V and the accusative stack on T ([Poo24] (16), (17)).

Equations

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

def Poole2024.Shape.bakerVinokurova (s : Shape) : Option Case × Option Case × Option Case

The cases after the dative rule (14a) in the VP phase, the indirect object above the direct object, and the accusative rule (14b) in the clause.

Equations

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

theorem Poole2024.sakha_eq_bakerVinokurova (s : Shape) : s.agree = s.bakerVinokurova

Table (19): on every clause shape the two stacks assign what the two dependent rules assign.

def Poole2024.tGoals (licensor accessible : Bool) : Case.Valuation Arg (Case × Case.Mechanism)

The goals of T's accusative stack in (15), (18) and (20): another caseless DP, if any, then the DP in question, if accessible to T.

Equations

• Poole2024.tGoals licensor accessible = (if licensor = true then [(Poole2024.Arg.EA, none)] else []) ++ if accessible = true then [(Poole2024.Arg.DO, none)] else []

def Poole2024.interpret (r : Datum) : Option (Bool × Bool × Bool)

A row's accusative marking, accessibility, and licensor, read from its features.

Equations

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

def Poole2024.Predicted (r : Datum) : Prop

A row is predicted: it is acceptable exactly when it carries accusative just in case T's stack assigns it.

Equations

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

@[instance_reducible]

instance Poole2024.instDecidablePredicted (r : Datum) : Decidable (Predicted r)

Equations

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

theorem Poole2024.accusative_rows (r : Datum) : r ∈ Examples.all → Predicted r

(15), (18), (20): the shifted direct object and the raised embedded subject are accusative exactly when another caseless DP unlocks T's stack; the unshifted object and the subject with no matrix DP are not.