Rebinarization: contracting unary (non-branching) nodes

[MCB25]

contractUnary collapses every unary node (a vertex with exactly one child) into that child, the edge-contraction that takes a syntactic object to its unique maximal binary rooted tree (MCB Def. 1.2.5). It is the second step of MCB's deletion quotient T/ᵈF_v: delete the cut subtrees (leaving the not-necessarily-binary T/ᵖF_v), then contractUnary to rebinarize.

Each contracted unary node removes exactly one vertex, so numNodes (contractUnary t) + unaryCount t = numNodes t.

Contracting unary nodes

contractUnary is a catamorphism over RoseTree.fold: rebuild each node from its already-contracted children, but a lone child replaces the parent — that is where a unary node collapses.

def RoseTree.contractCombine {α : Type u_1} (a : α) : List (RoseTree α) → RoseTree α

Rebuild a node from its (contracted) children: a single child replaces the node, otherwise the node is kept.

Equations

• RoseTree.contractCombine a [c] = c
• RoseTree.contractCombine a x✝ = RoseTree.node a x✝

@[simp]

theorem RoseTree.contractCombine_singleton {α : Type u_1} (a : α) (c : RoseTree α) : contractCombine a [c] = c

theorem RoseTree.contractCombine_nil {α : Type u_1} (a : α) : contractCombine a [] = node a []

theorem RoseTree.contractCombine_cons₂ {α : Type u_1} (a : α) (c d : RoseTree α) (cs : List (RoseTree α)) : contractCombine a (c :: d :: cs) = node a (c :: d :: cs)

def RoseTree.contractUnary {α : Type u_1} : RoseTree α → RoseTree α

Contract every unary node into its child (rebinarize to maximal binary), MCB's Δᵈ (Def. 1.2.5).

Equations

• RoseTree.contractUnary = RoseTree.fold RoseTree.contractCombine

@[simp]

theorem RoseTree.contractUnary_node {α : Type u_1} (a : α) (cs : List (RoseTree α)) : (node a cs).contractUnary = contractCombine a (List.map contractUnary cs)

theorem RoseTree.contractUnary_node_of_two_le {α : Type u_1} (a : α) (cs : List (RoseTree α)) (h : 2 ≤ cs.length) : (node a cs).contractUnary = node a (List.map contractUnary cs)

On a node with ≥ 2 children contractUnary keeps the root and recurses.

def RoseTree.unaryCount {α : Type u_1} : RoseTree α → ℕ

The number of unary (single-child) nodes.

Equations

• RoseTree.unaryCount = RoseTree.fold fun (x : α) (ns : List ℕ) => (if ns.length = 1 then 1 else 0) + ns.sum

@[simp]

theorem RoseTree.unaryCount_node {α : Type u_1} (a : α) (cs : List (RoseTree α)) : (node a cs).unaryCount = (if cs.length = 1 then 1 else 0) + (List.map unaryCount cs).sum

Node-count conservation: each contracted unary node drops one vertex

theorem RoseTree.numNodes_contractUnary_add {α : Type u_1} (t : RoseTree α) : t.contractUnary.numNodes + t.unaryCount = t.numNodes

Every contracted unary node removes exactly one vertex. A single RoseTree.rec' induction: the per-child hypotheses combine over the child list via List.sum_map_add; the two ifs (contractCombine drops the root of a lone child, unaryCount counts it) always sum to one.

unaryCount is PermEquiv-invariant

theorem RoseTree.unaryCount_permEquiv {α : Type u_1} {t s : RoseTree α} (h : t.PermEquiv s) : t.unaryCount = s.unaryCount

contractUnary is PermEquiv-invariant

theorem RoseTree.contractUnary_permStep {α : Type u_1} {t s : RoseTree α} (h : t.PermStep s) : t.contractUnary.PermEquiv s.contractUnary

theorem RoseTree.contractUnary_permEquiv {α : Type u_1} {t s : RoseTree α} (h : t.PermEquiv s) : t.contractUnary.PermEquiv s.contractUnary

Nonplanar contractUnary / unaryCount

def RootedTree.Nonplanar.unaryCount {α : Type u_1} : Nonplanar α → ℕ

The number of unary nodes of a nonplanar tree.

Equations

• RootedTree.Nonplanar.unaryCount = RootedTree.Nonplanar.lift RoseTree.unaryCount ⋯

@[simp]

theorem RootedTree.Nonplanar.unaryCount_mk {α : Type u_1} (t : RoseTree α) : (mk t).unaryCount = t.unaryCount

def RootedTree.Nonplanar.contractUnary {α : Type u_1} : Nonplanar α → Nonplanar α

Rebinarize: contract every unary node (MCB Δᵈ, Def. 1.2.5).

Equations

• RootedTree.Nonplanar.contractUnary = Quotient.map RoseTree.contractUnary ⋯

@[simp]

theorem RootedTree.Nonplanar.contractUnary_mk {α : Type u_1} (t : RoseTree α) : (mk t).contractUnary = mk t.contractUnary

theorem RootedTree.Nonplanar.numNodes_contractUnary_add {α : Type u_1} (t : Nonplanar α) : t.contractUnary.numNodes + t.unaryCount = t.numNodes

Each contracted unary node drops one vertex.