Minimal Yield (MCB Definition 1.6.1) #
[MCB25] §1.6.1, Def 1.6.1 on book p. 63
M-C-B's Minimal Yield principle as a predicate on workspace transformations,
with the per-merge counting characterizations of Prop 1.6.4 (EM/IM, p. 66)
and Prop 1.6.8 (Sideward, p. 69), on the canonical nonplanar carrier
Nonplanar (α ⊕ β) (Sum.inl lexical, Sum.inr trace). A workspace is a
Forest (Nonplanar (α ⊕ β)) = Multiset (Nonplanar (α ⊕ β)); External Merge of
S, S' builds Nonplanar.node (Sum.inl lbl) {S, S'}.
The principle (Def 1.6.1, eq. 1.6.2) asks of a transformation Φ:
b₀(Φ F) ≤ b₀ F (no divergence), α(Φ F) ≥ α F (no information loss),
σ(Φ F) = σ F + 1 (minimal yield). MinimalYield (strong) and
MinimalYieldWeak (first two bounds) are stated relationally.
Per-merge signatures (Prop 1.6.4 + Prop 1.6.8) #
| Merge | Δb₀ | Δα | Δσ | Strong | Weak |
|---|---|---|---|---|---|
| External | −1 | +2 | +1 | ✓ | ✓ |
| Internal Δᶜ | 0 | +1 | +1 | ✓ | ✓ |
| Internal Δᵈ | 0 | 0 | 0 | ✗ | ✓ |
| Sideward 2(b) Δᶜ | 0 | +1 | +1 | ✓ | ✓ |
| Sideward 3(a)/3(b) | +1 | ⋯ | ⋯ | ✗ | ✗ |
The size-delta theorems take the accessible-term relation as a hypothesis
(accCount/accCountC extraction, MCB Lemma 1.6.3, eqs. 1.6.7/1.6.8);
Sideward 3(a)/3(b) are ruled out by both forms via Δb₀ > 0.
The Minimal Yield principle #
The weak Minimal Yield principle: no increase in b₀, no decrease in α.
Instances For
The Minimal Yield principle: the weak form plus σ up by exactly one.
- minimalYield : RootedTree.Forest.sigma F' = RootedTree.Forest.sigma F + 1
Instances For
MinimalYieldWeak as a Pareto pullback preorder #
The Pareto signature (b₀ᵒᵈ, α), b₀ dualised so fewer components ranks higher.
Equations
- Minimalist.Merge.MinimalYieldSignature F = (OrderDual.toDual (RootedTree.Forest.b₀ F), RootedTree.Forest.alpha F)
Instances For
MinimalYieldWeak packaged as a PullbackPreorder.
Equations
- One or more equations did not get rendered due to their size.
Instances For
External Merge #
External Merge of a pair satisfies Minimal Yield: Δb₀ = −1, Δα = +2, Δσ = +1.
Internal Merge #
Internal Merge via composition leaves b₀, α, σ unchanged (Δᵈ counting):
the accessible-term relation α(T) = α(mover) + α(Q) + 2 is MCB eq. 1.6.7.
im_pair_size_deltas_deletion with the α relation discharged from a Δᵈ
admissible cut: deleting mover from T and rebinarizing the remainder
(contractUnary p.2) leaves b₀, α, σ unchanged. unaryCount p.2 = 1
characterizes a single edge cut at a binary node.
Internal Merge via composition leaves b₀ fixed and raises αᶜ, σᶜ by one
(Δᶜ counting): the relation αᶜ(T) = αᶜ(β_t) + αᶜ(trunk) + 1 is MCB eq. 1.6.8.
im_pair_size_deltas_contraction with the αᶜ relation discharged from a Δᶜ
admissible cut: re-merging an accessible subtree β_t of T = node (inl a₀) F₀
with the contraction quotient p.2 raises αᶜ, σᶜ by one.
Sideward Merge #
Sideward Merge of type 2(b) leaves the component count b₀ unchanged.
Sideward Merge of type 3(a) increases the component count b₀ by one.
Sideward Merge of type 3(b) increases the component count b₀ by one.
Sideward Merge of type 3(a) violates the weak Minimal Yield principle (Δb₀ > 0).
Sideward Merge of type 3(b) violates the weak Minimal Yield principle (Δb₀ > 0).
Strong-form corollary of sideward_3a_violates_noDivergenceWeak.
Strong-form corollary of sideward_3b_violates_noDivergenceWeak.
Unit merge #
The unit-merge stage {T} → {β, T/β} violates weak Minimal Yield (Δb₀ > 0).
Strong-form corollary of unitMerge_violates_noDivergenceWeak.