Minimal Search: the generic (cut-policy-parameterized) Merge operator #
MCB's Merge variants and the three coproducts (Δ^ρ/Δ^c/Δ^d) share one operator
shape M = ⊔ ∘ (B ⊗ id) ∘ δ_{S,S'} ∘ Δ, differing only in the coproduct Δ.
mergeOpG cuts parameterizes the operator over the cut enumeration (via
comulAlgHomNG), recovering the Δ^ρ mergeOp as the instance
cuts := cutSummandsN (definitional) and defining the Δ^c Merge mergeOpC τ as
cuts := cutSummandsCN τ. This is the operator-level companion to the
already-generic cut layer (cutSummandsG).
The Δ^c instance is the home of the Minimal-Search ε arc (MCB §1.5,
Prop 1.5.1): the trace coproduct is where extraction depth is recoverable
(RootedTree.Cut.depthC), so the ε-weighted graft and the ε → 0
Sideward-elimination belong on mergeOpC, not the Δ^ρ mergeOp.
Main definitions #
mergeOpG cuts lbl S S'— the generic Merge operator.mergeOp_eq_G— the Δ^ρmergeOpismergeOpG cutSummandsN(definitional).mergeOpC τ lbl S S'— the Δ^c Merge operator.epsWeight,emNetCost/imNetCost/swNetCost— the Minimal-Search ε-weight and the per-merge net costs (EM/IM = 0, Sideward > 0).mergeOpCEps τ ε c— the ε-weighted Δ^c Merge (ε^c • mergeOpC).mergeOpCEps_zero_em,mergeOpCEps_zero_im,mergeOpCEps_zero_sideward— MCB Proposition 1.5.1: at ε → 0, External and Internal Merge survive (1 • M = M), Sideward Merge vanishes (0 • M = 0).
The generic Merge operator M_{S,S'}^{cuts}, parameterized by the cut
enumeration cuts: mergePost lbl S S' ∘ comulAlgHomNG cuts. The
coproduct-agnostic post-chain mergePost (graft B, δ-projection, and
multiplication ⊔) is shared; only the coproduct comulAlgHomNG cuts
varies.
Equations
- Minimalist.Merge.mergeOpG cuts lbl S S' = Minimalist.Merge.mergePost lbl S S' ∘ₗ (RootedTree.ConnesKreimer.comulAlgHomNG cuts).toLinearMap
Instances For
The Δ^ρ Merge operator mergeOp is the generic operator at
cuts := cutSummandsN — definitional, since comulAlgHomN = comulAlgHomNG cutSummandsN.
The Δ^c (trace) Merge operator mergeOpC τ, the generic operator at
cuts := cutSummandsCN τ. Unlike the Δ^ρ mergeOp, this coproduct's
quotients carry a trace leaf at each cut site at exactly the cut depth, so
the Minimal-Search cost Cut.depthC is recoverable — making mergeOpC the
faithful home of MCB's ε-weighted Merge (§1.5).
Equations
- Minimalist.Merge.mergeOpC τ lbl S S' = Minimalist.Merge.mergeOpG (RootedTree.cutSummandsCN τ) lbl S S'
Instances For
The Minimal-Search ε arc (MCB §1.5, Prop 1.5.1) #
The ε-weighted Merge M^ε = ⊔ ∘ (Bᵉ ⊗ id) ∘ δ ∘ Δ (eq 1.5.1) scales the graft
Bᵉ(α⊔β) = ε^{c(𝔐(α,β))} B(α⊔β) (eq 1.5.2) by the Minimal-Search cost ε^c.
Since mergePost is linear and the graft is its only creation, scaling the
graft by ε^c equals scaling the whole operator: mergeOpCEps = ε^c • mergeOpC.
The net cost c is the sum of the two operands' signed depth-costs (MCB rules
1–2, RootedTree.Cut.extractionCost/quotientCost):
- EM
𝔐(T_i, T_j): both whole,c = 0. - IM
𝔐(T_v, T_i/T_v): extracted crown+dand its own quotient−dcancel,c = 0. - Sideward
𝔐(T_v, T'): the crown's+dis uncancelled (no quotient operand),c = d > 0.
At ε → 0, ε^0 = 1 keeps EM/IM, ε^{d>0} = 0 drops Sideward.
The Minimal-Search ε-weight of a merge with net cost c: ε^c
(MCB eq 1.5.2).
Equations
- Minimalist.Merge.epsWeight ε c = ε ^ c
Instances For
External Merge net cost (MCB rule 4, whole operands): 0.
Equations
Instances For
Internal Merge net cost (MCB Prop 1.5.1, IM): the extracted crown's +d
and its own quotient's −d cancel — the signed sum over the same cut p,
truncated to ℕ (it is 0, see imNetCost_eq_zero).
Equations
Instances For
Sideward Merge net cost (MCB Prop 1.5.1, Sideward 2b): the extracted
crown's +d, with no quotient operand to cancel it. Equals Cut.depthC p.
Equations
- Minimalist.Merge.swNetCost p = (RootedTree.Cut.extractionCost p).toNat
Instances For
A Sideward Merge of a lexical-rooted object has strictly positive net cost (MCB Prop 1.5.1) — the uncancelled extraction depth.
The ε-weighted Δ^c Merge operator (MCB §1.5, eq 1.5.2): the Δ^c merge
scaled by the Minimal-Search weight ε^c.
Equations
- Minimalist.Merge.mergeOpCEps τ ε c lbl S S' = Minimalist.Merge.epsWeight ε c • Minimalist.Merge.mergeOpC τ lbl S S'
Instances For
At ε = 1 the weight is trivial and mergeOpCEps recovers the unweighted Δ^c
Merge.
MCB Prop 1.5.1, External Merge survives ε → 0. EM has net cost 0, so its
weight ε^0 = 1 is unaffected: mergeOpCEps τ 0 emNetCost = mergeOpC τ.
MCB Prop 1.5.1, Internal Merge survives ε → 0. IM has net cost 0 — the
extraction +d and its own quotient's −d cancel — so its weight is 1 and
the operator is preserved at ε = 0.
MCB Prop 1.5.1, Sideward Merge vanishes ε → 0. A Sideward Merge has net
cost > 0 (the uncancelled extraction depth), so its weight ε^{>0} = 0 at
ε = 0: the operator is annihilated.
MCB Prop 1.5.1, Sideward Merge vanishes — instantiated at an actual Δ^c
extraction p of a lexical-rooted object: the uncancelled depth makes
swNetCost p > 0, so the operator is annihilated at ε = 0.