Fox and Pesetsky (2005): Cyclic Linearization of Syntactic Structure

This file formalizes [fox-pesetsky-2005]'s account of successive cyclicity and Holmberg's Generalization. Spell-out linearizes each domain as the derivation builds it, its ordering statements are never deleted, and a derivation converges only if they cohere (Minimalist.Linearization.Consistent). The paper's derivational scenarios are theorems over arbitrary terminals: movement from the left edge of a domain converges (scenario1), movement from a non-edge position crashes on the pair it reorders (scenario2), and moving the edge material along restores the order (scenario3). Object Shift in Swedish is these scenarios with the verb, the object and an intervener as the terminals: it converges only when the verb, and any other VP-internal material preceding the object, leaves VP as well (objectShift_verbToC, objectShift_embedded, objectShift_intervener, objectShift_intervener_fronted), and rows_predicted computes convergence for the paper's Swedish sentences from their configurations.

Implementation notes

Spell-out domains are lists of terminals and a derivation is its list of snapshots, so the scenarios quantify over any type of labels; the consistent cases need the final snapshot to be duplicate-free. The Swedish rows record the paper's analysis of each sentence, whether the verb moves to C, whether an auxiliary occupies C instead, whether a first object or particle precedes the object in VP, and whether that intervener fronts through the VP edge, and Config.phases builds the VP and CP snapshots of the paper's sketches from them.

References

• [fox-pesetsky-2005]
• [chomsky-2000]
• [chomsky-2001]

Derivational scenarios

theorem FoxPesetsky2005.scenario1 {α : Type u_1} {X Y Z a : α} [DecidableEq α] (hnd : [X, a, Y, Z].Nodup) : Minimalist.Linearization.Consistent [[X, Y, Z], [X, a, Y, Z]]

Scenario 1: leftward movement from the left edge of a domain converges.

theorem FoxPesetsky2005.scenario2 {α : Type u_1} {X Y Z a : α} : ¬Minimalist.Linearization.Consistent [[X, Y, Z], [Y, a, X, Z]]

Scenario 2: leftward movement from a non-edge position reorders the moved element and the edge, and the derivation crashes whatever else it contains.

theorem FoxPesetsky2005.scenario3 {α : Type u_1} {X Y Z a : α} [DecidableEq α] (hnd : [X, Y, a, Z].Nodup) : Minimalist.Linearization.Consistent [[X, Y, Z], [X, Y, a, Z]]

Scenario 3: moving the edge material along with the non-edge element preserves their order, so the derivation converges.

theorem FoxPesetsky2005.cycle {α : Type u_1} {a b c : α} : ¬Minimalist.Linearization.Consistent [[a, b], [b, c], [c, a]]

An ordering cycle through several Spell-outs crashes as well: the crash condition is the acyclicity of the accumulated order, not a directly contradicted pair.

Holmberg's Generalization

theorem FoxPesetsky2005.objectShift_verbToC {α : Type u_1} {S V O adv : α} [DecidableEq α] (hnd : [S, V, O, adv].Nodup) : Minimalist.Linearization.Consistent [[V, O], [S, V, O, adv]]

Object Shift with the verb in C: VP orders the verb before the object and CP keeps it so.

theorem FoxPesetsky2005.objectShift_embedded {α : Type u_1} {S V O adv C : α} : ¬Minimalist.Linearization.Consistent [[V, O], [C, S, O, adv, V]]

Object Shift in an embedded clause, where the verb stays in VP: the shifted object precedes the verb at CP against VP, and the derivation crashes.

theorem FoxPesetsky2005.objectShift_aux {α : Type u_1} {S V O adv aux : α} : ¬Minimalist.Linearization.Consistent [[V, O], [S, aux, O, adv, V]]

Object Shift under an auxiliary in C: the same contradiction.

theorem FoxPesetsky2005.objectShift_intervener {α : Type u_1} {S V O adv XP : α} : ¬Minimalist.Linearization.Consistent [[V, XP, O], [S, V, O, adv, XP]]

Any VP-internal material preceding the object blocks Object Shift, verb movement or not: the intervener precedes the object at VP and follows it at CP.

theorem FoxPesetsky2005.objectShift_intervener_fronted {α : Type u_1} {S V O adv XP : α} [DecidableEq α] (hnd : [XP, V, S, O, adv].Nodup) : Minimalist.Linearization.Consistent [[XP, V, O], [XP, V, S, O, adv]]

An intervener that fronts through the VP edge no longer blocks Object Shift: the order established at VP is the order at CP.

The Swedish data

inductive FoxPesetsky2005.Label : Type

The terminals of the paper's Object Shift sketches.

• S : Label
• V : Label
• O : Label
• adv : Label
• C : Label
• aux : Label
• XP : Label

@[instance_reducible]

instance FoxPesetsky2005.instDecidableEqLabel : DecidableEq Label

Equations

• FoxPesetsky2005.instDecidableEqLabel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def FoxPesetsky2005.instReprLabel.repr : Label → ℕ → Std.Format

Equations

• FoxPesetsky2005.instReprLabel.repr FoxPesetsky2005.Label.S prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "FoxPesetsky2005.Label.S")).group prec✝
• FoxPesetsky2005.instReprLabel.repr FoxPesetsky2005.Label.V prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "FoxPesetsky2005.Label.V")).group prec✝
• FoxPesetsky2005.instReprLabel.repr FoxPesetsky2005.Label.O prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "FoxPesetsky2005.Label.O")).group prec✝
• FoxPesetsky2005.instReprLabel.repr FoxPesetsky2005.Label.adv prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "FoxPesetsky2005.Label.adv")).group prec✝
• FoxPesetsky2005.instReprLabel.repr FoxPesetsky2005.Label.C prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "FoxPesetsky2005.Label.C")).group prec✝
• FoxPesetsky2005.instReprLabel.repr FoxPesetsky2005.Label.aux prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "FoxPesetsky2005.Label.aux")).group prec✝
• FoxPesetsky2005.instReprLabel.repr FoxPesetsky2005.Label.XP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "FoxPesetsky2005.Label.XP")).group prec✝

@[instance_reducible]

instance FoxPesetsky2005.instReprLabel : Repr Label

Equations

• FoxPesetsky2005.instReprLabel = { reprPrec := FoxPesetsky2005.instReprLabel.repr }

structure FoxPesetsky2005.Config : Type

The paper's analysis of an Object Shift sentence: whether the finite verb moves to C, whether an auxiliary occupies C instead, whether a first object or particle precedes the object in VP, and whether that intervener fronts through the VP edge.

• verbToC : Bool
• aux : Bool
• intervener : Bool
• intervenerMoved : Bool

@[instance_reducible]

instance FoxPesetsky2005.instDecidableEqConfig : DecidableEq Config

Equations

• FoxPesetsky2005.instDecidableEqConfig = FoxPesetsky2005.instDecidableEqConfig.decEq

def FoxPesetsky2005.instDecidableEqConfig.decEq (x✝ x✝¹ : Config) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance FoxPesetsky2005.instReprConfig : Repr Config

Equations

• FoxPesetsky2005.instReprConfig = { reprPrec := FoxPesetsky2005.instReprConfig.repr }

def FoxPesetsky2005.instReprConfig.repr : Config → ℕ → Std.Format

Equations

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

def FoxPesetsky2005.Config.vp (c : Config) : List Label

The VP snapshot: an intervener that will front has first moved to the VP edge.

Equations

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

def FoxPesetsky2005.Config.cp (c : Config) : List Label

The CP snapshot after Object Shift.

Equations

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

def FoxPesetsky2005.Config.phases (c : Config) : List (List Label)

The derivation's snapshots.

Equations

• c.phases = [c.vp, c.cp]

structure FoxPesetsky2005.Row : Type

• config : Config
• judgment : Features.Judgment

def FoxPesetsky2005.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

• FoxPesetsky2005.instDecidableEqRow.decEq { config := a, judgment := a_1 } { config := b, judgment := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance FoxPesetsky2005.instDecidableEqRow : DecidableEq Row

Equations

• FoxPesetsky2005.instDecidableEqRow = FoxPesetsky2005.instDecidableEqRow.decEq

def FoxPesetsky2005.yesNoTable : List (String × Bool)

Equations

• FoxPesetsky2005.yesNoTable = [("yes", true), ("no", false)]

def FoxPesetsky2005.Row.ofExample (ex : Data.Examples.LinguisticExample) : Option Row

Equations

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

def FoxPesetsky2005.rows : List Row

Equations

• FoxPesetsky2005.rows = List.filterMap FoxPesetsky2005.Row.ofExample FoxPesetsky2005.Examples.all

theorem FoxPesetsky2005.rows_predicted (r : Row) : r ∈ rows → (r.judgment = Features.Judgment.acceptable ↔ Minimalist.Linearization.Consistent r.config.phases)

The paper's Swedish sentences are acceptable exactly when their derivations linearize.