Chains, sharing and PF reduction on planar syntactic objects

A planar syntactic object whose traces remember the token that moved carries the two ways one token comes to occupy several positions. Internal Merge leaves a trace, the cancellation T/T_v of [marcolli-chomsky-berwick-2025] with T_v remembered, so a token's chain is its occurrence with its traces, and a trace no occurrence of its token c-commands is unbound: seen from its own conjunct, a copy without its antecedent. A token occurring twice is shared, dominated by two mothers — [citko-2005]'s Parallel Merge, which MCB §1.1.3.2 places outside Merge as a grafting away from the root — and a shared constituent is an identical subtree at two positions. At PF a token is pronounced once, at its last occurrence, so shared material follows all unshared material ([wilder-1999], [de-vries-2009]). An [E] feature on a head silences the head's complement ([merchant-2001]), and since a shared token is one token, eliding either of its occurrences silences it everywhere. An [E] head applies once per distinct complement, and an application that silences no pronounceable token an earlier one had not already silenced is vacuous, the configuration [citko-gracanin-yuksek-2025]'s Pronunciation Economy bans. A v or C projection whose edge hosts several wh-specifiers, wh-tokens or their traces, receives the asterisk of the multiple-wh-fronting parameter and crashes at PF unless its head is silenced. The cost of the object is read off its terms, the distinct subtrees as MCB's subtrees taken each once: the lexical leaves are the items drawn and the internal vertices the Merges, so a shared constituent is built once.

Main definitions

• tokenList, occurrences, unboundTraces, IsShared: occurrences and chains.
• terms: the distinct subtrees, a shared constituent's once.
• elidedDomains, IsSilenced, pfPhon: pronunciation under [E].
• IsVacuous, PronunciationEconomy: the ban on vacuous ellipsis.
• projection, phaseAt, IsAsterisked, Converges: the multiple-wh-fronting asterisk.
• planarCost: the object's DerivationCost.

References

• [M. Marcolli, N. Chomsky and R. C. Berwick, Mathematical Structure of Syntactic Merge (2025)][marcolli-chomsky-berwick-2025]
• [B. Citko, On the nature of Merge (2005)][citko-2005]
• [C. Wilder, Right node raising and the LCA (1999)][wilder-1999]
• [M. de Vries, On multidominance and linearization (2009)][de-vries-2009]
• [J. Merchant, The Syntax of Silence (2001)][merchant-2001]
• [B. Citko and M. Gračanin-Yuksek, Economy in PF reduction (2025)][citko-gracanin-yuksek-2025]

Occurrences and chains

def Minimalist.positions (f : SyntacticObject.Vertex → Option LIToken) : RoseTree SyntacticObject.Vertex → List (RoseTree.Pathed.Path × LIToken)

The positions whose label f accepts, with their paths, left to right.

Equations

• Minimalist.positions f (RoseTree.node a cs) = match f a with | some tok => [([], tok)] | none => Minimalist.positionsAux f 0 cs

def Minimalist.positionsAux (f : SyntacticObject.Vertex → Option LIToken) : ℕ → List (RoseTree SyntacticObject.Vertex) → List (RoseTree.Pathed.Path × LIToken)

Auxiliary: the positions in a children list from index i.

Equations

• Minimalist.positionsAux f x✝ [] = []
• Minimalist.positionsAux f x✝ (c :: cs) = List.map (fun (x : RoseTree.Pathed.Path × Minimalist.LIToken) => (x✝ :: x.1, x.2)) (Minimalist.positions f c) ++ Minimalist.positionsAux f (x✝ + 1) cs

def Minimalist.tokenList : RoseTree SyntacticObject.Vertex → List (RoseTree.Pathed.Path × LIToken)

The tokens with their paths, left to right.

Equations

• Minimalist.tokenList = Minimalist.positions (Sum.elim some fun (x : Option Minimalist.LIToken) => none)

def Minimalist.traceList : RoseTree SyntacticObject.Vertex → List (RoseTree.Pathed.Path × LIToken)

The traces with their paths, left to right.

Equations

• Minimalist.traceList = Minimalist.positions (Sum.elim (fun (x : Minimalist.LIToken) => none) id)

def Minimalist.occurrences (t : PlanarSyntacticObject) (tok : LIToken) : List RoseTree.Pathed.Path

The occurrences of tok.

Equations

• Minimalist.occurrences t tok = List.filterMap (fun (x : RoseTree.Pathed.Path × Minimalist.LIToken) => if x.2 = tok then some x.1 else none) (Minimalist.tokenList ↑t)

def Minimalist.tokens (t : PlanarSyntacticObject) : Finset LIToken

The tokens of t, each once.

Equations

• Minimalist.tokens t = (List.map (fun (x : RoseTree.Pathed.Path × Minimalist.LIToken) => x.2) (Minimalist.tokenList ↑t)).toFinset

def Minimalist.terms (t : PlanarSyntacticObject) : Finset (RoseTree SyntacticObject.Vertex)

The terms of t: its subtrees, a shared constituent's once.

Equations

• Minimalist.terms t = (List.filterMap (↑t).subtreeAt (RoseTree.Pathed.vertices ↑t)).toFinset

def Minimalist.IsShared (t : PlanarSyntacticObject) (tok : LIToken) : Prop

tok is shared, dominated by two mothers: it occurs twice.

Equations

• Minimalist.IsShared t tok = (2 ≤ (Minimalist.occurrences t tok).length)

@[instance_reducible]

instance Minimalist.instDecidableIsShared (t : PlanarSyntacticObject) (tok : LIToken) : Decidable (IsShared t tok)

Equations

• Minimalist.instDecidableIsShared t tok = Minimalist.instDecidableIsShared._aux_1 t tok

def Minimalist.CCommands (p q : RoseTree.Pathed.Path) : Prop

p c-commands q: the mother of p dominates q while p does not.

Equations

• Minimalist.CCommands p q = (List.dropLast p <+: q ∧ ¬p <+: q)

@[instance_reducible]

instance Minimalist.instDecidableCCommands (p q : RoseTree.Pathed.Path) : Decidable (CCommands p q)

Equations

• Minimalist.instDecidableCCommands p q = Minimalist.instDecidableCCommands._aux_1 p q

def Minimalist.IsBound (t : PlanarSyntacticObject) (x : RoseTree.Pathed.Path × LIToken) : Prop

The trace x is bound: an occurrence of its token c-commands it.

Equations

• Minimalist.IsBound t x = ∃ q ∈ Minimalist.occurrences t x.2, Minimalist.CCommands q x.1

@[instance_reducible]

instance Minimalist.instDecidableIsBound (t : PlanarSyntacticObject) (x : RoseTree.Pathed.Path × LIToken) : Decidable (IsBound t x)

Equations

• Minimalist.instDecidableIsBound t x = Minimalist.instDecidableIsBound._aux_1 t x

def Minimalist.unboundTraces (t : PlanarSyntacticObject) : List (RoseTree.Pathed.Path × LIToken)

The unbound traces: seen from their positions, copies without their antecedents.

Equations

• Minimalist.unboundTraces t = List.filter (fun (x : RoseTree.Pathed.Path × Minimalist.LIToken) => decide ¬Minimalist.IsBound t x) (Minimalist.traceList ↑t)

def Minimalist.pronouncedAt (t : PlanarSyntacticObject) (tok : LIToken) : Option RoseTree.Pathed.Path

The occurrence at which tok is pronounced: its last.

Equations

• Minimalist.pronouncedAt t tok = (Minimalist.occurrences t tok).getLast?

Ellipsis

def Minimalist.complementPath (p : RoseTree.Pathed.Path) : RoseTree.Pathed.Path

The complement of the head at p: its sister.

Equations

• Minimalist.complementPath p = List.dropLast p ++ [1 - List.getLastD p 0]

def Minimalist.eHeads (t : PlanarSyntacticObject) : List RoseTree.Pathed.Path

The [E] heads.

Equations

• Minimalist.eHeads t = List.filterMap (fun (x : RoseTree.Pathed.Path × Minimalist.LIToken) => if x.2.item.outerEllipsis = true then some x.1 else none) (Minimalist.tokenList ↑t)

def Minimalist.elidedDomains (t : PlanarSyntacticObject) : List RoseTree.Pathed.Path

The elided domains, one per distinct complement of an [E] head, in the order of the heads: a shared head over one shared complement applies once, over two complements twice.

Equations

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

def Minimalist.IsSilenced (t : PlanarSyntacticObject) (tok : LIToken) : Prop

tok is silenced: one of its occurrences lies in an elided domain.

Equations

• Minimalist.IsSilenced t tok = ∃ K ∈ Minimalist.elidedDomains t, ∃ p ∈ Minimalist.occurrences t tok, K <+: p

@[instance_reducible]

instance Minimalist.instDecidableIsSilenced (t : PlanarSyntacticObject) (tok : LIToken) : Decidable (IsSilenced t tok)

Equations

• Minimalist.instDecidableIsSilenced t tok = Minimalist.instDecidableIsSilenced._aux_1 t tok

def Minimalist.pfYield (t : PlanarSyntacticObject) : List LIToken

The pronounced tokens, left to right: each at its last occurrence, unless silenced.

Equations

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

def Minimalist.pfPhon (t : PlanarSyntacticObject) : List String

The pronounced forms, left to right.

Equations

• Minimalist.pfPhon t = List.filterMap Minimalist.LIToken.phonForm? (Minimalist.pfYield t)

def Minimalist.silencedBy (t : PlanarSyntacticObject) (K : RoseTree.Pathed.Path) : Finset LIToken

The pronounceable tokens the application at the domain K silences.

Equations

• Minimalist.silencedBy t K = {s ∈ Minimalist.tokens t | s.phonForm?.isSome = true ∧ ((Minimalist.occurrences t s).any fun (x : RoseTree.Pathed.Path) => decide (K <+: x)) = true}

def Minimalist.IsVacuous (t : PlanarSyntacticObject) (K : RoseTree.Pathed.Path) : Prop

The application at K has no effect on pronunciation: the earlier applications silenced every token it silences.

Equations

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

@[instance_reducible]

instance Minimalist.instDecidableIsVacuous (t : PlanarSyntacticObject) (K : RoseTree.Pathed.Path) : Decidable (IsVacuous t K)

Equations

• Minimalist.instDecidableIsVacuous t K = id inferInstance

def Minimalist.PronunciationEconomy (t : PlanarSyntacticObject) : Prop

Pronunciation Economy ([citko-gracanin-yuksek-2025] (39)): no application of ellipsis is vacuous.

Equations

• Minimalist.PronunciationEconomy t = ∀ K ∈ Minimalist.elidedDomains t, ¬Minimalist.IsVacuous t K

@[instance_reducible]

instance Minimalist.instDecidablePronunciationEconomy (t : PlanarSyntacticObject) : Decidable (PronunciationEconomy t)

Equations

• Minimalist.instDecidablePronunciationEconomy t = Minimalist.instDecidablePronunciationEconomy._aux_1 t

Phase edges and the multiple-wh-fronting asterisk

def Minimalist.projection (c : Cat) : RoseTree SyntacticObject.Vertex → Option (List (RoseTree SyntacticObject.Vertex) × LIToken)

The specifiers and head of the projection of a head of category c: down the right spine, the left daughters above the head, which is the first selecting item met; none when that item has another category or the spine ends first.

Equations

• One or more equations did not get rendered due to their size.
• Minimalist.projection c x✝ = none

def Minimalist.headToken? : RoseTree SyntacticObject.Vertex → Option LIToken

The head of a constituent: the token or trace at a leaf, else the first selecting item down the right spine.

Equations

• Minimalist.headToken? (RoseTree.node (Sum.inl tok) children) = some tok
• Minimalist.headToken? (RoseTree.node (Sum.inr (some tok)) children) = some tok
• Minimalist.headToken? (RoseTree.node (Sum.inr none) [RoseTree.node (Sum.inl tok) [], r]) = if tok.item.outerSel = [] then Minimalist.headToken? r else some tok
• Minimalist.headToken? (RoseTree.node (Sum.inr none) [head, r]) = Minimalist.headToken? r
• Minimalist.headToken? (RoseTree.node (Sum.inr none) children) = none

def Minimalist.IsWhSpecifier (s : RoseTree SyntacticObject.Vertex) : Prop

The constituent is a wh-specifier: its head is a wh-token or its trace.

Equations

• Minimalist.IsWhSpecifier s = ∃ tok ∈ (Minimalist.headToken? s).toList, tok.item.outerWh = true

@[instance_reducible]

instance Minimalist.instDecidableIsWhSpecifier (s : RoseTree SyntacticObject.Vertex) : Decidable (IsWhSpecifier s)

Equations

• Minimalist.instDecidableIsWhSpecifier s = Minimalist.instDecidableIsWhSpecifier._aux_1 s

def Minimalist.phaseAt (t : PlanarSyntacticObject) (p : RoseTree.Pathed.Path) : Option (Syntax.Question.PhaseEdge × List (RoseTree SyntacticObject.Vertex) × LIToken)

The phase at p, a v or C projection: its edge, specifiers and head.

Equations

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

def Minimalist.IsAsterisked (t : PlanarSyntacticObject) (param : Syntax.Question.MWFParameter) (p : RoseTree.Pathed.Path) : Prop

The phase at p receives the asterisk of the parameter ([citko-gracanin-yuksek-2025] (27)): its edge hosts more wh-specifiers than the parameter allows there.

Equations

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

@[instance_reducible]

instance Minimalist.instDecidableIsAsterisked (t : PlanarSyntacticObject) (param : Syntax.Question.MWFParameter) (p : RoseTree.Pathed.Path) : Decidable (IsAsterisked t param p)

Equations

• Minimalist.instDecidableIsAsterisked t param p = Minimalist.instDecidableIsAsterisked._aux_1 t param p

def Minimalist.Converges (t : PlanarSyntacticObject) (param : Syntax.Question.MWFParameter) : Prop

The object converges at PF: the head of every asterisked phase is silenced.

Equations

• Minimalist.Converges t param = ∀ p ∈ RoseTree.Pathed.vertices ↑t, Minimalist.IsAsterisked t param p → ∀ x ∈ (Minimalist.phaseAt t p).toList, Minimalist.IsSilenced t x.2.2

@[instance_reducible]

instance Minimalist.instDecidableConverges (t : PlanarSyntacticObject) (param : Syntax.Question.MWFParameter) : Decidable (Converges t param)

Equations

• Minimalist.instDecidableConverges t param = Minimalist.instDecidableConverges._aux_1 t param

Cost

def Minimalist.planarCost (t : PlanarSyntacticObject) : DerivationCost

The cost of the object: its tokens are the lexical items drawn, its internal terms the Merges, and its elided domains the applications of ellipsis.

Equations

• Minimalist.planarCost t Minimalist.CostDimension.lexicalItems = (Minimalist.tokens t).card
• Minimalist.planarCost t Minimalist.CostDimension.mergeOps = {s ∈ Minimalist.terms t | s.isLeaf = false}.card
• Minimalist.planarCost t Minimalist.CostDimension.agreeOps = 0
• Minimalist.planarCost t Minimalist.CostDimension.ellipsisOps = (Minimalist.elidedDomains t).length