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 Minimalism.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.

instance Minimalism.instReprMergeType : Repr MergeType

Equations

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

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

Equations

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

instance Minimalism.instDecidableEqMergeType : DecidableEq MergeType

Equations

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

def Minimalism.instBEqMergeType.beq : MergeType → MergeType → Bool

Equations

• Minimalism.instBEqMergeType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Minimalism.instBEqMergeType : BEq MergeType

Equations

• Minimalism.instBEqMergeType = { beq := Minimalism.instBEqMergeType.beq }

def Minimalism.MergeType.isSpec : MergeType → Bool

Is this a specifier position (external or via movement)?

Equations

• Minimalism.MergeType.extSpec.isSpec = true
• Minimalism.MergeType.intSpec.isSpec = true
• Minimalism.MergeType.extComp.isSpec = false

def Minimalism.MergeType.isMovement : MergeType → Bool

Was this position created by movement?

Equations

• Minimalism.MergeType.intSpec.isMovement = true
• x✝.isMovement = false

structure Minimalism.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

instance Minimalism.instReprMergeEvent : Repr MergeEvent

Equations

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

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

Equations

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

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

Equations

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

instance Minimalism.instDecidableEqMergeEvent : DecidableEq MergeEvent

Equations

• Minimalism.instDecidableEqMergeEvent = Minimalism.instDecidableEqMergeEvent.decEq

def Minimalism.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

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

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

X is a complement of Y in event history events.

Equations

• Minimalism.isCompIn events x y = ∃ (e : Minimalism.MergeEvent), e ∈ events ∧ e.daughter = x ∧ e.target = y ∧ e.mtype = Minimalism.MergeType.extComp

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

X moved to the specifier of Y via internal merge.

Equations

• Minimalism.movedToSpecOf events x y = ∃ (e : Minimalism.MergeEvent), e ∈ events ∧ e.daughter = x ∧ e.target = y ∧ e.mtype = Minimalism.MergeType.intSpec

def Minimalism.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 positional restatement of Phase.antiLocality.

Equations

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

def Minimalism.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

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

structure Minimalism.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 Minimalism.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

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

def Minimalism.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

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

theorem Minimalism.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 Minimalism.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

• Minimalism.extractionRestriction pf extractee = Minimalism.isStranded pf extractee

structure Minimalism.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 Minimalism.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 Minimalism.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 Minimalism.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 Minimalism.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 Minimalism.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 Minimalism.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 : Minimalism.CyclicPosition) => x.agreeResult.isSome) chain.positions).length

def Minimalism.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 : Minimalism.CyclicPosition) => x.agreeResult) chain.positions