Trees

Unified tree type parameterized by node labels (C) and terminal content (W).

Tree C W — The Y-Model Tree

N-ary branching with categories on every node. Supports both:

• Compositional interpretation (LF): interp/evalTree in Composition/Tree.lean — type-driven, ignores categories
• Structural operations (PF): @cite{katzir-2007} StructOp (substitution, deletion, contraction) in Alternatives/Structural.lean — category-aware

Parameterized by category type C (UD tags, CCG categories, feature bundles, Unit for unlabeled, ...) and terminal type W.

Instantiations

• Tree Unit String — category-free, for H&K composition. Use convenience constructors .leaf, .bin, .un, .tr, .binder.
• Tree Cat String — UD-grounded categories, for Katzir structural alternatives.
• Tree Unit LIToken — bare phrase structure, for Minimalist syntax (categories inside LIToken, not on nodes).

Cat — Default Category System

Grounded in Universal Dependencies UPOS. Word-level categories via head : UPOS → Cat, phrasal via proj : UPOS → Cat, plus S and CP.

TreePath and Tree.toTreeOrder

A TreePath is a list of child indices identifying a subtree position. The forgetful map Tree.toTreeOrder extracts the dominance partial order from any Tree C W as a Core.Order.TreeOrder TreePath, making the B&P command-relation library (Linglib.Core.Order.Command) applicable to concrete trees regardless of category type.

inductive Core.Tree.Cat : Type

Default syntactic category system grounded in Universal Dependencies UPOS (@cite{de-marneffe-zeman-2021}).

• head pos — word-level (terminal): wraps a UPOS tag directly
• proj pos — maximal X-bar projection of a UPOS head
• S — sentence/clause (not a projection of a single lexical head)
• CP — complementizer phrase

Phrasal categories are derived systematically: NP = proj .NOUN, VP = proj .VERB, DP = proj .DET, ConjP = proj .CCONJ, etc.

This is one possible instantiation of Tree's C parameter. Framework-specific category systems (CCG functors, Minimalist feature bundles, etc.) can be used instead.

• head : UD.UPOS → Cat
• proj : UD.UPOS → Cat
• S : Cat
• CP : Cat

@[implicit_reducible]

instance Core.Tree.instDecidableEqCat : DecidableEq Cat

Equations

• Core.Tree.instDecidableEqCat = Core.Tree.instDecidableEqCat.decEq

def Core.Tree.instDecidableEqCat.decEq (x✝ x✝¹ : Cat) : Decidable (x✝ = x✝¹)

Equations

• Core.Tree.instDecidableEqCat.decEq (Core.Tree.Cat.head a) (Core.Tree.Cat.head b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Core.Tree.instDecidableEqCat.decEq (Core.Tree.Cat.head a) (Core.Tree.Cat.proj a_1) = isFalse ⋯
• Core.Tree.instDecidableEqCat.decEq (Core.Tree.Cat.head a) Core.Tree.Cat.S = isFalse ⋯
• Core.Tree.instDecidableEqCat.decEq (Core.Tree.Cat.head a) Core.Tree.Cat.CP = isFalse ⋯
• Core.Tree.instDecidableEqCat.decEq (Core.Tree.Cat.proj a) (Core.Tree.Cat.head a_1) = isFalse ⋯
• Core.Tree.instDecidableEqCat.decEq (Core.Tree.Cat.proj a) (Core.Tree.Cat.proj b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Core.Tree.instDecidableEqCat.decEq (Core.Tree.Cat.proj a) Core.Tree.Cat.S = isFalse ⋯
• Core.Tree.instDecidableEqCat.decEq (Core.Tree.Cat.proj a) Core.Tree.Cat.CP = isFalse ⋯
• Core.Tree.instDecidableEqCat.decEq Core.Tree.Cat.S (Core.Tree.Cat.head a) = isFalse ⋯
• Core.Tree.instDecidableEqCat.decEq Core.Tree.Cat.S (Core.Tree.Cat.proj a) = isFalse ⋯
• Core.Tree.instDecidableEqCat.decEq Core.Tree.Cat.S Core.Tree.Cat.S = isTrue ⋯
• Core.Tree.instDecidableEqCat.decEq Core.Tree.Cat.S Core.Tree.Cat.CP = isFalse Core.Tree.instDecidableEqCat.decEq._proof_13
• Core.Tree.instDecidableEqCat.decEq Core.Tree.Cat.CP (Core.Tree.Cat.head a) = isFalse ⋯
• Core.Tree.instDecidableEqCat.decEq Core.Tree.Cat.CP (Core.Tree.Cat.proj a) = isFalse ⋯
• Core.Tree.instDecidableEqCat.decEq Core.Tree.Cat.CP Core.Tree.Cat.S = isFalse Core.Tree.instDecidableEqCat.decEq._proof_16
• Core.Tree.instDecidableEqCat.decEq Core.Tree.Cat.CP Core.Tree.Cat.CP = isTrue ⋯

def Core.Tree.instReprCat.repr : Cat → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Core.Tree.instReprCat.repr Core.Tree.Cat.S prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Tree.Cat.S")).group prec✝
• Core.Tree.instReprCat.repr Core.Tree.Cat.CP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Tree.Cat.CP")).group prec✝

@[implicit_reducible]

instance Core.Tree.instReprCat : Repr Cat

Equations

• Core.Tree.instReprCat = { reprPrec := Core.Tree.instReprCat.repr }

@[implicit_reducible]

instance Core.Tree.instInhabitedCat : Inhabited Cat

Equations

• Core.Tree.instInhabitedCat = { default := Core.Tree.Cat.S }

@[implicit_reducible]

instance Core.Tree.instBEqCat : BEq Cat

Equations

• Core.Tree.instBEqCat = { beq := fun (a b : Core.Tree.Cat) => decide (a = b) }

instance Core.Tree.instLawfulBEqCat : LawfulBEq Cat

@[reducible, match_pattern, inline]

abbrev Core.Tree.Cat.N : Cat

Equations

• Core.Tree.Cat.N = Core.Tree.Cat.head UD.UPOS.NOUN

@[reducible, match_pattern, inline]

abbrev Core.Tree.Cat.V : Cat

Equations

• Core.Tree.Cat.V = Core.Tree.Cat.head UD.UPOS.VERB

@[reducible, match_pattern, inline]

abbrev Core.Tree.Cat.Det : Cat

Equations

• Core.Tree.Cat.Det = Core.Tree.Cat.head UD.UPOS.DET

@[reducible, match_pattern, inline]

abbrev Core.Tree.Cat.Adj : Cat

Equations

• Core.Tree.Cat.Adj = Core.Tree.Cat.head UD.UPOS.ADJ

@[reducible, match_pattern, inline]

abbrev Core.Tree.Cat.Adv : Cat

Equations

• Core.Tree.Cat.Adv = Core.Tree.Cat.head UD.UPOS.ADV

@[reducible, match_pattern, inline]

abbrev Core.Tree.Cat.P : Cat

Equations

• Core.Tree.Cat.P = Core.Tree.Cat.head UD.UPOS.ADP

@[reducible, match_pattern, inline]

abbrev Core.Tree.Cat.Conj : Cat

Equations

• Core.Tree.Cat.Conj = Core.Tree.Cat.head UD.UPOS.CCONJ

@[reducible, match_pattern, inline]

abbrev Core.Tree.Cat.Neg : Cat

Equations

• Core.Tree.Cat.Neg = Core.Tree.Cat.head UD.UPOS.PART

@[reducible, match_pattern, inline]

abbrev Core.Tree.Cat.C : Cat

Equations

• Core.Tree.Cat.C = Core.Tree.Cat.head UD.UPOS.SCONJ

@[reducible, match_pattern, inline]

abbrev Core.Tree.Cat.Num : Cat

Equations

• Core.Tree.Cat.Num = Core.Tree.Cat.head UD.UPOS.NUM

@[reducible, match_pattern, inline]

abbrev Core.Tree.Cat.Pron : Cat

Equations

• Core.Tree.Cat.Pron = Core.Tree.Cat.head UD.UPOS.PRON

@[reducible, match_pattern, inline]

abbrev Core.Tree.Cat.Aux : Cat

Equations

• Core.Tree.Cat.Aux = Core.Tree.Cat.head UD.UPOS.AUX

@[reducible, match_pattern, inline]

abbrev Core.Tree.Cat.NP : Cat

Equations

• Core.Tree.Cat.NP = Core.Tree.Cat.proj UD.UPOS.NOUN

@[reducible, match_pattern, inline]

abbrev Core.Tree.Cat.VP : Cat

Equations

• Core.Tree.Cat.VP = Core.Tree.Cat.proj UD.UPOS.VERB

@[reducible, match_pattern, inline]

abbrev Core.Tree.Cat.DP : Cat

Equations

• Core.Tree.Cat.DP = Core.Tree.Cat.proj UD.UPOS.DET

@[reducible, match_pattern, inline]

abbrev Core.Tree.Cat.PP : Cat

Equations

• Core.Tree.Cat.PP = Core.Tree.Cat.proj UD.UPOS.ADP

@[reducible, match_pattern, inline]

abbrev Core.Tree.Cat.AdjP : Cat

Equations

• Core.Tree.Cat.AdjP = Core.Tree.Cat.proj UD.UPOS.ADJ

@[reducible, match_pattern, inline]

abbrev Core.Tree.Cat.AdvP : Cat

Equations

• Core.Tree.Cat.AdvP = Core.Tree.Cat.proj UD.UPOS.ADV

@[reducible, match_pattern, inline]

abbrev Core.Tree.Cat.ConjP : Cat

Equations

• Core.Tree.Cat.ConjP = Core.Tree.Cat.proj UD.UPOS.CCONJ

@[reducible, match_pattern, inline]

abbrev Core.Tree.Cat.NegP : Cat

Equations

• Core.Tree.Cat.NegP = Core.Tree.Cat.proj UD.UPOS.PART

@[reducible, match_pattern, inline]

abbrev Core.Tree.Cat.NumP : Cat

Equations

• Core.Tree.Cat.NumP = Core.Tree.Cat.proj UD.UPOS.NUM

inductive Core.Tree.Tree (C W : Type) : Type

Framework-neutral tree, parameterized by node label type C and terminal word type W.

• terminal c w — leaf carrying category c and word w
• node c cs — internal node with category c and children cs
• trace n c — movement trace with index n and category c
• bind n c body — λ-abstraction with index n, category c, scope body

The node constructor takes a List of children, subsuming both binary branching (for Heim & Kratzer composition) and n-ary structure (for Katzir's deletion operation). Binary nodes are node c [l, r].

trace and bind support Quantifier Raising and variable binding. Frameworks without movement (CCG, HPSG) simply never construct these.

For category-free trees (C = Unit), use the convenience constructors leaf, bin, un, tr, binder which hide the Unit parameter.

• terminal {C W : Type} : C → W → Tree C W
• node {C W : Type} : C → List (Tree C W) → Tree C W
• trace {C W : Type} : ℕ → C → Tree C W
• bind {C W : Type} : ℕ → C → Tree C W → Tree C W

@[implicit_reducible]

instance Core.Tree.instReprTree {C✝ W✝ : Type} [Repr C✝] [Repr W✝] : Repr (Tree C✝ W✝)

Equations

• Core.Tree.instReprTree = { reprPrec := Core.Tree.instReprTree.repr }

partial def Core.Tree.instReprTree.repr {C✝ W✝ : Type} [Repr C✝] [Repr W✝] : Tree C✝ W✝ → ℕ → Std.Format

@[reducible, match_pattern, inline]

abbrev Core.Tree.Tree.leaf {W : Type} (w : W) : Tree Unit W

Equations

• Core.Tree.Tree.leaf w = Core.Tree.Tree.terminal () w

@[reducible, match_pattern, inline]

abbrev Core.Tree.Tree.un {W : Type} (t : Tree Unit W) : Tree Unit W

Equations

• t.un = Core.Tree.Tree.node () [t]

@[reducible, match_pattern, inline]

abbrev Core.Tree.Tree.bin {W : Type} (t1 t2 : Tree Unit W) : Tree Unit W

Equations

• t1.bin t2 = Core.Tree.Tree.node () [t1, t2]

@[reducible, match_pattern, inline]

abbrev Core.Tree.Tree.tr {W : Type} (n : ℕ) : Tree Unit W

Equations

• Core.Tree.Tree.tr n = Core.Tree.Tree.trace n ()

@[reducible, match_pattern, inline]

abbrev Core.Tree.Tree.binder {W : Type} (n : ℕ) (body : Tree Unit W) : Tree Unit W

Equations

• Core.Tree.Tree.binder n body = Core.Tree.Tree.bind n () body

def Core.Tree.Tree.cat {C W : Type} : Tree C W → C

Category label of the root node. Total: every constructor carries a category (including bind, where it labels the result of PA).

Equations

• (Core.Tree.Tree.terminal a a_1).cat = a
• (Core.Tree.Tree.node a a_1).cat = a
• (Core.Tree.Tree.trace a a_1).cat = a_1
• (Core.Tree.Tree.bind a a_1 a_2).cat = a_1

def Core.Tree.Tree.beq {C W : Type} [BEq C] [BEq W] : Tree C W → Tree C W → Bool

Structural equality for trees (mutual recursion through List).

Equations

• (Core.Tree.Tree.terminal c₁ w₁).beq (Core.Tree.Tree.terminal c₂ w₂) = (c₁ == c₂ && w₁ == w₂)
• (Core.Tree.Tree.node c₁ cs₁).beq (Core.Tree.Tree.node c₂ cs₂) = (c₁ == c₂ && Core.Tree.Tree.beq.beqList cs₁ cs₂)
• (Core.Tree.Tree.trace n₁ c₁).beq (Core.Tree.Tree.trace n₂ c₂) = (n₁ == n₂ && c₁ == c₂)
• (Core.Tree.Tree.bind n₁ c₁ b₁).beq (Core.Tree.Tree.bind n₂ c₂ b₂) = (n₁ == n₂ && c₁ == c₂ && b₁.beq b₂)
• x✝¹.beq x✝ = false

def Core.Tree.Tree.beq.beqList {C W : Type} [BEq C] [BEq W] : List (Tree C W) → List (Tree C W) → Bool

Equations

• Core.Tree.Tree.beq.beqList [] [] = true
• Core.Tree.Tree.beq.beqList (a :: as) (b :: bs) = (a.beq b && Core.Tree.Tree.beq.beqList as bs)
• Core.Tree.Tree.beq.beqList a✝¹ a✝ = false

@[implicit_reducible]

instance Core.Tree.Tree.instBEq {C W : Type} [BEq C] [BEq W] : BEq (Tree C W)

Equations

• Core.Tree.Tree.instBEq = { beq := Core.Tree.Tree.beq }

def Core.Tree.Tree.decEq {C W : Type} [DecidableEq C] [DecidableEq W] (a b : Tree C W) : Decidable (a = b)

Decidable equality on Tree C W, mutually recursive with the list-of-trees case. Required because deriving DecidableEq does not handle the nested List (Tree C W) in node.

Equations

• One or more equations did not get rendered due to their size.
• (Core.Tree.Tree.terminal c₁ w₁).decEq (Core.Tree.Tree.terminal c₂ w₂) = if hc : c₁ = c₂ then if hw : w₁ = w₂ then isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• (Core.Tree.Tree.trace n₁ c₁).decEq (Core.Tree.Tree.trace n₂ c₂) = if hn : n₁ = n₂ then if hc : c₁ = c₂ then isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• (Core.Tree.Tree.terminal a a_1).decEq (Core.Tree.Tree.node a_2 a_3) = isFalse ⋯
• (Core.Tree.Tree.terminal a a_1).decEq (Core.Tree.Tree.trace a_2 a_3) = isFalse ⋯
• (Core.Tree.Tree.terminal a a_1).decEq (Core.Tree.Tree.bind a_2 a_3 a_4) = isFalse ⋯
• (Core.Tree.Tree.node a a_1).decEq (Core.Tree.Tree.terminal a_2 a_3) = isFalse ⋯
• (Core.Tree.Tree.node a a_1).decEq (Core.Tree.Tree.trace a_2 a_3) = isFalse ⋯
• (Core.Tree.Tree.node a a_1).decEq (Core.Tree.Tree.bind a_2 a_3 a_4) = isFalse ⋯
• (Core.Tree.Tree.trace a a_1).decEq (Core.Tree.Tree.terminal a_2 a_3) = isFalse ⋯
• (Core.Tree.Tree.trace a a_1).decEq (Core.Tree.Tree.node a_2 a_3) = isFalse ⋯
• (Core.Tree.Tree.trace a a_1).decEq (Core.Tree.Tree.bind a_2 a_3 a_4) = isFalse ⋯
• (Core.Tree.Tree.bind a a_1 a_2).decEq (Core.Tree.Tree.terminal a_3 a_4) = isFalse ⋯
• (Core.Tree.Tree.bind a a_1 a_2).decEq (Core.Tree.Tree.node a_3 a_4) = isFalse ⋯
• (Core.Tree.Tree.bind a a_1 a_2).decEq (Core.Tree.Tree.trace a_3 a_4) = isFalse ⋯

def Core.Tree.Tree.decEqList {C W : Type} [DecidableEq C] [DecidableEq W] (as bs : List (Tree C W)) : Decidable (as = bs)

Helper: decidable equality for list of trees.

Equations

• One or more equations did not get rendered due to their size.
• Core.Tree.Tree.decEqList [] [] = isTrue ⋯
• Core.Tree.Tree.decEqList [] (head :: tail) = isFalse ⋯
• Core.Tree.Tree.decEqList (head :: tail) [] = isFalse ⋯

@[implicit_reducible]

instance Core.Tree.Tree.instDecidableEq {C W : Type} [DecidableEq C] [DecidableEq W] : DecidableEq (Tree C W)

Equations

• Core.Tree.Tree.instDecidableEq = Core.Tree.Tree.decEq

def Core.Tree.Tree.size {C W : Type} : Tree C W → ℕ

Number of nodes in the tree.

Equations

• (Core.Tree.Tree.terminal a a_1).size = 1
• (Core.Tree.Tree.node a a_1).size = 1 + Core.Tree.Tree.size.sizeList a_1
• (Core.Tree.Tree.trace a a_1).size = 1
• (Core.Tree.Tree.bind a a_1 a_2).size = 1 + a_2.size

def Core.Tree.Tree.size.sizeList {C W : Type} : List (Tree C W) → ℕ

Equations

• Core.Tree.Tree.size.sizeList [] = 0
• Core.Tree.Tree.size.sizeList (t :: ts) = t.size + Core.Tree.Tree.size.sizeList ts

def Core.Tree.Tree.leafCount {C W : Type} : Tree C W → ℕ

Number of word-bearing terminals (leaves) in the tree. Traces and binders contribute 0; internal nodes recurse.

Equations

• (Core.Tree.Tree.terminal a a_1).leafCount = 1
• (Core.Tree.Tree.node a a_1).leafCount = Core.Tree.Tree.leafCount.leafCountList a_1
• (Core.Tree.Tree.trace a a_1).leafCount = 0
• (Core.Tree.Tree.bind a a_1 a_2).leafCount = a_2.leafCount

def Core.Tree.Tree.leafCount.leafCountList {C W : Type} : List (Tree C W) → ℕ

Equations

• Core.Tree.Tree.leafCount.leafCountList [] = 0
• Core.Tree.Tree.leafCount.leafCountList (t :: ts) = t.leafCount + Core.Tree.Tree.leafCount.leafCountList ts

@[irreducible]

def Core.Tree.Tree.binRec {W : Type} {motive : Tree Unit W → Sort u_1} (term : (w : W) → motive (terminal () w)) (binNode : (l r : Tree Unit W) → motive l → motive r → motive (node () [l, r])) (tr : (n : ℕ) → motive (trace n ())) (bd : (n : ℕ) → (body : Tree Unit W) → motive body → motive (bind n () body)) (nilNode : motive (node () [])) (singletonNode : (c : Tree Unit W) → motive (node () [c])) (manyNode : (c1 c2 c3 : Tree Unit W) → (cs : List (Tree Unit W)) → motive (node () (c1 :: c2 :: c3 :: cs))) (t : Tree Unit W) : motive t

Custom recursor for binary trees over Tree Unit W. The default induction tactic refuses nested inductives like Tree; this recursor expands the node-case enumeration so each non-binary arity (0, 1, ≥3 children) gets its own branch, separate from the binary binNode case that carries inductive hypotheses. With @[elab_as_elim], used as induction t using Tree.binRec with | term … | binNode … | tr … | bd … | nilNode | singletonNode … | manyNode ….

Equations

• One or more equations did not get rendered due to their size.
• Core.Tree.Tree.binRec term binNode tr bd nilNode singletonNode manyNode (Core.Tree.Tree.terminal PUnit.unit w) = term w
• Core.Tree.Tree.binRec term binNode tr bd nilNode singletonNode manyNode (Core.Tree.Tree.node PUnit.unit []) = nilNode
• Core.Tree.Tree.binRec term binNode tr bd nilNode singletonNode manyNode (Core.Tree.Tree.node PUnit.unit [c]) = singletonNode c
• Core.Tree.Tree.binRec term binNode tr bd nilNode singletonNode manyNode (Core.Tree.Tree.node PUnit.unit (c1 :: c2 :: c3 :: cs)) = manyNode c1 c2 c3 cs
• Core.Tree.Tree.binRec term binNode tr bd nilNode singletonNode manyNode (Core.Tree.Tree.trace n PUnit.unit) = tr n

def Core.Tree.Tree.subtrees {C W : Type} : Tree C W → List (Tree C W)

All subtrees including self (pre-order traversal).

Equations

• (Core.Tree.Tree.terminal a a_1).subtrees = [Core.Tree.Tree.terminal a a_1]
• (Core.Tree.Tree.node a cs).subtrees = Core.Tree.Tree.node a cs :: Core.Tree.Tree.subtrees.subtreesList cs
• (Core.Tree.Tree.trace a a_1).subtrees = [Core.Tree.Tree.trace a a_1]
• (Core.Tree.Tree.bind a a_1 body).subtrees = Core.Tree.Tree.bind a a_1 body :: body.subtrees

def Core.Tree.Tree.subtrees.subtreesList {C W : Type} : List (Tree C W) → List (Tree C W)

Equations

• Core.Tree.Tree.subtrees.subtreesList [] = []
• Core.Tree.Tree.subtrees.subtreesList (t :: ts) = t.subtrees ++ Core.Tree.Tree.subtrees.subtreesList ts

def Core.Tree.Tree.containsCat {C W : Type} [BEq C] (target : C) : Tree C W → Bool

Whether a category appears anywhere in the tree.

Equations

• Core.Tree.Tree.containsCat target (Core.Tree.Tree.terminal a a_1) = (target == a)
• Core.Tree.Tree.containsCat target (Core.Tree.Tree.node a a_1) = (target == a || Core.Tree.Tree.containsCat.containsCatList target a_1)
• Core.Tree.Tree.containsCat target (Core.Tree.Tree.trace a a_1) = (target == a_1)
• Core.Tree.Tree.containsCat target (Core.Tree.Tree.bind a a_1 a_2) = (target == a_1 || Core.Tree.Tree.containsCat target a_2)

def Core.Tree.Tree.containsCat.containsCatList {C W : Type} [BEq C] (target : C) : List (Tree C W) → Bool

Equations

• Core.Tree.Tree.containsCat.containsCatList target [] = false
• Core.Tree.Tree.containsCat.containsCatList target (t :: ts) = (Core.Tree.Tree.containsCat target t || Core.Tree.Tree.containsCat.containsCatList target ts)

def Core.Tree.Tree.leafSubst {C W : Type} [BEq C] [BEq W] (target replacement : W) (c : C) : Tree C W → Tree C W

Substitute all terminals of category c carrying word target with replacement. This is the most common structural operation: replacing one scalar item with another of the same category.

Equations

• Core.Tree.Tree.leafSubst target replacement c (Core.Tree.Tree.terminal a a_1) = if (c == a && a_1 == target) = true then Core.Tree.Tree.terminal a replacement else Core.Tree.Tree.terminal a a_1
• Core.Tree.Tree.leafSubst target replacement c (Core.Tree.Tree.node a a_1) = Core.Tree.Tree.node a (Core.Tree.Tree.leafSubst.leafSubstList target replacement c a_1)
• Core.Tree.Tree.leafSubst target replacement c (Core.Tree.Tree.trace a a_1) = Core.Tree.Tree.trace a a_1
• Core.Tree.Tree.leafSubst target replacement c (Core.Tree.Tree.bind a a_1 a_2) = Core.Tree.Tree.bind a a_1 (Core.Tree.Tree.leafSubst target replacement c a_2)

def Core.Tree.Tree.leafSubst.leafSubstList {C W : Type} [BEq C] [BEq W] (target replacement : W) (c : C) : List (Tree C W) → List (Tree C W)

Equations

• Core.Tree.Tree.leafSubst.leafSubstList target replacement c [] = []
• Core.Tree.Tree.leafSubst.leafSubstList target replacement c (t :: ts) = Core.Tree.Tree.leafSubst target replacement c t :: Core.Tree.Tree.leafSubst.leafSubstList target replacement c ts

structure Core.Tree.TreePath : Type

A path from the root of a tree, encoded as a list of child indices.

Each element is the index in the parent's child list (or 0 for the unique child of a bind). The empty path identifies the root.

• toList : List ℕ

  The underlying list of child indices.

@[implicit_reducible]

instance Core.Tree.TreePath.instLE : LE TreePath

Dominance order: p ≤ q iff p is a prefix of q.

Equations

• Core.Tree.TreePath.instLE = { le := fun (p q : Core.Tree.TreePath) => p.toList <+: q.toList }

@[implicit_reducible]

instance Core.Tree.TreePath.instPartialOrder : PartialOrder TreePath

Equations

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

theorem Core.Tree.TreePath.prefix_or_prefix {p q r : TreePath} (hp : p ≤ r) (hq : q ≤ r) : p ≤ q ∨ q ≤ p

Two prefixes of the same list are comparable. This is the Connected Ancestor Condition (CAC) for the prefix order.

def Core.Tree.Tree.subtreeAt {C W : Type} : Tree C W → List ℕ → Option (Tree C W)

Subtree at the given path; none if the path leaves the tree.

For node c cs, the next index i selects child cs[i]?; for bind, only index 0 is valid (binders have a single body).

Equations

• x✝.subtreeAt [] = some x✝
• (Core.Tree.Tree.node a cs).subtreeAt (i :: rest) = cs[i]?.bind fun (child : Core.Tree.Tree C W) => child.subtreeAt rest
• (Core.Tree.Tree.bind a a_1 body).subtreeAt (0 :: rest) = body.subtreeAt rest
• (Core.Tree.Tree.bind a a_1 a_2).subtreeAt (head :: tail) = none
• (Core.Tree.Tree.terminal a a_1).subtreeAt (head :: tail) = none
• (Core.Tree.Tree.trace a a_1).subtreeAt (head :: tail) = none

def Core.Tree.Tree.validPaths {C W : Type} (t : Tree C W) : Set TreePath

Set of valid paths in the tree (paths that resolve to a subtree).

Equations

• t.validPaths = {p : Core.Tree.TreePath | (t.subtreeAt p.toList).isSome = true}

theorem Core.Tree.Tree.nil_validPath {C W : Type} (t : Tree C W) : { toList := [] } ∈ t.validPaths

def Core.Tree.Tree.toTreeOrder {C W : Type} (t : Tree C W) : Order.TreeOrder TreePath

Forgetful map from a Tree C W to its dominance order as a TreeOrder TreePath. This makes the framework-agnostic command- relation library (@cite{barker-pullum-1990}, B&P) directly applicable to any concrete tree, regardless of category or word type.

Equations

• t.toTreeOrder = { nodes := t.validPaths, root := { toList := [] }, root_in_nodes := ⋯, root_le_all := ⋯, ancestor_connected := ⋯ }

def FreeMagma.toTree {α : Type} : FreeMagma α → Core.Tree.Tree Unit α

Forgetful map from a free magma to a binary Core.Tree.Tree Unit α.

The image lives in a strict subset of Tree Unit α: only .terminal () (from .of) and the binary .node () [_, _] (from .mul) are produced; the n-ary .node, .trace, and .bind constructors are never used.

By composition with Core.Tree.Tree.toTreeOrder, every FreeMagma α inherits a Core.Order.TreeOrder Core.Tree.TreePath, making B&P's framework-agnostic command-relation library (Linglib.Core.Order.Command) directly applicable.

Universe note: capped at α : Type because Core.Tree.Tree is monomorphic in Type 0; sufficient for LIToken-indexed SyntacticObject.

Equations

• (FreeMagma.of a).toTree = Core.Tree.Tree.terminal () a
• (l.mul r).toTree = Core.Tree.Tree.node () [l.toTree, r.toTree]