Docs / Syntax / Minimalist / Case / SyntacticObject

Case on syntactic objects

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

Case is read off an object with traces, phase by phase. The domain of a phase head sees the NPs with a copy in what it transfers on its own (transferSlice), ordered by asymmetric c-command between those copies; its probes are the heads with an Agree case whose complement it transfers, each reaching the copies it c-commands there; and its elsewhere case goes to the NPs whose pronounced copy it transfers. An NP that shifts to the edge of a phase is thus seen by the phase through its lower copy and by the next phase through its higher one, and PhasedNP, the order of the NPs and the probes of a derivation are all read off the object. Assignment is assignBy over the phase heads innermost first, of which the calculus over NPs placed by hand is another instance by definition (CaseAssigners.assign).

Main definitions

Minimalist.copiesAt: the copies of an NP in what a phase transfers on its own.
Minimalist.VisibleAt, Minimalist.SpelledOutAt: an NP seen by a phase, and spelled out there.
Minimalist.CCommandsAt, Minimalist.ReachesAt: c-command among the NPs of a phase, and the NPs a head reaches there.
Minimalist.projectingHeads, Minimalist.phaseHeads: the heads that project, and the phase heads, deepest first.
Minimalist.CaseAssigners.probesAt: the probes of a phase.
Minimalist.CaseAssigners.assignOn: case for the NPs of an object.

Implementation notes

Copies count wherever they stand, the representational reading Baker and Vinokurova mention in their note 6. They note that it needs copies in A-bar positions not to count (note 7): an object scrambled above the subject within one phase ((16), (17)) would otherwise make each the other's competitor. No such proviso is modelled.

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
Chomsky 2001, Derivation by Phase

Declarations

The copies of an NP standing in what the phase head at h transfers on its own, each at the projection of its token.

def copiesAt L59–62

(hd : HeadFunction) (t : LinearizedSyntacticObject) (Φ : Finset Core.Order.TreePath) (D : Core.Order.TreePath → Set Core.Order.TreePath) [(h : Core.Order.TreePath) → DecidablePred fun (x : Core.Order.TreePath) => x ∈ D h] (h : Core.Order.TreePath) (tok : LexicalItem.Token) :

List Core.Order.TreePath

The definition is too large to print here; read it in the source.

Used by VisibleAt, CCommandsAt, ReachesAt, instDecidableVisibleAt

An NP is seen by the phase head at h when a copy of it stands in what h transfers.

def VisibleAt L64–65

Prop

VisibleAt hd t Φ D h tok = (copiesAt hd t Φ D h tok ≠ [])

Built from

Used by instDecidableVisibleAt

An NP is spelled out by the phase head at h when its pronounced copy stands in what h transfers.

def SpelledOutAt L67–70

(hd : HeadFunction) (t : LinearizedSyntacticObject) (Φ : Finset Core.Order.TreePath) (D : Core.Order.TreePath → Set Core.Order.TreePath) (h : Core.Order.TreePath) (tok : LexicalItem.Token) :

Prop

SpelledOutAt hd t Φ D h tok = ∃ p ∈ occurrences t tok, projectionAt hd t p ∈ transferSlice Φ D h

Used by instDecidableSpelledOutAt

In what h transfers, x c-commands y when a copy of x there asymmetrically c-commands a copy of y there.

def CCommandsAt L72–76

Prop

CCommandsAt hd t Φ D h x y = ∃ p ∈ copiesAt hd t Φ D h x, ∃ q ∈ copiesAt hd t Φ D h y, (↑t).CCommands p q ∧ ¬(↑t).CCommands q p

Built from

Used by instDecidableRelTokenCCommandsAt

The head at a reaches an NP when it c-commands a copy of it standing in what h transfers.

def ReachesAt L78–81

Prop

ReachesAt hd t Φ D h a tok = ∃ p ∈ copiesAt hd t Φ D h tok, (↑t).CCommands a p

Built from

Used by instDecidableReachesAt

The heads of t that project, deepest first: the pronounced tokens heading their mothers.

def projectingHeads L95–100

(hd : HeadFunction) (t : LinearizedSyntacticObject) :

List (Core.Order.TreePath × LexicalItem.Token)

The definition is too large to print here; read it in the source.

Used by phaseHeads

The probes of the phase head at h: the heads with an Agree case whose complement it transfers, deepest first, each with its case and the NPs of U it reaches.

def CaseAssigners.probesAt L102–109

List ((Case × Case.Mechanism) × Finset LexicalItem.Token)

The definition is too large to print here; read it in the source.

The phase heads of t with their positions, innermost first.

def phaseHeads L111–114

(hd : HeadFunction) (t : LinearizedSyntacticObject) (IsPhaseHead : LexicalItem.Token → Prop) [DecidablePred IsPhaseHead] :

List (Core.Order.TreePath × LexicalItem.Token)

phaseHeads hd t IsPhaseHead = List.filter (fun (x : Core.Order.TreePath × LexicalItem.Token) => decide (IsPhaseHead x.2)) (projectingHeads hd t)

Built from

Case for the NPs xs of t, phase by phase innermost first, D giving the domain of each phase head and case the case slot each NP enters with.

def CaseAssigners.assignOn L116–131

(hd : HeadFunction) (t : LinearizedSyntacticObject) (g : CaseAssigners) (D : Core.Order.TreePath → Set Core.Order.TreePath) [(h : Core.Order.TreePath) → DecidablePred fun (x : Core.Order.TreePath) => x ∈ D h] (IsPhaseHead : LexicalItem.Token → Prop) [DecidablePred IsPhaseHead] (case : LexicalItem.Token → FeatureSlot Case) (xs : List LexicalItem.Token) :

LexicalItem.Token → FeatureSlot (Case × Case.Mechanism)

The definition is too large to print here; read it in the source.