Spell-out domains of a derivation

A Spell-out domain in the sense of [FP05] is a constituent the derivation has built, linearized when Spell-out applies to it. On a derivation the constituent built by the first m steps is the ordered object of that stage, and at a later stage n it stands inside the larger object with whatever has moved out of it in between replaced by traces (Derivation.spelloutDomain). Its Spell-out at n is its pronounced yield (Derivation.spellout), so the Spell-out snapshots that cyclic linearization reads (Linearization/Cyclic.lean) come from the derivation itself, and a derivation linearizes under a schedule of Spell-outs when those snapshots cohere (Derivation.Linearizes).

Fox and Pesetsky spell a domain out when it is built, which reads the surface of its stage (Derivation.spellout_self); spelling a phase out when the next phase head merges, as Chomsky proposes, takes the stage after that merge (Derivation.mergeStage?). Which constituent a study spells out, the whole phase or the head with its complement, is the stage it names. A head moved into a phase head by Internal Merge stays inside the constituent the two build, so the moved verb of a verb-plus-v head is spelled out with v.

Main definitions

• Minimalist.Derivation.spelloutDomain, Derivation.spellout: a domain at a later stage, and its Spell-out.
• Minimalist.Derivation.Linearizes: a derivation linearizes under a schedule.

Main statements

• Minimalist.Derivation.spellout_self: a domain spelled out when it is built reads the surface of its stage.
• Minimalist.Derivation.spellout_append_of_le: extending a derivation changes no earlier Spell-out.

References

• [FP05]
• [Cho01]

def Minimalist.Step.applyInside (step : Step) (D : PlanarSyntacticObject) : PlanarSyntacticObject

Inside a constituent built earlier, External Merge and merging back do nothing, and Internal Merge and extraction replace the mover by its trace, unless the constituent is itself the mover, which then moves intact.

Equations

• (Minimalist.Step.em side item).applyInside D = D
• (Minimalist.Step.remerge side).applyInside D = D
• (Minimalist.Step.im mover side).applyInside D = if ↑D = mover then D else Minimalist.PlanarSyntacticObject.replaceWhere mover mover.tracePlanar D
• (Minimalist.Step.extract mover).applyInside D = if ↑D = mover then D else Minimalist.PlanarSyntacticObject.replaceWhere mover mover.tracePlanar D

def Minimalist.Derivation.stage? (d : Derivation) (n : ℕ) : Option PlanarSyntacticObject

d.stage? n is the ordered object after the first n steps, if the replay succeeds.

Equations

• d.stage? n = (d.take n).externalize?

def Minimalist.Derivation.spelloutDomain (d : Derivation) (m n : ℕ) : Option PlanarSyntacticObject

The constituent built by the first m steps stands at stage n with the movers of the steps in between replaced by their traces.

Equations

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

def Minimalist.Derivation.spellout (d : Derivation) (m n : ℕ) : List LexicalItem.Token

The Spell-out at stage n of the domain built by stage m is its pronounced yield.

Equations

• d.spellout m n = (Option.map (fun (x : Minimalist.PlanarSyntacticObject) => Minimalist.planarYield ↑x) (d.spelloutDomain m n)).getD []

def Minimalist.Derivation.mergeStage? (d : Derivation) (item : SyntacticObject) : Option ℕ

d.mergeStage? item is the stage right after item is externally merged, if it is.

Equations

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

def Minimalist.Derivation.Linearizes (d : Derivation) (sched : List (ℕ × ℕ)) : Prop

A derivation linearizes under a schedule of Spell-outs, each the stage at which a domain is built and the stage at which it is spelled out, when their snapshots cohere.

Equations

• d.Linearizes sched = Minimalist.Linearization.Consistent (List.map (fun (p : ℕ × ℕ) => d.spellout p.1 p.2) sched)

@[instance_reducible]

instance Minimalist.Derivation.instDecidableLinearizes (d : Derivation) (sched : List (ℕ × ℕ)) : Decidable (d.Linearizes sched)

Equations

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

@[simp]

theorem Minimalist.Derivation.spelloutDomain_self {d : Derivation} {m : ℕ} : d.spelloutDomain m m = d.stage? m

theorem Minimalist.Derivation.spellout_self {d : Derivation} {m : ℕ} : d.spellout m m = (d.take m).surfaceTokens

A domain spelled out when it is built reads the surface of its stage.

theorem Minimalist.Derivation.stage?_append_of_le {d : Derivation} {n : ℕ} {steps : List Step} (h : n ≤ d.length) : (d.append steps).stage? n = d.stage? n

theorem Minimalist.Derivation.spelloutDomain_append_of_le {d : Derivation} {m n : ℕ} {steps : List Step} (hmn : m ≤ n) (h : n ≤ d.length) : (d.append steps).spelloutDomain m n = d.spelloutDomain m n

theorem Minimalist.Derivation.spellout_append_of_le {d : Derivation} {m n : ℕ} {steps : List Step} (hmn : m ≤ n) (h : n ≤ d.length) : (d.append steps).spellout m n = d.spellout m n

Extending a derivation changes no earlier Spell-out.

theorem Minimalist.Derivation.Linearizes.nodup {d : Derivation} {sched : List (ℕ × ℕ)} (h : d.Linearizes sched) {p : ℕ × ℕ} (hp : p ∈ sched) : (d.spellout p.1 p.2).Nodup

A linearizing derivation spells no domain out with a repeated token.