Constituency Trees

The constituency tree and LF interface format of the Syntax layer: one tree type, parameterized by node labels (C) and terminal content (W), shared by the frameworks whose structures are constituency trees — not by all of syntax. The library has two structural hubs:

1. Syntax.Tree (this file) — for constituency: H&K composition reads it (LF), Katzir structural operations transform it (PF), Minimalist derivations project down to it at Spell-Out.
2. Core.Order.TreeOrder + the B&P command library — the genuinely framework-agnostic layer, where non-constituency frameworks connect via their own node types (HPSG signs, DG word-indices, Minimalist syntactic objects), each with its own dominance order.

Frameworks whose structures are not trees do not and cannot instantiate this type: CCG derivations are proof trees (nodes are rule applications); HPSG signs are reentrant feature structures (structure sharing has no tree representation); dependency structures are head-indexed graphs; multidominance objects are nonplanar (which is why Syntax/Minimalist/ keeps its own SyntacticObject and only projects to Tree at the interface).

Syntax.Tree C W

N-ary branching with categories on every node. Read by both interfaces:

• Compositional interpretation (LF): interp/evalTree in Semantics/Composition/Tree.lean — type-driven, ignores categories
• Structural operations (PF): [Kat07] StructOp (substitution, deletion, contraction) in Semantics/Alternatives/Structural.lean — category-aware

The generic core is terminal/node with the pluggable category parameter C (UD tags, feature bundles, Unit for unlabeled, ...). The trace and bind constructors encode the trace-theoretic / QR analysis of movement specifically ([HK98] Ch. 5): indexed traces plus λ-binders. Rival representations of movement are not expressible on this type — copy theory needs a side-car chain relation over TreePaths, and multidominance needs the nonplanar SyntacticObject (Syntax/Minimalist/Multidominance.lean). Frameworks without movement simply never construct these cases. Binder–trace well-formedness (each bind n binding a matching trace n) is a predicate to be imposed, not a type guarantee; bind's category label is recorded for uniformity but is not consulted by interp or StructOp.

Instantiations

• Tree Unit String — category-free, for H&K composition. Use convenience constructors .leaf, .bin, .un, .tr, .binder.
• Tree Cat String — UD-grounded categories (Syntax/Tree/Cat.lean), for Katzir structural alternatives.
• Tree Unit LIToken — bare phrase structure projected from Minimalist syntax at Spell-Out via FreeMagma.toTree (categories inside the token, not on nodes).

Positions and dominance

Tree is an instance of Core.Order.Branching (the rose-tree interface), so all position machinery is inherited rather than re-stipulated: Gorn addresses (Core.Order.TreePath), the dominance order with mathlib's rooted-tree stack (root ⊥, parent Order.pred, least common ancestor ⊓), and the forgetful map Core.Order.Branching.toTreeOrder into the B&P command-relation library (Linglib.Core.Order.Command, [BP90]).

The tree type

inductive Syntax.Tree (C : Type u_1) (W : Type u_2) : Type (max u_1 u_2)

Constituency 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 : Type u_1} {W : Type u_2} : C → W → Tree C W
• node {C : Type u_1} {W : Type u_2} : C → List (Tree C W) → Tree C W
• trace {C : Type u_1} {W : Type u_2} : ℕ → C → Tree C W
• bind {C : Type u_1} {W : Type u_2} : ℕ → C → Tree C W → Tree C W

@[implicit_reducible]

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

Equations

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

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

@[reducible, match_pattern, inline]

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

Equations

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

@[reducible, match_pattern, inline]

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

Equations

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

@[reducible, match_pattern, inline]

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

Equations

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

@[reducible, match_pattern, inline]

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

Equations

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

@[reducible, match_pattern, inline]

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

Equations

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

Basic accessors

def Syntax.Tree.cat {C : Type u_1} {W : Type u_2} : 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

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

Decidable equality

DecidableEq is the single source of truth for tree equality; BEq and LawfulBEq (Tree C W) come for free (and coherently) from the global instBEqOfDecidableEq. A hand-rolled beq/BEq instance used to shadow this — it left LawfulBEq (Tree C W) unsynthesizable and was a second, unproven-coherent notion of tree equality, so it was removed.

def Syntax.Tree.decEq {C : Type u_1} {W : Type u_2} [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.
• (Syntax.Tree.terminal c₁ w₁).decEq (Syntax.Tree.terminal c₂ w₂) = if hc : c₁ = c₂ then if hw : w₁ = w₂ then isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• (Syntax.Tree.trace n₁ c₁).decEq (Syntax.Tree.trace n₂ c₂) = if hn : n₁ = n₂ then if hc : c₁ = c₂ then isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• (Syntax.Tree.terminal a a_1).decEq (Syntax.Tree.node a_2 a_3) = isFalse ⋯
• (Syntax.Tree.terminal a a_1).decEq (Syntax.Tree.trace a_2 a_3) = isFalse ⋯
• (Syntax.Tree.terminal a a_1).decEq (Syntax.Tree.bind a_2 a_3 a_4) = isFalse ⋯
• (Syntax.Tree.node a a_1).decEq (Syntax.Tree.terminal a_2 a_3) = isFalse ⋯
• (Syntax.Tree.node a a_1).decEq (Syntax.Tree.trace a_2 a_3) = isFalse ⋯
• (Syntax.Tree.node a a_1).decEq (Syntax.Tree.bind a_2 a_3 a_4) = isFalse ⋯
• (Syntax.Tree.trace a a_1).decEq (Syntax.Tree.terminal a_2 a_3) = isFalse ⋯
• (Syntax.Tree.trace a a_1).decEq (Syntax.Tree.node a_2 a_3) = isFalse ⋯
• (Syntax.Tree.trace a a_1).decEq (Syntax.Tree.bind a_2 a_3 a_4) = isFalse ⋯
• (Syntax.Tree.bind a a_1 a_2).decEq (Syntax.Tree.terminal a_3 a_4) = isFalse ⋯
• (Syntax.Tree.bind a a_1 a_2).decEq (Syntax.Tree.node a_3 a_4) = isFalse ⋯
• (Syntax.Tree.bind a a_1 a_2).decEq (Syntax.Tree.trace a_3 a_4) = isFalse ⋯

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

Helper: decidable equality for list of trees.

Equations

• Syntax.Tree.decEqList [] [] = isTrue ⋯
• Syntax.Tree.decEqList [] (head :: tail) = isFalse ⋯
• Syntax.Tree.decEqList (head :: tail) [] = isFalse ⋯
• Syntax.Tree.decEqList (a :: as) (b :: bs) = match a.decEq b, Syntax.Tree.decEqList as bs with | isTrue ha, isTrue has => isTrue ⋯ | isFalse ha, x => isFalse ⋯ | x, isFalse has => isFalse ⋯

@[implicit_reducible]

instance Syntax.Tree.instDecidableEq {C : Type u_1} {W : Type u_2} [DecidableEq C] [DecidableEq W] : DecidableEq (Tree C W)

Equations

• Syntax.Tree.instDecidableEq = Syntax.Tree.decEq

Size

def Syntax.Tree.size {C : Type u_1} {W : Type u_2} : Tree C W → ℕ

Number of nodes in the tree.

Equations

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

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

Equations

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

def Syntax.Tree.leafCount {C : Type u_1} {W : Type u_2} : Tree C W → ℕ

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

Equations

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

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

Equations

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

Induction principle

@[irreducible]

def Syntax.Tree.recAux {C : Type u_1} {W : Type u_2} {motive : Tree C W → Sort u_3} (terminal : (c : C) → (w : W) → motive (terminal c w)) (node : (c : C) → (cs : List (Tree C W)) → ((t : Tree C W) → t ∈ cs → motive t) → motive (node c cs)) (trace : (n : ℕ) → (c : C) → motive (trace n c)) (bind : (n : ℕ) → (c : C) → (b : Tree C W) → motive b → motive (bind n c b)) (t : Tree C W) : motive t

Membership-based recursor/induction principle for Tree. The default induction tactic refuses nested inductives, and the raw two-motive Tree.rec forces a parallel List motive; this principle hands the node case the hypothesis proofs actually want — ∀ t ∈ cs, motive t — so structural inductions read directly. With @[elab_as_elim], used as induction t using Tree.recAux with | terminal … | node c cs ih | trace … | bind ….

Equations

• Syntax.Tree.recAux terminal node trace bind (Syntax.Tree.terminal a a_1) = terminal a a_1
• Syntax.Tree.recAux terminal node trace bind (Syntax.Tree.node a a_1) = node a a_1 fun (t : Syntax.Tree C W) (x : t ∈ a_1) => Syntax.Tree.recAux terminal node trace bind t
• Syntax.Tree.recAux terminal node trace bind (Syntax.Tree.trace a a_1) = trace a a_1
• Syntax.Tree.recAux terminal node trace bind (Syntax.Tree.bind a a_1 a_2) = bind a a_1 a_2 (Syntax.Tree.recAux terminal node trace bind a_2)

Subtrees

def Syntax.Tree.subtrees {C : Type u_1} {W : Type u_2} : Tree C W → List (Tree C W)

All subtrees including self (pre-order traversal).

Equations

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

def Syntax.Tree.subtrees.subtreesList {C : Type u_1} {W : Type u_2} : List (Tree C W) → List (Tree C W)

Equations

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

theorem Syntax.Tree.subtreesList_eq_flatMap {C : Type u_1} {W : Type u_2} (cs : List (Tree C W)) : subtrees.subtreesList cs = List.flatMap subtrees cs

theorem Syntax.Tree.subtrees_node {C : Type u_1} {W : Type u_2} (cat : C) (cs : List (Tree C W)) : (node cat cs).subtrees = node cat cs :: List.flatMap subtrees cs

Category queries

def Syntax.Tree.ContainsCat {C : Type u_1} {W : Type u_2} [DecidableEq C] (target : C) (t : Tree C W) : Prop

ContainsCat target t holds when category target appears on some subtree of t. A Prop predicate (with a kernel-reducible Decidable instance from List membership, so decide closes concrete goals) over the file's own structurally-recursive subtrees — not a Bool function.

Equations

• Syntax.Tree.ContainsCat target t = (target ∈ List.map Syntax.Tree.cat t.subtrees)

@[implicit_reducible]

instance Syntax.Tree.instDecidableContainsCat {C : Type u_1} {W : Type u_2} [DecidableEq C] (target : C) (t : Tree C W) : Decidable (ContainsCat target t)

Equations

• Syntax.Tree.instDecidableContainsCat target t = Syntax.Tree.instDecidableContainsCat._aux_1 target t

theorem Syntax.Tree.containsCat_node_iff {C : Type u_1} {W : Type u_2} [DecidableEq C] (target cat : C) (cs : List (Tree C W)) : ContainsCat target (node cat cs) ↔ target = cat ∨ ∃ t ∈ cs, ContainsCat target t

ContainsCat at a node: it is the node's own category, or appears in some child.

theorem Syntax.Tree.containsCat_bind_iff {C : Type u_1} {W : Type u_2} [DecidableEq C] (target c : C) (n : ℕ) (body : Tree C W) : ContainsCat target (bind n c body) ↔ target = c ∨ ContainsCat target body

ContainsCat at a binder: the binder's category, or inside the body.

Leaf substitution

def Syntax.Tree.leafSubst {C : Type u_1} {W : Type u_2} [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

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

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

Equations

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

Branching instance: positions, dominance, command relations

The path machinery (Gorn addresses, Core.Order.TreePath, the dominance order, the B&P command-relation bridge) is generic over Core.Order.Branching; Tree participates through the instance below. Branching.subtreeAt at this instance behaves as before: for node c cs the next index selects cs[i]?; for bind only index 0 is valid (binders have a single body); terminals and traces have no children. Positions inherit mathlib's rooted-tree order stack from TreePath: root ⊥, parent Order.pred, least common ancestor ⊓.

@[implicit_reducible]

instance Syntax.instBranchingTree {C : Type u_1} {W : Type u_2} : Core.Order.Branching (Tree C W)

Equations

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

instance Syntax.instIsFiniteBranchingTree {C : Type u_1} {W : Type u_2} : Core.Order.IsFiniteBranching (Tree C W)

Children strictly decrease the sizeOf measure, unlocking the generic recursion API (Branching.size, subtrees, yield, inductionOn). noncomputable because the measure field stores sizeOf, whose nested-List IR the LCNF boxing pass cannot compile; the measure is only a termination witness, and yield/size reduce symbolically via their _def lemmas.

@[implicit_reducible]

instance Syntax.instHasContentTree {C : Type u_1} {W : Type u_2} : Core.Order.HasContent (Tree C W) W

Terminal content: the word at a terminal; traces, binders, and internal nodes are contentless, so Branching.yield computes the frontier string.

Equations

• Syntax.instHasContentTree = { content? := fun (x : Syntax.Tree C W) => match x with | Syntax.Tree.terminal a w => some w | x => none }

Branching.yield-instance simp lemmas

Make the generic Branching.yield reduce by simp/decide at concrete Tree constructors — the prerequisite for consumers (Studies files) to replace bespoke yield computations with the generic API.

@[simp]

theorem Syntax.branching_content_terminal {C : Type u_1} {W : Type u_2} (c : C) (w : W) : Core.Order.content? (Tree.terminal c w) = some w

@[simp]

theorem Syntax.branching_content_node {C : Type u_1} {W : Type u_2} (c : C) (cs : List (Tree C W)) : Core.Order.content? (Tree.node c cs) = none

@[simp]

theorem Syntax.branching_content_trace {C : Type u_1} {W : Type u_2} (n : ℕ) (c : C) : Core.Order.content? (Tree.trace n c) = none

@[simp]

theorem Syntax.branching_content_bind {C : Type u_1} {W : Type u_2} (n : ℕ) (c : C) (body : Tree C W) : Core.Order.content? (Tree.bind n c body) = none

@[simp]

theorem Syntax.branching_yield_terminal {C : Type u_1} {W : Type u_2} (c : C) (w : W) : Core.Order.Branching.yield (Tree.terminal c w) = [w]

@[simp]

theorem Syntax.branching_yield_node {C : Type u_1} {W : Type u_2} (c : C) (cs : List (Tree C W)) : Core.Order.Branching.yield (Tree.node c cs) = List.flatMap Core.Order.Branching.yield cs

@[simp]

theorem Syntax.branching_yield_trace {C : Type u_1} {W : Type u_2} (n : ℕ) (c : C) : Core.Order.Branching.yield (Tree.trace n c) = []

@[simp]

theorem Syntax.branching_yield_bind {C : Type u_1} {W : Type u_2} (n : ℕ) (c : C) (body : Tree C W) : Core.Order.Branching.yield (Tree.bind n c body) = Core.Order.Branching.yield body

FreeMagma → Tree forgetful map

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

Forgetful map from a free magma to a binary Syntax.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.Order.Branching.toTreeOrder, every FreeMagma α inherits a Core.Order.TreeOrder Core.Order.TreePath, making B&P's framework-agnostic command-relation library (Linglib.Core.Order.Command) directly applicable.

Universe-polymorphic in α, matching Syntax.Tree.

Equations

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