Docs / Syntax / Minimalist / Case / Assignment

Case assignment by phase

import Linglib.Syntax.Minimalist.Case.Assignment · namespace Minimalist

The configurational rules of Syntax/Case/Dependent.lean run domain by domain, innermost first, each phase head's domain with its own high, low and elsewhere cases, and functional heads value case under Agree on the closest caseless NP they reach, which is what a relativized probe finds; a value once assigned is kept, so a dative valued in the verb phrase survives the clause. A language's case assigners are the rules of each phase head's domain and the case each head values under Agree, so configurational, Agree-based and hybrid systems are points in one space. Assignment is a fold over domains; CaseAssigners.assign builds them from NPs placed by hand, and Case/SyntacticObject.lean reads them off an object.

Implementation notes

A value once assigned is never replaced. Baker and Vinokurova let a later domain re-mark an NP and spell out its innermost case (their (15)), which agrees with this wherever the outer case is not overt.

References

Baker & Vinokurova 2010, Two Modalities of Case Assignment: Case in Sakha formalized
Baker 2015, Case: Its Principles and Its Parameters formalized
Chomsky 2000, Minimalist Inquiries: The Framework
Preminger 2014, Agreement and Its Failures formalized

Agree

Agree into the domain D: the closest goal in D, the goals being its unvalued NPs, is valued with v. Goals neither of which c-commands the other are all closest, and all are valued.

def agree L51–54

{ι : Type u_1} {κ : Type u_2} [DecidableEq ι] (lt : ι → ι → Prop) [DecidableRel lt] (v : κ) (D : Finset ι) (s : ι → FeatureSlot κ) :

ι → FeatureSlot κ

agree lt v D s = CaseRule.passUnvalued lt (CaseRule.inOrder [v]) D s

Used by agree_apply, extends_agree, agree_eq_unvalued_of_forall, map_agree, agree_eq_search

Used in Kalin2018

agree is Agree: a probe relativized to unvalued NPs, the activity condition of Chomsky 2000, searches the domain in c-command order, and the goal it finds is valued while every other NP is left as it is; if it finds none, nothing changes, the failed Agree of Preminger 2014.

theorem agree_eq_search L106–142

{ι : Type u_1} {κ : Type u_2} [DecidableEq ι] {lt : ι → ι → Prop} [DecidableRel lt] {s : ι → FeatureSlot κ} {v : κ} {xs : List ι} [Std.Asymm lt] (hxs : List.Pairwise lt xs) :

agree lt v xs.toFinset s = ((Probe.relativized fun (x : ι) => s x = FeatureSlot.unvalued).search xs).elim s fun (x : ι) => Function.update s x (FeatureSlot.valued v)

Built from

Positions set by hand

Case assigners

L172–179

Assignment over domains

One domain of case assignment: c-command among its NPs, its dependent rule and the NPs that rule reads and values, its probes with the value each gives and the NPs each reaches, and its elsewhere rule and the NPs that rule values.

structure CaseDomain L183–199

(ι : Type u_1) (κ : Type u_2) :

Type (max u_1 u_2)

above : ι → ι → Prop
C-command among the NPs of the domain.
decAbove : DecidableRel self.above
dependent : CaseRule κ
The dependent rule.
sees : Finset ι
The NPs the dependent rule reads and values.
probes : List (κ × Finset ι)
The probes, each with the value it gives and the NPs it reaches.
elsewhere : CaseRule κ
The elsewhere rule.
spellOut : Finset ι
The NPs the elsewhere rule values.

Used by CaseDomain.pass, CaseDomain.values, CaseDomain.extends_pass, assignBy, extends_assignBy, CaseAssigners.domain

L207–211

L213–215

L217–225

Assignment over the domains ds, innermost first.

def assignBy L227–229

{ι : Type u_1} {κ : Type u_2} [DecidableEq ι] (ds : List (CaseDomain ι κ)) (s : ι → FeatureSlot κ) :

ι → FeatureSlot κ

assignBy ds s = List.foldl (fun (st : ι → FeatureSlot κ) (d : CaseDomain ι κ) => d.pass st) s ds

Built from ,

Used by extends_assignBy, CaseAssigners.assign

L231–235

Assignment over NPs placed by hand

L245–250

L254–261

Case for the NPs U placed by hand, lt their c-command, the domains spelling out in order.

def CaseAssigners.assign L263–266

{ι : Type u_1} (g : CaseAssigners) (U : Finset ι) (np : ι → PhasedNP) [DecidableEq ι] (lt : ι → ι → Prop) [DecidableRel lt] (probes : List (Cat × Cat)) (order : List Cat) :

ι → FeatureSlot (Case × Case.Mechanism)

g.assign U np lt probes order = assignBy (List.map (g.domain U np lt probes) order) (Case.lexical fun (x : ι) => (np x).case)

Built from , , ,

Used by CaseAssigners.of_assign_eq_valued

Used in BakerVinokurova2010, Kalin2018

L268–287