Subtree extraction

def Minimalism.SyntacticObject.subtrees : SyntacticObject → List SyntacticObject

All subtrees of an SO (including self)

Equations

• (Minimalism.SyntacticObject.leaf a).subtrees = [Minimalism.SyntacticObject.leaf a]
• (a.node b).subtrees = a.node b :: (a.subtrees ++ b.subtrees)

def Minimalism.SyntacticObject.properSubtrees : SyntacticObject → List SyntacticObject

Proper subtrees (excluding self)

Equations

• (Minimalism.SyntacticObject.leaf a).properSubtrees = []
• (a.node b).properSubtrees = a.subtrees ++ b.subtrees

def Minimalism.SyntacticObject.internalNodes : SyntacticObject → List SyntacticObject

Internal nodes (subtrees that are.node)

Equations

• (Minimalism.SyntacticObject.leaf a).internalNodes = []
• (a.node b).internalNodes = a.node b :: (a.internalNodes ++ b.internalNodes)

theorem Minimalism.internalNodes_length_eq_nodeCount (so : SyntacticObject) : so.internalNodes.length = so.nodeCount

Internal node count (= nodeCount from SyntacticObjects.lean)

Leaf multisets (frontier tokens)

def Minimalism.SyntacticObject.leafMultiset : SyntacticObject → List LIToken

The multiset of leaf tokens at the frontier of an SO

Equations

• (Minimalism.SyntacticObject.leaf a).leafMultiset = [a]
• (a.node b).leafMultiset = a.leafMultiset ++ b.leafMultiset

theorem Minimalism.leafMultiset_length_eq_leafCount (so : SyntacticObject) : so.leafMultiset.length = so.leafCount

def Minimalism.SyntacticObject.leafMultisetM (so : SyntacticObject) : Multiset LIToken

Leaf multiset as a Multiset — the mathematically correct type (frontier token identity is order-independent).

Equations

• so.leafMultisetM = ↑so.leafMultiset

Accessible terms (Definition 2.4)

For a tree T, the accessible terms are the leaf-sets of subtrees rooted at internal nodes. That is, for each internal node v, we take L(T_v) = the leaf multiset of the subtree rooted at v.

def Minimalism.SyntacticObject.accessibleTerms : SyntacticObject → List (List LIToken)

Accessible terms: leaf-multisets of subtrees at internal nodes

Equations

• (Minimalism.SyntacticObject.leaf a).accessibleTerms = []
• (a.node b).accessibleTerms = (a.node b).leafMultiset :: (a.accessibleTerms ++ b.accessibleTerms)

def Minimalism.SyntacticObject.accessibleTermsM (so : SyntacticObject) : Multiset (Multiset LIToken)

Accessible terms as Multiset of Multisets — order-independent identity.

Equations

• so.accessibleTermsM = ↑(List.map (fun (x : List Minimalism.LIToken) => ↑x) so.accessibleTerms)

theorem Minimalism.accessibleTerms_length_eq_nodeCount (so : SyntacticObject) : so.accessibleTerms.length = so.nodeCount

Number of accessible terms = number of internal nodes

Workspace counting (Definition 2.4, equations 2.8–2.9)

A workspace (forest) is a list of SOs = the connected components.

def Minimalism.b₀ (F : List SyntacticObject) : ℕ

b₀(F): number of connected components = List.length

Equations

• Minimalism.b₀ F = F.length

def Minimalism.numAcc (F : List SyntacticObject) : ℕ

Total accessible terms across all trees in forest

Equations

• Minimalism.numAcc F = (List.map (fun (x : Minimalism.SyntacticObject) => x.accessibleTerms.length) F).sum

def Minimalism.wsSize (F : List SyntacticObject) : ℕ

σ(F) = b₀(F) + #Acc(F) (eq 2.8)

Equations

• Minimalism.wsSize F = Minimalism.b₀ F + Minimalism.numAcc F

def Minimalism.numVertices (F : List SyntacticObject) : ℕ

Total internal nodes across all trees in forest

Equations

• Minimalism.numVertices F = (List.map (fun (x : Minimalism.SyntacticObject) => x.nodeCount) F).sum

def Minimalism.wsSizeAlt (F : List SyntacticObject) : ℕ

σ̂(F) = b₀(F) + #V(F) (eq 2.9)

Equations

• Minimalism.wsSizeAlt F = Minimalism.b₀ F + Minimalism.numVertices F

theorem Minimalism.numAcc_eq_numVertices (F : List SyntacticObject) : numAcc F = numVertices F

numAcc and numVertices agree: accessible term count = internal node count per tree, so the sums coincide.

theorem Minimalism.wsSize_eq_wsSizeAlt (F : List SyntacticObject) : wsSize F = wsSizeAlt F

σ̂ = σ since #Acc = #V (both equal total nodeCount)

Depth of a subtree occurrence

def Minimalism.SyntacticObject.depthOf (α β : SyntacticObject) : Option ℕ

Depth of β in α (0 if β = α, +1 per level)

Equations

• (Minimalism.SyntacticObject.leaf a).depthOf β = if (Minimalism.SyntacticObject.leaf a == β) = true then some 0 else none
• (a.node b).depthOf β = if (a.node b == β) = true then some 0 else match a.depthOf β, b.depthOf β with | some d, x => some (d + 1) | x, some d => some (d + 1) | none, none => none

Proposition 2.17: Counting behavior of EM vs IM

External Merge takes two trees T₁, T₂ from workspace F and creates merge(T₁, T₂), reducing components by 1 and adding a new root node.

Internal Merge takes a tree T from F with a contained subtree β, re-merging β at the root: merge(β, T), keeping the same components.

List filter/count helpers

def Minimalism.emWorkspace (T₁ T₂ : SyntacticObject) (F : List SyntacticObject) : List SyntacticObject

External Merge: workspace goes from F to F' where T₁,T₂ ∈ F replaced by merge(T₁,T₂)

Equations

• Minimalism.emWorkspace T₁ T₂ F = List.filter (fun (x : Minimalism.SyntacticObject) => x != T₂) (Minimalism.merge T₁ T₂ :: List.filter (fun (x : Minimalism.SyntacticObject) => x != T₁) F)

def Minimalism.imWorkspace (T β : SyntacticObject) (F : List SyntacticObject) : List SyntacticObject

Internal Merge: workspace goes from F to F' where T ∈ F replaced by merge(β, T)

Equations

• Minimalism.imWorkspace T β F = Minimalism.merge β T :: List.filter (fun (x : Minimalism.SyntacticObject) => x != T) F

theorem Minimalism.em_b0_decreases {F : List SyntacticObject} (T₁ T₂ : SyntacticObject) (hT₁ : T₁ ∈ F) (hT₂ : T₂ ∈ F) (hne : T₁ ≠ T₂) (huniq₁ : List.count T₁ F = 1) (huniq₂ : List.count T₂ F = 1) : b₀ (emWorkspace T₁ T₂ F) = b₀ F - 1

EM: b₀ decreases by 1 (two components become one)

theorem Minimalism.em_acc_increases {F : List SyntacticObject} (T₁ T₂ : SyntacticObject) (hT₁ : T₁ ∈ F) (hT₂ : T₂ ∈ F) (hne : T₁ ≠ T₂) (huniq₁ : List.count T₁ F = 1) (huniq₂ : List.count T₂ F = 1) : numAcc (emWorkspace T₁ T₂ F) = numAcc F + 1

EM: accessible terms increase by 2 (new root adds one for each child subtree plus the root itself, but the children's accessible terms are preserved)

theorem Minimalism.em_wsSize_change {F : List SyntacticObject} (T₁ T₂ : SyntacticObject) (hT₁ : T₁ ∈ F) (hT₂ : T₂ ∈ F) (hne : T₁ ≠ T₂) (huniq₁ : List.count T₁ F = 1) (huniq₂ : List.count T₂ F = 1) : wsSize (emWorkspace T₁ T₂ F) = wsSize F

EM: σ increases by 1 (Δb₀ = -1, Δ#Acc = +1, net = 0... but σ = b₀ + #Acc so Δσ = -1 + 1 = 0 — actually MCB2023 Table says Δσ = +1 for EM. This is because Δ#Acc = +2 in their counting.

theorem Minimalism.im_b0_preserved {F : List SyntacticObject} (T β : SyntacticObject) (hT : T ∈ F) (hβT : contains T β) (huniq : List.count T F = 1) : b₀ (imWorkspace T β F) = b₀ F

IM: b₀ preserved (same number of components)

theorem Minimalism.im_acc_change {F : List SyntacticObject} (T β : SyntacticObject) (hT : T ∈ F) (hβT : contains T β) (huniq : List.count T F = 1) : numAcc (imWorkspace T β F) = numAcc F + 1 + β.nodeCount

IM: accessible terms increase by 1 + β.nodeCount.

merge(β, T) =.node β T has nodeCount = 1 + β.nodeCount + T.nodeCount. Since T is replaced in the forest, the net change in numVertices (= numAcc) is 1 + β.nodeCount. Note: β's subtree is duplicated (it remains inside T and also appears as a new child of the root). In MCB2023's sharing model β would not be duplicated and the change would be just +1; here we track the tree-copy semantics faithfully.

theorem Minimalism.im_wsSizeAlt_change {F : List SyntacticObject} (T β : SyntacticObject) (hT : T ∈ F) (hβT : contains T β) (huniq : List.count T F = 1) : wsSizeAlt (imWorkspace T β F) = wsSizeAlt F + 1 + β.nodeCount

IM: σ̂ increases by 1 + β.nodeCount.

wsSizeAlt = b₀ + numVertices. Under IM, b₀ is preserved and numVertices increases by 1 + β.nodeCount (see im_acc_change).

Corollary 2.22: Sideward/Countercyclic Merge violates constraints

Sideward Merge: merge(β, T₂) where β is contained in T₁, and T₁ ≠ T₂. This extracts a subterm from one tree and merges it with another.

Countercyclic Merge: merge(T₁, T₂) where one is contained in the other but NOT as a root constituent.

structure Minimalism.SidewardMerge : Type

Sideward Merge condition: β is in T₁, we merge β with T₂

• T₁ : SyntacticObject
• T₂ : SyntacticObject
• β : SyntacticObject
• distinct : self.T₁ ≠ self.T₂
• β_in_T₁ : contains self.T₁ self.β
• β_not_T₁ : self.β ≠ self.T₁
• β_not_in_T₂ : ¬contains self.T₂ self.β

def Minimalism.sidewardWorkspace (sm : SidewardMerge) (F : List SyntacticObject) : List SyntacticObject

Sideward Merge workspace: remove nothing (β stays in T₁), add merge(β, T₂)

Equations

• Minimalism.sidewardWorkspace sm F = Minimalism.merge sm.β sm.T₂ :: F

theorem Minimalism.sideward_violates_b0 (sm : SidewardMerge) (F : List SyntacticObject) : b₀ (sidewardWorkspace sm F) = b₀ F + 1

Sideward Merge violates b₀ preservation: it adds a component without removing one. This is the key constraint violation that distinguishes it from standard EM/IM.

Bridge: counting behavior consistent with EM/IM trichotomy

The counting characterization aligns with the order-theoretic partition from MergeUnification.lean.

theorem Minimalism.em_counting_from_trichotomy (α β : SyntacticObject) (F : List SyntacticObject) (h : ¬contains α β ∧ ¬contains β α) (hne : α ≠ β) (hα : α ∈ F) (hβ : β ∈ F) (huniqα : List.count α F = 1) (huniqβ : List.count β F = 1) : b₀ (emWorkspace α β F) = b₀ F - 1

When α and β are incomparable (EM case), merge reduces component count by 1. Requires uniqueness of α and β in F (each appears exactly once).

theorem Minimalism.im_counting_from_trichotomy (α β : SyntacticObject) (F : List SyntacticObject) (h : contains α β) (hα : α ∈ F) (huniq : List.count α F = 1) : b₀ (imWorkspace α β F) = b₀ F

When one contains the other (IM case), merge preserves component count. Requires uniqueness of α in F.