Minimal Search as a weighting of Merge

Marcolli, Chomsky and Berwick implement Minimal Search by weighting the terms of the coproduct (their §1.5). Extracting an accessible term at distance d from its root costs ε^d, the costs of simultaneous extractions multiply, and Merge pays the weight of the terms it grafts, their M^ε_{S,S'} = ⊔ ∘ (B^ε ⊗ id) ∘ δ_{S,S'} ∘ Δ of (1.5.1) and (1.5.2).

The weighted coproduct comulEps ε scales a tree by ε for each level it is moved down on its way to the left channel. At ε = 1 it is the pruning coproduct, so the weighted Merge mergeOpEps 1 is Merge. At ε = 0 only whole components reach the left channel and the coproduct is primitive, so mergeOpEps 0 merges two components of the workspace and nothing else. At every ε, weighted Merge agrees with its value at ε = 0 up to a multiple of ε, and External and Internal Merge have weight 1 (Proposition 1.5.1): they cost nothing, every Sideward term costs at least one, and in the limit only External and Internal Merge remain.

Main definitions

• Minimalist.Merge.comulEps: the depth-weighted coproduct.
• Minimalist.Merge.mergeOpEps: Merge weighted by Minimal Search.

Main results

• Minimalist.Merge.comulEps_one, comulEps_zero: at ε = 1 the weighted coproduct is the pruning coproduct, and at ε = 0 it is the primitive coproduct.
• Minimalist.Merge.mergeOpEps_pair, mergeOpEps_im_composition: External and Internal Merge have weight 1 at every ε.
• Minimalist.Merge.mergeOpEps_eq_add_smul, mergeOpEps_of'_eq_smul_of_not_le: weighted Merge is its value at ε = 0 plus a multiple of ε, so every form of Sideward Merge is a multiple of ε.
• Minimalist.Merge.mergeOpEps_zero_of'_of_not_le, mergeOpEps_zero_pair_add: at ε = 0, Merge vanishes unless both objects are components, and External Merge survives beside any spectators that do not repeat its objects.

Implementation notes

• The book weights the left channel by ε^d and the right channel by ε^{-d}, and lets B^ε read the left weight. In a tensor product over R the two weights would cancel, so the weight is the coefficient of the left channel only. The book uses the right weight only to compute the cost d - d = 0 of Internal Merge, which here is the cost 0 of merging two components.
• The unit stage M_{β,1} grafts nothing and costs nothing (the book's rule 4), so Internal Merge is mergeOpEps ε lbl Q β ∘ mergeOpUnit β, as the book writes it in proving Proposition 1.5.1.
• The weights are polynomial in ε, and the limit ε → 0 is evaluation at ε = 0, the book's M^ε_{S,S'}|_{ε=0}.

References

• [MCB25]

The empty-cut enumeration

instance Minimalist.Merge.instIsMergeCutsEmptyCuts {α : Type u_2} : IsMergeCuts ConnesKreimer.emptyCuts

The weighted coproduct

noncomputable def Minimalist.Merge.comulTreeEpsStep {R : Type u_1} [CommSemiring R] {α : Type u_2} (ε : R) (a : α) (bs : Multiset (UnorderedTree α × TensorProduct R (ConnesKreimer R (UnorderedTree α)) (ConnesKreimer R (UnorderedTree α)))) : UnorderedTree α × TensorProduct R (ConnesKreimer R (UnorderedTree α)) (ConnesKreimer R (UnorderedTree α))

The step of the fold computing the weighted coproduct pairs the node rebuilt from its children with its weighted coproduct.

Equations

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

noncomputable def Minimalist.Merge.comulTreeEps {R : Type u_1} [CommSemiring R] {α : Type u_2} (ε : R) (T : UnorderedTree α) : TensorProduct R (ConnesKreimer R (UnorderedTree α)) (ConnesKreimer R (UnorderedTree α))

The depth-weighted coproduct of a tree ([MCB25] §1.5.2), in which an extraction at distance d from the root has weight ε^d.

Equations

• Minimalist.Merge.comulTreeEps ε T = (UnorderedTree.fold (Minimalist.Merge.comulTreeEpsStep ε) T).2

theorem Minimalist.Merge.comulTreeEps_node {R : Type u_1} [CommSemiring R] {α : Type u_2} (ε : R) (a : α) (F : UnorderedTree.Forest (UnorderedTree α)) : comulTreeEps ε (UnorderedTree.node a F) = ConnesKreimer.ofTree (UnorderedTree.node a F) ⊗ₜ[R] 1 + (TensorProduct.map (ConnesKreimer.aeval fun (t : UnorderedTree α) => ε • ConnesKreimer.ofTree t).toLinearMap (ConnesKreimer.bPlusLin a)) (Multiset.map (comulTreeEps ε) F).prod

The weighted coproduct of a node keeps the node whole, or takes the weighted coproduct of its children with every extracted tree one level further down.

noncomputable def Minimalist.Merge.comulEps {R : Type u_1} [CommSemiring R] {α : Type u_2} (ε : R) : ConnesKreimer R (UnorderedTree α) →ₐ[R] TensorProduct R (ConnesKreimer R (UnorderedTree α)) (ConnesKreimer R (UnorderedTree α))

The depth-weighted coproduct on workspaces.

Equations

• Minimalist.Merge.comulEps ε = ConnesKreimer.aeval (Minimalist.Merge.comulTreeEps ε)

@[simp]

theorem Minimalist.Merge.comulEps_ofTree {R : Type u_1} [CommSemiring R] {α : Type u_2} (ε : R) (T : UnorderedTree α) : (comulEps ε) (ConnesKreimer.ofTree T) = comulTreeEps ε T

theorem Minimalist.Merge.comulEps_one {R : Type u_1} [CommSemiring R] {α : Type u_2} : comulEps 1 = ConnesKreimer.comulAlgHomN

At ε = 1 every extraction has weight 1, and the weighted coproduct is the pruning coproduct.

theorem Minimalist.Merge.comulTreeEps_zero {R : Type u_1} [CommSemiring R] {α : Type u_2} (T : UnorderedTree α) : comulTreeEps 0 T = ConnesKreimer.ofTree T ⊗ₜ[R] 1 + 1 ⊗ₜ[R] ConnesKreimer.ofTree T

At ε = 0 every tree is primitive for the weighted coproduct, since only whole components reach the left channel.

theorem Minimalist.Merge.comulEps_zero {R : Type u_1} [CommSemiring R] {α : Type u_2} : comulEps 0 = ConnesKreimer.comulPrim

At ε = 0 the weighted coproduct is the primitive coproduct.

The weighted coproduct modulo ε

Every term of the weighted coproduct but those of ε = 0 extracts a tree and so carries a factor of ε, and every term but T ⊗ 1 has a left factor with fewer vertices than T.

theorem Minimalist.Merge.comulEps_eq_add_smul {R : Type u_1} [CommSemiring R] {α : Type u_2} (ε : R) (x : ConnesKreimer R (UnorderedTree α)) : ∃ (y : TensorProduct R (ConnesKreimer R (UnorderedTree α)) (ConnesKreimer R (UnorderedTree α))), (comulEps ε) x = (comulEps 0) x + ε • y

The weighted coproduct agrees with its value at ε = 0 modulo ε.

Weighted Merge

noncomputable def Minimalist.Merge.mergeOpEps {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] (ε : R) (lbl : α) (S S' : UnorderedTree α) : ConnesKreimer R (UnorderedTree α) →ₗ[R] ConnesKreimer R (UnorderedTree α)

Merge weighted by Minimal Search ([MCB25] (1.5.1)) grafts each matching term with the weight of its extractions.

Equations

• Minimalist.Merge.mergeOpEps ε lbl S S' = Minimalist.Merge.mergePost lbl S S' ∘ₗ (Minimalist.Merge.comulEps ε).toLinearMap

theorem Minimalist.Merge.mergeOpEps_one {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] (lbl : α) (S S' : UnorderedTree α) : mergeOpEps 1 lbl S S' = mergeOp lbl S S'

At ε = 1 weighted Merge is Merge.

theorem Minimalist.Merge.mergeOpEps_zero {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] (lbl : α) (S S' : UnorderedTree α) : mergeOpEps 0 lbl S S' = mergeOpG ConnesKreimer.emptyCuts lbl S S'

At ε = 0 weighted Merge is Merge at the empty-cut enumeration.

theorem Minimalist.Merge.mergeOpEps_zero_of'_of_not_le {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] (lbl : α) {S S' : UnorderedTree α} {F : UnorderedTree.Forest (UnorderedTree α)} (h : ¬{S, S'} ≤ F) : (mergeOpEps 0 lbl S S') (ConnesKreimer.of' F) = 0

At ε = 0 Merge vanishes on a workspace unless S and S' are both components of it ([MCB25] Proposition 1.5.1). This covers each form of Sideward Merge, in which S or S' is an accessible term of a component.

theorem Minimalist.Merge.mergeOpEps_zero_ofTree_mul {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] (lbl : α) {S S' U : UnorderedTree α} (hS : U ≠ S) (hS' : U ≠ S') (w : ConnesKreimer R (UnorderedTree α)) : (mergeOpEps 0 lbl S S') (ConnesKreimer.ofTree U * w) = ConnesKreimer.ofTree U * (mergeOpEps 0 lbl S S') w

At ε = 0 Merge commutes with a spectator tree U other than S and S', whatever accessible terms U has.

theorem Minimalist.Merge.mergeOpEps_zero_of'_mul {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] (lbl : α) {S S' : UnorderedTree α} {F : UnorderedTree.Forest (UnorderedTree α)} (hS : S ∉ F) (hS' : S' ∉ F) (w : ConnesKreimer R (UnorderedTree α)) : (mergeOpEps 0 lbl S S') (ConnesKreimer.of' F * w) = ConnesKreimer.of' F * (mergeOpEps 0 lbl S S') w

At ε = 0 a spectator workspace passes through Merge whenever neither S nor S' is one of its components.

theorem Minimalist.Merge.mergeOpEps_zero_pair_add {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] (lbl : α) {S S' : UnorderedTree α} {F : UnorderedTree.Forest (UnorderedTree α)} (hS : S ∉ F) (hS' : S' ∉ F) : (mergeOpEps 0 lbl S S') (ConnesKreimer.of' ({S, S'} + F)) = ConnesKreimer.of' ({UnorderedTree.node lbl {S, S'}} + F)

External Merge survives at ε = 0 ([MCB25] Proposition 1.5.1), beside any spectator workspace that does not repeat S or S' as a component.

theorem Minimalist.Merge.mergeOpEps_eq_add_smul {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] (ε : R) (lbl : α) (S S' : UnorderedTree α) (x : ConnesKreimer R (UnorderedTree α)) : ∃ (y : ConnesKreimer R (UnorderedTree α)), (mergeOpEps ε lbl S S') x = (mergeOpEps 0 lbl S S') x + ε • y

Weighted Merge agrees with its value at ε = 0 modulo ε, so External Merge and Internal Merge, which survive at ε = 0, are its leading terms ([MCB25] Proposition 1.5.1).

theorem Minimalist.Merge.mergeOpEps_of'_eq_smul_of_not_le {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] (ε : R) (lbl : α) {S S' : UnorderedTree α} {F : UnorderedTree.Forest (UnorderedTree α)} (h : ¬{S, S'} ≤ F) : ∃ (y : ConnesKreimer R (UnorderedTree α)), (mergeOpEps ε lbl S S') (ConnesKreimer.of' F) = ε • y

Unless S and S' are both components of the workspace, weighted Merge is a multiple of ε, so every form of Sideward Merge costs at least one ([MCB25] Proposition 1.5.1).

theorem Minimalist.Merge.mergeOpEps_pair {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] (ε : R) (lbl : α) (S S' : UnorderedTree α) : (mergeOpEps ε lbl S S') (ConnesKreimer.of' {S, S'}) = ConnesKreimer.of' {UnorderedTree.node lbl {S, S'}}

External Merge has weight 1 at every ε ([MCB25] Proposition 1.5.1), since its two objects are taken whole, at no cost.

theorem Minimalist.Merge.mergeOpEps_im_composition {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] (ε : R) (lbl : α) (β T Q : UnorderedTree α) (p0 : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) (h_filter : Multiset.filter (fun (p : Multiset (UnorderedTree α) × UnorderedTree α) => p.1 = {β}) (ConnesKreimer.cutSummandsN T) = {p0}) (h_remainder : p0.2 = Q) (hTβ : T ≠ β) : (mergeOpEps ε lbl Q β) ((mergeOpUnit β) (ConnesKreimer.of' {T})) = ConnesKreimer.of' {UnorderedTree.node lbl {Q, β}}

Internal Merge has weight 1 at every ε ([MCB25] Proposition 1.5.1), since its unit stage is weightless and its second stage merges two components.