Bud generating systems on colored binary trees

A bud generating system ([Gir19]) equips an operad with a set of colors, a set of colored operations (the rules), and a set of terminal colors; the generated language is the set of colored operations derivable from a single-color unit by color-matching operad composition. This file develops the construction over the free binary operad, whose operations are binary trees and whose insertions graft a tree onto a leaf. A Bud.Tree carries a color at every vertex: leaf colors are the operation's inputs, the root color its output, and the internal colors record the colors matched during composition — in a colored operad the color at a grafting vertex is determined by the matched pair, so the decorations are exactly the data of a decomposition into generators.

Main declarations

• Bud.Tree, Bud.Tree.out, Bud.Tree.inputs — vertex-colored binary trees with their output and input colors.
• Bud.Tree.graft — insertion at the i-th leaf, the free binary operad's partial composition; Bud.Tree.graft_graft is the nested-insertion relation.
• Bud.Tree.NodeLocal — a predicate holds at every internal vertex; the invariant format preserved by color-matched grafting.
• Bud.System, Bud.System.Derives, Bud.System.Lang — bud generating systems with initial colors the non-terminal ones ([Gir19]'s I = Ω ∖ T case), derivability from a unit, and the generated language.
• Bud.System.Derives.compose — derivations compose along color-matched inputs; Bud.System.Derives.nodeLocal — any vertex-local property of the rules holds throughout every derivable tree.

Implementation notes

Bud generating systems are the operadic analogue of context-free grammars, with trees in place of words ([Gir19] develops the correspondence); this file follows the register of Mathlib.Computability.ContextFreeGrammar — a rule set, an inductive derivation relation, and the generated language — with colors playing the role of Symbol and the terminal-color set replacing the terminal/nonterminal type split. Mathlib's SimpleGraph.Coloring is not applicable: proper graph coloring constrains adjacent colors to differ, while operadic coloring constrains composed colors to match.

inductive Bud.Tree (Ω : Type u_2) : Type u_2

A binary tree with a color at every vertex: an operation of the bud operad over the free binary operad, decorated with the colors it propagates ([Gir19]).

• leaf {Ω : Type u_2} (c : Ω) : Tree Ω
• node {Ω : Type u_2} (c : Ω) (l r : Tree Ω) : Tree Ω

@[instance_reducible]

instance Bud.instDecidableEqTree {Ω✝ : Type u_2} [DecidableEq Ω✝] : DecidableEq (Tree Ω✝)

Equations

• Bud.instDecidableEqTree = Bud.instDecidableEqTree.decEq

def Bud.instDecidableEqTree.decEq {Ω✝ : Type u_2} [DecidableEq Ω✝] (x✝ x✝¹ : Tree Ω✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Bud.instDecidableEqTree.decEq (Bud.Tree.leaf a) (Bud.Tree.leaf b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Bud.instDecidableEqTree.decEq (Bud.Tree.leaf c) (Bud.Tree.node c_1 l r) = isFalse ⋯
• Bud.instDecidableEqTree.decEq (Bud.Tree.node c l r) (Bud.Tree.leaf c_1) = isFalse ⋯

@[instance_reducible]

instance Bud.instReprTree {Ω✝ : Type u_2} [Repr Ω✝] : Repr (Tree Ω✝)

Equations

• Bud.instReprTree = { reprPrec := Bud.instReprTree.repr }

def Bud.instReprTree.repr {Ω✝ : Type u_2} [Repr Ω✝] : Tree Ω✝ → ℕ → Std.Format

Equations

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

def Bud.Tree.out {Ω : Type u_1} : Tree Ω → Ω

The output color: the color at the root.

Equations

• (Bud.Tree.leaf a).out = a
• (Bud.Tree.node a a_1 a_2).out = a

@[simp]

theorem Bud.Tree.out_leaf {Ω : Type u_1} {c : Ω} : (leaf c).out = c

@[simp]

theorem Bud.Tree.out_node {Ω : Type u_1} {c : Ω} {l r : Tree Ω} : (node c l r).out = c

def Bud.Tree.inputs {Ω : Type u_1} : Tree Ω → List Ω

The input colors: the leaf colors, left to right.

Equations

• (Bud.Tree.leaf a).inputs = [a]
• (Bud.Tree.node a a_1 a_2).inputs = a_1.inputs ++ a_2.inputs

@[simp]

theorem Bud.Tree.inputs_leaf {Ω : Type u_1} {c : Ω} : (leaf c).inputs = [c]

@[simp]

theorem Bud.Tree.inputs_node {Ω : Type u_1} {c : Ω} {l r : Tree Ω} : (node c l r).inputs = l.inputs ++ r.inputs

def Bud.Tree.numInputs {Ω : Type u_1} : Tree Ω → ℕ

The number of inputs.

Equations

• (Bud.Tree.leaf a).numInputs = 1
• (Bud.Tree.node a a_1 a_2).numInputs = a_1.numInputs + a_2.numInputs

@[simp]

theorem Bud.Tree.numInputs_leaf {Ω : Type u_1} {c : Ω} : (leaf c).numInputs = 1

@[simp]

theorem Bud.Tree.numInputs_node {Ω : Type u_1} {c : Ω} {l r : Tree Ω} : (node c l r).numInputs = l.numInputs + r.numInputs

@[simp]

theorem Bud.Tree.length_inputs {Ω : Type u_1} (x : Tree Ω) : x.inputs.length = x.numInputs

theorem Bud.Tree.numInputs_pos {Ω : Type u_1} (x : Tree Ω) : 0 < x.numInputs

theorem Bud.Tree.getElem?_inputs_node {Ω : Type u_1} {c : Ω} {i : ℕ} {l r : Tree Ω} : (node c l r).inputs[i]? = if i < l.numInputs then l.inputs[i]? else r.inputs[i - l.numInputs]?

def Bud.Tree.graft {Ω : Type u_1} : Tree Ω → ℕ → Tree Ω → Tree Ω

Graft s onto the i-th leaf of x: the free binary operad's insertion x ∘ᵢ s. Out-of-range indices leave the tree unchanged.

Equations

• (Bud.Tree.leaf c).graft 0 x✝ = x✝
• (Bud.Tree.leaf c).graft n.succ x✝ = Bud.Tree.leaf c
• (Bud.Tree.node c l r).graft x✝¹ x✝ = if x✝¹ < l.numInputs then Bud.Tree.node c (l.graft x✝¹ x✝) r else Bud.Tree.node c l (r.graft (x✝¹ - l.numInputs) x✝)

@[simp]

theorem Bud.Tree.graft_leaf_zero {Ω : Type u_1} {s : Tree Ω} {c : Ω} : (leaf c).graft 0 s = s

theorem Bud.Tree.graft_node {Ω : Type u_1} {s : Tree Ω} {c : Ω} {i : ℕ} {l r : Tree Ω} : (node c l r).graft i s = if i < l.numInputs then node c (l.graft i s) r else node c l (r.graft (i - l.numInputs) s)

theorem Bud.Tree.out_graft {Ω : Type u_1} {x s : Tree Ω} {i : ℕ} (h : x.inputs[i]? = some s.out) : (x.graft i s).out = x.out

Color-matched grafting preserves the output color.

theorem Bud.Tree.graft_unit {Ω : Type u_1} {x : Tree Ω} {d : Ω} {i : ℕ} (h : x.inputs[i]? = some d) : x.graft i (leaf d) = x

Grafting the unit of the matched color changes nothing.

theorem Bud.Tree.inputs_graft {Ω : Type u_1} {x s : Tree Ω} {i : ℕ} (h : i < x.numInputs) : (x.graft i s).inputs = List.take i x.inputs ++ s.inputs ++ List.drop (i + 1) x.inputs

Grafting splices the inserted tree's inputs into the host's.

theorem Bud.Tree.numInputs_graft {Ω : Type u_1} {x s : Tree Ω} {i : ℕ} (h : i < x.numInputs) : (x.graft i s).numInputs = x.numInputs + s.numInputs - 1

theorem Bud.Tree.getElem?_inputs_graft_middle {Ω : Type u_1} {x s : Tree Ω} {i j : ℕ} (hi : i < x.numInputs) (hj : j < s.numInputs) : (x.graft i s).inputs[i + j]? = s.inputs[j]?

The inserted tree's inputs sit at offset i in the grafted tree.

theorem Bud.Tree.mem_inputs_graft {Ω : Type u_1} {x s : Tree Ω} {i : ℕ} (h : x.inputs[i]? = some s.out) (d : Ω) : d ∈ (x.graft i s).inputs → d ∈ x.inputs ∨ d ∈ s.inputs

An input of the grafted tree comes from the host or from the inserted tree.

theorem Bud.Tree.mem_inputs_graft_of_mem {Ω : Type u_1} {x s : Tree Ω} {i : ℕ} (h : x.inputs[i]? = some s.out) (d : Ω) : d ∈ x.inputs → d ∈ (x.graft i s).inputs ∨ d = s.out

A host input survives grafting, unless it is the matched color.

theorem Bud.Tree.mem_inputs_graft_of_mem_right {Ω : Type u_1} {x s : Tree Ω} {i : ℕ} (h : x.inputs[i]? = some s.out) (d : Ω) : d ∈ s.inputs → d ∈ (x.graft i s).inputs

The inserted tree's inputs are inputs of the grafted tree.

theorem Bud.Tree.graft_graft {Ω : Type u_1} {x s y : Tree Ω} {i j : ℕ} (hi : i < x.numInputs) (hj : j < s.numInputs) : (x.graft i s).graft (i + j) y = x.graft i (s.graft j y)

Nested insertions compose, with the inner index offset by the outer insertion point: the nested case of the operadic insertion relations.

def Bud.Tree.NodeLocal {Ω : Type u_1} (P : Ω → Ω → Ω → Prop) : Tree Ω → Prop

P holds at every internal vertex, of the vertex color and the two children's output colors.

Equations

• Bud.Tree.NodeLocal P (Bud.Tree.leaf a) = True
• Bud.Tree.NodeLocal P (Bud.Tree.node a a_1 a_2) = (P a a_1.out a_2.out ∧ Bud.Tree.NodeLocal P a_1 ∧ Bud.Tree.NodeLocal P a_2)

@[simp]

theorem Bud.Tree.nodeLocal_leaf {Ω : Type u_1} {c : Ω} {P : Ω → Ω → Ω → Prop} : NodeLocal P (leaf c)

@[simp]

theorem Bud.Tree.nodeLocal_node {Ω : Type u_1} {c : Ω} {P : Ω → Ω → Ω → Prop} {l r : Tree Ω} : NodeLocal P (node c l r) ↔ P c l.out r.out ∧ NodeLocal P l ∧ NodeLocal P r

theorem Bud.Tree.NodeLocal.graft {Ω : Type u_1} {x s : Tree Ω} {i : ℕ} {P : Ω → Ω → Ω → Prop} (hx : NodeLocal P x) (hs : NodeLocal P s) (h : x.inputs[i]? = some s.out) : NodeLocal P (x.graft i s)

Color-matched grafting preserves vertex-local properties: the host's vertices keep their colors (the replaced leaf's color equals the inserted root's), and the inserted tree brings its own.

structure Bud.System (Ω : Type u_2) : Type u_2

A bud generating system over the free binary operad ([Gir19], with initial colors I = Ω ∖ Terminal): a set of colored operations (the rules) and a set of terminal colors.

• rules : Set (Tree Ω)
• Terminal : Set Ω

inductive Bud.System.Derives {Ω : Type u_1} (B : System Ω) (c : Ω) : Tree Ω → Prop

Derivability from the unit of color c: start from the one-leaf tree and repeatedly graft rules onto color-matched leaves.

• unit {Ω : Type u_1} {B : System Ω} {c : Ω} (hc : ¬c ∈ B.Terminal) : B.Derives c (Tree.leaf c)
• graft {Ω : Type u_1} {B : System Ω} {c : Ω} {x s : Tree Ω} (i : ℕ) (hx : B.Derives c x) (hs : s ∈ B.rules) (hm : x.inputs[i]? = some s.out) : B.Derives c (x.graft i s)

def Bud.System.Lang {Ω : Type u_1} (B : System Ω) (x : Tree Ω) : Prop

The generated language: trees derivable from some unit, all of whose inputs are terminal.

Equations

• B.Lang x = ((∃ (c : Ω), B.Derives c x) ∧ ∀ (d : Ω), d ∈ x.inputs → d ∈ B.Terminal)

theorem Bud.System.Derives.out_eq {Ω : Type u_1} {B : System Ω} {c : Ω} {x : Tree Ω} (h : B.Derives c x) : x.out = c

A derivation preserves the unit's color as output.

theorem Bud.System.Derives.out_not_terminal {Ω : Type u_1} {B : System Ω} {c : Ω} {x : Tree Ω} (h : B.Derives c x) : ¬c ∈ B.Terminal

The output color of a derivable tree is non-terminal.

theorem Bud.System.Derives.compose {Ω : Type u_1} {B : System Ω} {c d : Ω} {x s : Tree Ω} {i : ℕ} (hx : B.Derives c x) (hi : i < x.numInputs) (hm : x.inputs[i]? = some d) (hs : B.Derives d s) : B.Derives c (x.graft i s)

Derivations compose along a color-matched input: a derivation of the matched color can be carried out in place inside the host.

theorem Bud.System.Derives.nodeLocal {Ω : Type u_1} {B : System Ω} {c : Ω} {x : Tree Ω} {P : Ω → Ω → Ω → Prop} (h : B.Derives c x) (hR : ∀ (r : Tree Ω), r ∈ B.rules → Tree.NodeLocal P r) : Tree.NodeLocal P x

Any vertex-local property of the rules holds throughout every derivable tree: the fundamental invariant of bud derivation.

theorem Bud.System.Derives.node {Ω : Type u_1} {B : System Ω} {c a b : Ω} {S S' : Tree Ω} (hr : Tree.node c (Tree.leaf a) (Tree.leaf b) ∈ B.rules) (hc : ¬c ∈ B.Terminal) (ha : B.Derives a S) (hb : B.Derives b S') : B.Derives c (Tree.node c S S')

Bottom-up node formation: when the one-node operation on the parts' output colors is a rule, joining two derivable trees under it is derivable — top-down bud derivation subsumes bottom-up structure building.