Docs / Syntax / Minimalist / Linearization / Cyclic

Cyclic linearization of syntactic structure

import Linglib.Syntax.Minimalist.Linearization.Cyclic · namespace Minimalist.Linearization

Fox & Pesetsky 2005's theory of the syntax–phonology interface: Spell-out linearizes each Spell-out domain as the derivation builds it, the ordering statements it establishes are never deleted (Order Preservation, (52)), and a derivation converges only if the accumulated statements cohere.

A derivation is its list of phase snapshots. A snapshot contributes the ordering statements a < b between its terminals, the pair-sublist relation [a, b] <+ p (Statement), and SpelloutOrder is the transitive closure of their union. Convergence (Consistent) is irreflexivity of this candidate order, so the crash condition is exactly that Spell-out induces a strict order (consistent_iff_isStrictOrder), equivalently that some duplicate-free string has every snapshot as a sub-order (consistent_iff_exists_linearization): the derivation has a PF string. Order Preservation is monotonicity (SpelloutOrder.mono), not an axiom; it keeps adjacency too, since whatever a later Spell-out places between two terminals adjacent at an earlier one was not spelled out with them (Consistent.notMem_of_isInfix); the order reads only the set of snapshots (spelloutOrder_perm); two Spell-outs, the later containing the earlier, cohere exactly when the earlier is a sub-order of the later (consistent_pair_iff_sublist); and Consistent decides on concrete data.

Main results

Minimalist.Linearization.consistent_iff_isStrictOrder: the crash condition is that Spell-out induces a strict order.
Minimalist.Linearization.consistent_iff_exists_linearization: a derivation converges exactly when a duplicate-free string extends every Spell-out.

References

Fox & Pesetsky 2005, Cyclic Linearization of Syntactic Structure formalized

Declarations

An ordering statement a < b is established when the pair [a, b] is a sub-order of some phase snapshot (Fox & Pesetsky 2005 (10), (52)).

def Statement L54–56

{α : Type u_1} (phases : List (List α)) (a b : α) :

Prop

Statement phases a b = ∃ p ∈ phases, [a, b].Sublist p

Used by SpelloutOrder, Statement.spelloutOrder, not_consistent_of_pair, Statement.left_mem_support, Statement.right_mem_support, instDecidableStatement, instDecidableReflTransGenStatement

The candidate order induced by a derivation is the transitive closure of its ordering statements.

def SpelloutOrder L58–61

{α : Type u_1} (phases : List (List α)) :

α → α → Prop

SpelloutOrder phases = Relation.TransGen (Statement phases)

Built from

Used by Consistent, Statement.spelloutOrder, consistent_iff_isStrictOrder, SpelloutOrder.mono, spelloutOrder_perm, spelloutOrder_singleton_idxOf, instDecidableSpelloutOrder, instDecidableConsistent

A derivation linearizes when its candidate order is irreflexive, so that, transitivity being free, it is a strict order with no ordering cycle of any length (Fox & Pesetsky 2005's convergence condition).

def Consistent L63–66

{α : Type u_1} (phases : List (List α)) :

Prop

Consistent phases = ∀ (a : α), ¬SpelloutOrder phases a a

Built from

Used by consistent_iff_isStrictOrder, not_consistent_of_pair, Consistent.nodup, Consistent.notMem_of_isInfix, consistent_singleton, consistent_of_forall_sublist, consistent_pair_iff_sublist, consistent_iff_exists_linearization, instDecidableConsistent

Used in Syntax/Minimalist/Linearization/SpelloutDomain, ErlewineSommerlot2025, FoxPesetsky2005, SandeClemDabkowski2026

L68

The crash condition, in order-theoretic vocabulary.

theorem consistent_iff_isStrictOrder L70–74

{α : Type u_1} {phases : List (List α)} :

Consistent phases ↔ IsStrictOrder α (SpelloutOrder phases)

Built from ,

By Order Preservation ((52)) ordering statements are never deleted, so a larger derivation induces a larger order.

theorem SpelloutOrder.mono L76–80

{α : Type u_1} {ps qs : List (List α)} {a b : α} (h : ∀ p ∈ ps, p ∈ qs) (hab : SpelloutOrder ps a b) :

SpelloutOrder qs a b

Built from

theorem spelloutOrder_perm L82–84

{α : Type u_1} {ps qs : List (List α)} (h : ps.Perm qs) :

SpelloutOrder ps = SpelloutOrder qs

Built from

L86–88

L90–91

theorem Consistent.notMem_of_isInfix L93–105

{α : Type u_1} {phases : List (List α)} {p q : List α} {a b c : α} (h : Consistent phases) (hp : p ∈ phases) (hq : q ∈ phases) (hab : [a, b] <:+: p) (hac : [a, c].Sublist q) (hcb : [c, b].Sublist q) :

c ∉ p

Built from

L109–119

L121–122

L124–128

theorem consistent_pair_iff_sublist L130–137

{α : Type u_1} {p q : List α} [DecidableEq α] (hq : q.Nodup) (hpq : p ⊆ q) :

Consistent [p, q] ↔ p.Sublist q

Built from

L139–140

L142–144

L146–148

Convergence is the existence of a PF string: a duplicate-free order of the terminals of which every Spell-out is a sub-order. One direction is consistent_of_forall_sublist; the other extends the candidate order to a linear order (Szpilrajn) and sorts the support by it.

theorem consistent_iff_exists_linearization L150–172

{α : Type u_1} {phases : List (List α)} [DecidableEq α] :

Consistent phases ↔ ∃ (l : List α), l.Nodup ∧ ∀ p ∈ phases, p.Sublist l

Built from

Decidability

The candidate order's generator only relates terminals in the support, so irreflexivity reduces to a finite check over the support, with reachability decided by Relation.ReflTransGen.decidable_of_finite.