Derivational Positions

@cite{abels-2012} @cite{erlewine-2016} @cite{erlewine-2018} @cite{chomsky-1995}

Derives positional information (specifier vs. complement) from merge history, following the Minimalist view that position is derivational, not representational.

In bare phrase structure, node X Y does not encode which daughter is the specifier and which is the complement. That information lives in the derivation: the first external Merge into a projection creates the complement; the second creates the specifier; internal Merge (movement) always creates a specifier/edge.

This module defines MergeEvent records that track derivational position and derives anti-locality constraints and the predicate- fronting extraction restriction from them.

Anti-Locality

Two variants are formalized:

1. Complement-to-Spec: the complement of a head H cannot move to Spec,HP. Restated positionally here; the original formulation is in Phase.lean.

2. Spec-to-Spec (@cite{erlewine-2016}): movement from Spec,XP to Spec,YP is blocked when YP immediately dominates XP (no intervening maximal projection). Originally proposed for Agent Focus in Kaqchikel (@cite{erlewine-2016}). Also interacts with Toba Batak clause structure (@cite{erlewine-2018}).

inductive Minimalist.MergeType : Type

How a constituent came to occupy its position in the tree.

This is a derivational property: it records which Merge operation placed the constituent, not where it sits in the final tree.

• extComp : MergeType

  First external merge into a projection: complement position. E.g., V merges with DP_obj → DP_obj is complement of V.

• extSpec : MergeType

  Second external merge into a projection: specifier position. E.g., DP_subj merges with v' → DP_subj is specifier of vP.

• intSpec : MergeType

  Internal merge (movement): specifier/edge position. E.g., wh-phrase moves to Spec,CP.

def Minimalist.instReprMergeType.repr : MergeType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprMergeType : Repr MergeType

Equations

• Minimalist.instReprMergeType = { reprPrec := Minimalist.instReprMergeType.repr }

@[implicit_reducible]

instance Minimalist.instDecidableEqMergeType : DecidableEq MergeType

Equations

• Minimalist.instDecidableEqMergeType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Minimalist.MergeEvent : Type

A record of one Merge operation's positional consequence.

Given a derivation, each Merge step produces a MergeEvent recording what was merged, into which projection, and what positional slot the merged element occupies.

The result field stores the SO after this merge — useful for inspecting the representational state at any derivational point.

• target : SyntacticObject

  The projection being extended (the "target" of Merge)

• daughter : SyntacticObject

  The constituent merged into that projection

• result : SyntacticObject

  The resulting SO after this Merge

• mtype : MergeType

  What positional slot the daughter occupies

@[implicit_reducible]

instance Minimalist.instReprMergeEvent : Repr MergeEvent

Equations

• Minimalist.instReprMergeEvent = { reprPrec := Minimalist.instReprMergeEvent.repr }

def Minimalist.instReprMergeEvent.repr : MergeEvent → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instDecidableEqMergeEvent : DecidableEq MergeEvent

Equations

• Minimalist.instDecidableEqMergeEvent = Minimalist.instDecidableEqMergeEvent.decEq

def Minimalist.instDecidableEqMergeEvent.decEq (x✝ x✝¹ : MergeEvent) : Decidable (x✝ = x✝¹)

Equations

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

def Minimalist.isSpecIn (events : List MergeEvent) (x y : SyntacticObject) : Prop

X is a specifier of Y in event history events: some merge placed X into Y's projection as a specifier.

Equations

• Minimalist.isSpecIn events x y = ∃ e ∈ events, e.daughter = x ∧ e.target = y ∧ (e.mtype = Minimalist.MergeType.extSpec ∨ e.mtype = Minimalist.MergeType.intSpec)

def Minimalist.isCompIn (events : List MergeEvent) (x y : SyntacticObject) : Prop

X is a complement of Y in event history events.

Equations

• Minimalist.isCompIn events x y = ∃ e ∈ events, e.daughter = x ∧ e.target = y ∧ e.mtype = Minimalist.MergeType.extComp

def Minimalist.movedToSpecOf (events : List MergeEvent) (x y : SyntacticObject) : Prop

X moved to the specifier of Y via internal merge.

Equations

• Minimalist.movedToSpecOf events x y = ∃ e ∈ events, e.daughter = x ∧ e.target = y ∧ e.mtype = Minimalist.MergeType.intSpec

def Minimalist.compToSpecAntiLocality (events : List MergeEvent) (x h : SyntacticObject) : Prop

Complement-to-Spec anti-locality, restated positionally.

If X is the complement of H, then X cannot move to Spec,HP. This is the canonical formulation of @cite{abels-2012}'s anti-locality constraint (Ch. 4): the complement of a phase head cannot raise to its edge because no maximal projection intervenes.

Equations

• Minimalist.compToSpecAntiLocality events x h = (Minimalist.isCompIn events x h → ¬Minimalist.movedToSpecOf events x h)

def Minimalist.specToSpecAntiLocality (events : List MergeEvent) (mover xP yP : SyntacticObject) : Prop

Spec-to-Spec anti-locality.

Movement from Spec,XP to Spec,YP is blocked when YP immediately dominates XP — i.e., when there is no intervening maximal projection. This is "too local": Ā-movement must cross at least one full projection boundary.

In Toba Batak, this prevents the pivot in Spec,TP from moving to Spec,CP clause-internally (fn. 24, @cite{erlewine-2018}), though the primary extraction restriction derives from nominal licensing.

Equations

• Minimalist.specToSpecAntiLocality events mover xP yP = (Minimalist.isSpecIn events mover xP → Minimalist.immediatelyContains yP xP → ¬Minimalist.movedToSpecOf events mover yP)

structure Minimalist.PredicateFronting : Type

Predicate fronting: VP/vP moves to Spec,CP via internal merge.

This derives V-initial word order in languages like Toba Batak. The predicate occupies a specifier (edge) position in the C-domain, leaving the subject/pivot stranded in Spec,TP.

• predicate : SyntacticObject

  The predicate phrase that fronts (VP or vP)

• cProjection : SyntacticObject

  The C-domain projection it fronts to

• events : List MergeEvent

  The derivation events

• fronted : movedToSpecOf self.events self.predicate self.cProjection

  The predicate was internal-merged to Spec,CP

def Minimalist.isStranded (pf : PredicateFronting) (x : SyntacticObject) : Prop

After predicate fronting, a constituent X is "stranded" if it is NOT inside the fronted predicate. Stranded elements remain accessible for further operations (e.g., extraction by a higher probe).

Equations

• Minimalist.isStranded pf x = ¬Minimalist.contains pf.predicate x

def Minimalist.isTrapped (pf : PredicateFronting) (x : SyntacticObject) : Prop

After predicate fronting, a constituent X is "trapped" if it IS inside the fronted predicate. Trapped elements are inaccessible: the fronted phrase is a moved constituent and acts as a freezing domain.

Equations

• Minimalist.isTrapped pf x = Minimalist.contains pf.predicate x

theorem Minimalist.stranded_or_trapped (pf : PredicateFronting) (x : SyntacticObject) : isStranded pf x ∨ isTrapped pf x

Stranded and trapped are complementary: every constituent of the clause is either stranded or trapped (tertium non datur).

def Minimalist.extractionRestriction (pf : PredicateFronting) (extractee : SyntacticObject) : Prop

The extraction restriction in predicate-fronting languages: only stranded elements (those outside the fronted predicate) can undergo further Ā-extraction.

Equations

• Minimalist.extractionRestriction pf extractee = Minimalist.isStranded pf extractee

structure Minimalist.Pivot : Type

The pivot: the element stranded by predicate fronting. It sits in Spec,TP, outside the fronted VP, and is therefore the only argument accessible for extraction.

• element : SyntacticObject

  The pivot element

• tProjection : SyntacticObject

  The TP whose specifier it occupies

• events : List MergeEvent

  Derivation events

• inSpecTP : isSpecIn self.events self.element self.tProjection

  The pivot sits in Spec,TP

theorem Minimalist.pivot_is_stranded (pf : PredicateFronting) (pivot : Pivot) (h_outside : ¬contains pf.predicate pivot.element) : extractionRestriction pf pivot.element

The pivot satisfies the extraction restriction: it is stranded (outside the fronted predicate), hence extractable.

theorem Minimalist.nonpivot_trapped (pf : PredicateFronting) (x : SyntacticObject) (h_inside : contains pf.predicate x) : ¬extractionRestriction pf x

Non-pivot arguments are trapped (inside the fronted predicate), hence not extractable.

theorem Minimalist.pivot_blocked_by_anti_locality (events : List MergeEvent) (pivot tP cP : SyntacticObject) (h_spec : isSpecIn events pivot tP) (h_imm : immediatelyContains cP tP) (h_anti : specToSpecAntiLocality events pivot tP cP) : ¬movedToSpecOf events pivot cP

Anti-locality prevents the pivot from moving to Spec,CP in its own clause: Spec,TP → Spec,CP is too local.

The pivot thus stays in Spec,TP. It does NOT move clause-internally, but it remains accessible to a higher probe because it sits at the edge of its clause, outside the fronted predicate.

structure Minimalist.CyclicPosition : Type

A successive-cyclic position: an intermediate landing site in Ā-movement. Each such site is a Spec of a phase head (Spec,vP or Spec,CP) that the moving element passes through.

In Toba Batak, each intermediate C checks [+Pred] against the passing wh-copy, yielding extraction morphology. In Mam, each intermediate Voice⁰ Agrees [+oblique], yielding =(y)a'. Both are modeled as entries in a CyclicChain.

The agreeResult field records whether Agree occurred at this position. When the mover passes through a phase head that probes for features (e.g., Voice with [uOblique]), Agree values the probe's features. The valued features can then be spelled out morphologically — this is how multiple =(y)a' arise in Mam long-distance extraction (one per Voice along the chain).

• mover : SyntacticObject

  The moving element

• projection : SyntacticObject

  The projection whose specifier it temporarily occupies

• events : List MergeEvent

  Derivation events

• passedThrough : movedToSpecOf self.events self.mover self.projection

  Evidence that the mover passed through this spec

• agreeResult : Option FeatureBundle

  Features on the probe head at this position after Agree, if Agree occurred. none = no probe at this position (e.g., a non-phase edge). some fb = the probe's valued features, ready for Spellout (e.g., [+oblique] on Voice → =(y)a').

structure Minimalist.CyclicChain : Type

A successive-cyclic chain: the ordered sequence of intermediate landing sites an element occupies during long-distance movement.

• mover : SyntacticObject

  The moving element

• positions : List CyclicPosition

  Intermediate positions, ordered from lowest to highest

• sameMover (p : CyclicPosition) : p ∈ self.positions → p.mover = self.mover

  All positions involve the same mover

def Minimalist.CyclicChain.agreeCount (chain : CyclicChain) : ℕ

Count cyclic positions where Agree occurred (features were valued). In Mam, this equals the number of =(y)a' morphemes expected in long-distance extraction: one per Voice/Dir along the chain.

Equations

• chain.agreeCount = (List.filter (fun (x : Minimalist.CyclicPosition) => x.agreeResult.isSome) chain.positions).length

def Minimalist.CyclicChain.agreedFeatures (chain : CyclicChain) : List FeatureBundle

Extract the agreed feature bundles from a chain, in order. Each some fb corresponds to a position where Agree occurred, yielding features that will be spelled out at PF.

Equations

• chain.agreedFeatures = List.filterMap (fun (x : Minimalist.CyclicPosition) => x.agreeResult) chain.positions