Bud generating systems

A bud generating system consists of colored operations, the rules, and sets of initial and terminal colors. One operation derives another when the second is reached from the first by grafting rules onto inputs of matching color, and the system generates the operations derivable from the unit of an initial color whose inputs are all terminal. This file develops bud generating systems over the free binary operad, whose operations are binary trees and whose partial composition grafts a tree onto a leaf.

Main definitions

• Bud.Tree: binary trees with a color at every vertex.
• Bud.Tree.graft: grafting onto the i-th leaf, the partial composition of the operad.
• Bud.System.Derives, Bud.System.language: derivability and the generated language.
• Bud.System.ofCherries: the system whose rules are the cherries, single binary vertices, with colors in a given relation.

Main statements

• Bud.System.Derives.graft: a derivation can be carried out at any input of a larger tree.
• Bud.System.Derives.node: joining derivable trees under a cherry rule is derivable.
• Bud.System.ofCherries_derives_leaf_iff: in a system of cherries, a tree is derivable from the unit of its root color iff every vertex and its two children form a rule.

Implementation notes

Derives is the reflexive transitive closure of one grafting step, as ContextFreeGrammar.Derives is of one rewriting step. An element of a bud operad records the output and input colors of a tree but not the colors at its internal vertices; a Bud.Tree records those too, as in the vertex colorings of Marcolli and Larson, so that a tree derived from cherries is also its own decomposition into generators.

References

• [Gir19]
• [ML25]

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

A binary tree with a color at every vertex. The leaves carry the input colors and the root the output color.

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

  The unit of color c, a single leaf.

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

  A binary vertex of color c over the trees l and r.

@[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, at the root.

Equations

• (Bud.Tree.leaf c).out = c
• (Bud.Tree.node c l r).out = c

@[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, at the leaves from left to right.

Equations

• (Bud.Tree.leaf c).inputs = [c]
• (Bud.Tree.node c l r).inputs = l.inputs ++ r.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 c).numInputs = 1
• (Bud.Tree.node c l r).numInputs = l.numInputs + r.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.lt_numInputs_of_getElem?_eq_some {Ω : Type u_1} {x : Tree Ω} {d : Ω} {i : ℕ} (h : x.inputs[i]? = some d) : i < 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.cherry {Ω : Type u_1} (c a b : Ω) : Tree Ω

The cherry of color c over the inputs a and b, a single binary vertex.

Equations

• Bud.Tree.cherry c a b = Bud.Tree.node c (Bud.Tree.leaf a) (Bud.Tree.leaf b)

@[simp]

theorem Bud.Tree.out_cherry {Ω : Type u_1} {c a b : Ω} : (cherry c a b).out = c

@[simp]

theorem Bud.Tree.inputs_cherry {Ω : Type u_1} {c a b : Ω} : (cherry c a b).inputs = [a, b]

@[simp]

theorem Bud.Tree.cherry_inj {Ω : Type u_1} {c a b c' a' b' : Ω} : cherry c a b = cherry c' a' b' ↔ c = c' ∧ a = a' ∧ b = b'

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

Graft s onto the i-th leaf of x, the partial composition x ∘ᵢ s of the free binary operad. An index out of range leaves x 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

Grafting at a leaf of the matching color keeps 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 color at a leaf 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 {Ω : 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.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, the inner index offset by the outer insertion point: the sequential composition axiom of the operad.

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

P holds at every internal vertex, of its color and the output colors of its children.

Equations

• Bud.Tree.NodeLocal P (Bud.Tree.leaf c) = True
• Bud.Tree.NodeLocal P (Bud.Tree.node c l r) = (P c l.out r.out ∧ Bud.Tree.NodeLocal P l ∧ Bud.Tree.NodeLocal P r)

@[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

@[simp]

theorem Bud.Tree.nodeLocal_cherry {Ω : Type u_1} {c a b : Ω} {P : Ω → Ω → Ω → Prop} : NodeLocal P (cherry c a b) ↔ P c a b

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)

Grafting at a leaf of the matching color preserves vertex-local properties: the host's vertices keep their colors, 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, with colors in Ω.

• rules : Set (Tree Ω)

  The rules, grafted one at a time in a derivation.

• initial : Set Ω

  The colors whose units begin the derivations of generated trees.

• terminal : Set Ω

  The colors allowed at the inputs of generated trees.

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

B.Produces x y means that grafting a rule of B onto an input of x of the matching color gives y.

Equations

• B.Produces x y = ∃ (r : Bud.Tree Ω), r ∈ B.rules ∧ ∃ (i : ℕ), x.inputs[i]? = some r.out ∧ x.graft i r = y

@[reducible, inline]

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

B.Derives x y means that B can transform x into y in some number of grafting steps.

Equations

• B.Derives = Relation.ReflTransGen B.Produces

def Bud.System.language {Ω : Type u_1} (B : System Ω) : Set (Tree Ω)

A tree is in the language generated by B when its output color is initial, it is derivable from the unit of that color, and its inputs are all terminal.

Equations

• B.language = {x : Bud.Tree Ω | x.out ∈ B.initial ∧ B.Derives (Bud.Tree.leaf x.out) x ∧ ∀ (c : Ω), c ∈ x.inputs → c ∈ B.terminal}

theorem Bud.System.Produces.single {Ω : Type u_1} {B : System Ω} {x y : Tree Ω} (h : B.Produces x y) : B.Derives x y

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

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

theorem Bud.System.Produces.graft {Ω : Type u_1} {B : System Ω} {x s t : Tree Ω} {i : ℕ} (hi : i < x.numInputs) (h : B.Produces s t) : B.Produces (x.graft i s) (x.graft i t)

theorem Bud.System.Derives.graft {Ω : Type u_1} {B : System Ω} {x s t : Tree Ω} {i : ℕ} (hi : i < x.numInputs) (h : B.Derives s t) : B.Derives (x.graft i s) (x.graft i t)

A derivation can be carried out at any input of a larger tree.

theorem Bud.System.Derives.node_left {Ω : Type u_1} {B : System Ω} {s t : Tree Ω} (h : B.Derives s t) (c : Ω) (r : Tree Ω) : B.Derives (Tree.node c s r) (Tree.node c t r)

theorem Bud.System.Derives.node_right {Ω : Type u_1} {B : System Ω} {s t : Tree Ω} (h : B.Derives s t) (c : Ω) (l : Tree Ω) : B.Derives (Tree.node c l s) (Tree.node c l t)

theorem Bud.System.Derives.node {Ω : Type u_1} {B : System Ω} {l r : Tree Ω} {c a b : Ω} (hc : Tree.cherry c a b ∈ B.rules) (hl : B.Derives (Tree.leaf a) l) (hr : B.Derives (Tree.leaf b) r) : B.Derives (Tree.leaf c) (Tree.node c l r)

Joining derivable trees under a cherry rule is derivable: derivability is closed under the colored Merge of the cherry's colors.

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

A vertex-local property of every rule is preserved by derivation.

theorem Bud.System.derives_leaf_of_nodeLocal {Ω : Type u_1} {B : System Ω} {x : Tree Ω} {P : Ω → Ω → Ω → Prop} (hP : ∀ (c a b : Ω), P c a b → Tree.cherry c a b ∈ B.rules) (h : Tree.NodeLocal P x) : B.Derives (Tree.leaf x.out) x

A tree whose every vertex and its children form a cherry rule is derivable from the unit of its root color.

def Bud.System.ofCherries {Ω : Type u_1} (R : Ω → Ω → Ω → Prop) (I T : Set Ω) : System Ω

The system whose rules are the cherries with colors in the relation R, with initial colors I and terminal colors T.

Equations

• Bud.System.ofCherries R I T = { rules := {t : Bud.Tree Ω | ∃ (c : Ω), ∃ (a : Ω), ∃ (b : Ω), R c a b ∧ Bud.Tree.cherry c a b = t}, initial := I, terminal := T }

@[simp]

theorem Bud.System.cherry_mem_ofCherries {Ω : Type u_1} {c a b : Ω} {R : Ω → Ω → Ω → Prop} {I T : Set Ω} : Tree.cherry c a b ∈ (ofCherries R I T).rules ↔ R c a b

theorem Bud.System.ofCherries_derives_leaf_iff {Ω : Type u_1} {x : Tree Ω} {c : Ω} {R : Ω → Ω → Ω → Prop} {I T : Set Ω} : (ofCherries R I T).Derives (Tree.leaf c) x ↔ x.out = c ∧ Tree.NodeLocal R x

In a system of cherries, a tree is derivable from the unit of c iff c is its root color and every vertex and its two children form a rule.

theorem Bud.System.mem_ofCherries_language_iff {Ω : Type u_1} {x : Tree Ω} {R : Ω → Ω → Ω → Prop} {I T : Set Ω} : x ∈ (ofCherries R I T).language ↔ x.out ∈ I ∧ Tree.NodeLocal R x ∧ ∀ (c : Ω), c ∈ x.inputs → c ∈ T

The language of a system of cherries consists of the trees with an initial root color, terminal input colors, and every vertex and its two children forming a rule.