Documentation

Linglib.Syntax.Minimalist.Linearization.Cyclic

Cyclic linearization of syntactic structure #

[FP05]'s theory of the syntax–phonology interface: linearization applies at the end of each phase (Spell-out domain), the ordering statements it establishes are never deleted (Order Preservation, their (52)), and a derivation converges only if the accumulated statements cohere.

The account is one mathematical object: a derivation exposes a word of phase snapshots, each snapshot carries its pair-sublist relation ([a, b] <+ p — the paper's ordering statements, their (10)), and spelloutOrder is the transitive closure of their union. Grammaticality (Consistent) is the statement that this candidate is a genuine strict order (consistent_iff_isStrictOrder); transitivity is free, so the entire crash condition is irreflexivity. Order Preservation is monotonicity (spelloutOrder_mono), not an axiom, and the order is blind to the sequencing of Spell-outs (spelloutOrder_perm) — the account reads only the set of snapshots.

The paper's worked examples (Scenarios (13)/(14), successive-cyclic movement (3)–(8), Holmberg's Generalization §3) live in Studies/FoxPesetsky2005.lean; Malayic and Guébie applications in Studies/ErlewineSommerlot2025.lean and Studies/SandeClemDabkowski2026.lean.

Main declarations #

Main results #

source
def Minimalist.Linearization.spelloutOrder {α : Type u_1} (phases : List (List α)) :
α → α → Prop

The spell-out order induced by a derivation's phase snapshots: the transitive closure of "a precedes b at some Spell-out", per-phase precedence being the pair-sublist relation ([FP05] (10), (52)).

Equations
Instances For
    source
    def Minimalist.Linearization.Consistent {α : Type u_1} (phases : List (List α)) :
    Prop

    The derivation linearizes: spell-out induces a genuine strict order ([FP05]'s convergence condition). Transitivity is free, so the content is irreflexivity — no ordering cycle of any length.

    Equations
    Instances For
      source
      theorem Minimalist.Linearization.consistent_iff_isStrictOrder {α : Type u_1} {phases : List (List α)} :
      Consistent phases ↔ IsStrictOrder α (spelloutOrder phases)

      The crash condition, in order-theoretic vocabulary.

      source
      theorem Minimalist.Linearization.spelloutOrder_mono {α : Type u_1} {ps qs : List (List α)} {a b : α} (h : ∀ p ∈ ps, p ∈ qs) (hab : spelloutOrder ps a b) :
      spelloutOrder qs a b

      Order Preservation ([FP05] (52)): ordering statements are never deleted — a larger derivation induces a larger order.

      source
      theorem Minimalist.Linearization.spelloutOrder_perm {α : Type u_1} {ps qs : List (List α)} (h : ps.Perm qs) :
      spelloutOrder ps = spelloutOrder qs

      The induced order is blind to the sequencing of Spell-outs: it reads only the set of phase snapshots.

      source
      theorem Minimalist.Linearization.spelloutOrder_singleton_idxOf {α : Type u_1} {a b : α} [DecidableEq α] {p : List α} (hnd : p.Nodup) (h : spelloutOrder [p] a b) :
      List.idxOf a p < List.idxOf b p

      On a single duplicate-free snapshot, the induced order is index order.

      source
      theorem Minimalist.Linearization.consistent_singleton {α : Type u_1} [DecidableEq α] {p : List α} (hnd : p.Nodup) :
      Consistent [p]

      A single Spell-out of distinct terminals always linearizes.

      Decidability #

      Consistent decides on concrete phase data: the candidate order's generator only relates terminals mentioned at some Spell-out, so irreflexivity reduces to a finite check over the support, with reachability decided by Relation.ReflTransGen.decidable_of_finite.

      source
      def Minimalist.Linearization.support {α : Type u_1} [DecidableEq α] (phases : List (List α)) :
      List α

      Every terminal mentioned at any Spell-out.

      Equations
      Instances For
        source
        @[implicit_reducible]
        instance Minimalist.Linearization.instDecidableReflTransGen {α : Type u_1} [DecidableEq α] (phases : List (List α)) (a b : α) :
        Decidable (Relation.ReflTransGen (fun (a b : α) => ∃ p ∈ phases, [a, b].Sublist p) a b)
        Equations
        source
        @[implicit_reducible]
        instance Minimalist.Linearization.instDecidableSpelloutOrder {α : Type u_1} [DecidableEq α] (phases : List (List α)) (a b : α) :
        Decidable (spelloutOrder phases a b)
        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[implicit_reducible]
        instance Minimalist.Linearization.instDecidableConsistent {α : Type u_1} [DecidableEq α] (phases : List (List α)) :
        Decidable (Consistent phases)
        Equations