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.

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

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 ⋯

instance Core.Tree.instReprCat : Repr Cat

Equations

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

def Core.Tree.instReprCat.repr : Cat → Nat → 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✝

instance Core.Tree.instInhabitedCat : Inhabited Cat

Equations

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

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} : Nat → C → Tree C W
• bind {C W : Type} : Nat → C → Tree C W → Tree C W

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

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

Equations

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

@[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 : Nat) : 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 : Nat) (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 x✝¹ x✝ = false

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.size {C W : Type} : Tree C W → Nat

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) → Nat

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.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