Constituency trees

A constituency tree over a category type C and a word type W is a rose tree whose nodes carry labels: a terminal carries a category and a word, an internal node a category, the mother of an adjunction a category too, marking it a further segment of its host's category rather than a projection above it, and the two nodes of Heim and Kratzer's trace theory of movement, an indexed trace and an indexed binder over a body, carry a category each. Type-driven interpretation reads the tree with C = Unit; structural operations on parse trees read it with a category system such as PhraseStructure.Cat. Positions, subtrees, replacement and the frontier are those of the rose tree.

Main declarations

• PhraseStructure.Tree.Label, PhraseStructure.Tree: the node labels and the trees over them, with the pattern-matchable constructors terminal, node, adjoin, trace, bind and the category-free leaf, bin, tr, binder.
• PhraseStructure.Tree.Label.Licenses, PhraseStructure.Tree.IsWellFormed: terminals and traces are leaves and binders have one body.
• PhraseStructure.Tree.rec': induction over the five shapes, with a case for ill-formed nodes.
• PhraseStructure.Tree.terminals, yield, cats, map, freeIndices, leafSubst.
• PhraseStructure.Tree.positionedTerminals: the terminals with their positions, in the order of the yield, which is precedence (pairwise_precedes_positionedTerminals).

Implementation notes

Daughters are a List, so a node is binary or n-ary by its list and sibling order is linear precedence. Only the trace theory of movement is expressible: a copy or a multidominance representation is not a tree over these labels. Ill-formed label and arity combinations, such as a terminal with daughters, are expressible; IsWellFormed excludes them where a theorem needs it, and the interpreter denotes them none. The mark on the mother of an adjunction follows May's and Chomsky's segment theory, in which adjunction extends its host's category rather than projecting a new one, and bare phrase structure labels the adjunction structure apart from a projection. That each binder binds a trace of its index is a property of a tree, not a guarantee of the type, and interpretation does not read the category on a binder.

Tree C W abbreviates RoseTree (Label C W), so the rose tree's navigation (children, subtreeAt) returns RoseTree (Label C W). Dot notation for this file's operations does not resolve on those results, so write Tree.cat s, and write constructor patterns on them as Tree.node: an anonymous .node would elaborate as RoseTree.node, which matches any label.

References

• [HK98]
• [Kat07]
• [BP90]
• [May85]
• [Cho95b]

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

A node of a constituency tree carries a terminal's category and word, an internal node's category, the category of an adjunction structure, or a trace's or binder's index and category.

• terminal {C : Type u_1} {W : Type u_2} : C → W → Label C W
• node {C : Type u_1} {W : Type u_2} : C → Label C W
• segment {C : Type u_1} {W : Type u_2} : C → Label C W

  segment c labels the mother of an adjunction, a segment of the category c of its host daughter, not a projection above it.

• trace {C : Type u_1} {W : Type u_2} : ℕ → C → Label C W
• bind {C : Type u_1} {W : Type u_2} : ℕ → C → Label C W

def PhraseStructure.Tree.instDecidableEqLabel.decEq {C✝ : Type u_1} {W✝ : Type u_2} [DecidableEq C✝] [DecidableEq W✝] (x✝ x✝¹ : Label C✝ W✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• PhraseStructure.Tree.instDecidableEqLabel.decEq (PhraseStructure.Tree.Label.terminal a a_1) (PhraseStructure.Tree.Label.node a_2) = isFalse ⋯
• PhraseStructure.Tree.instDecidableEqLabel.decEq (PhraseStructure.Tree.Label.terminal a a_1) (PhraseStructure.Tree.Label.segment a_2) = isFalse ⋯
• PhraseStructure.Tree.instDecidableEqLabel.decEq (PhraseStructure.Tree.Label.terminal a a_1) (PhraseStructure.Tree.Label.trace a_2 a_3) = isFalse ⋯
• PhraseStructure.Tree.instDecidableEqLabel.decEq (PhraseStructure.Tree.Label.terminal a a_1) (PhraseStructure.Tree.Label.bind a_2 a_3) = isFalse ⋯
• PhraseStructure.Tree.instDecidableEqLabel.decEq (PhraseStructure.Tree.Label.node a) (PhraseStructure.Tree.Label.terminal a_1 a_2) = isFalse ⋯
• PhraseStructure.Tree.instDecidableEqLabel.decEq (PhraseStructure.Tree.Label.node a) (PhraseStructure.Tree.Label.node b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• PhraseStructure.Tree.instDecidableEqLabel.decEq (PhraseStructure.Tree.Label.node a) (PhraseStructure.Tree.Label.segment a_1) = isFalse ⋯
• PhraseStructure.Tree.instDecidableEqLabel.decEq (PhraseStructure.Tree.Label.node a) (PhraseStructure.Tree.Label.trace a_1 a_2) = isFalse ⋯
• PhraseStructure.Tree.instDecidableEqLabel.decEq (PhraseStructure.Tree.Label.node a) (PhraseStructure.Tree.Label.bind a_1 a_2) = isFalse ⋯
• PhraseStructure.Tree.instDecidableEqLabel.decEq (PhraseStructure.Tree.Label.segment a) (PhraseStructure.Tree.Label.terminal a_1 a_2) = isFalse ⋯
• PhraseStructure.Tree.instDecidableEqLabel.decEq (PhraseStructure.Tree.Label.segment a) (PhraseStructure.Tree.Label.node a_1) = isFalse ⋯
• PhraseStructure.Tree.instDecidableEqLabel.decEq (PhraseStructure.Tree.Label.segment a) (PhraseStructure.Tree.Label.segment b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• PhraseStructure.Tree.instDecidableEqLabel.decEq (PhraseStructure.Tree.Label.segment a) (PhraseStructure.Tree.Label.trace a_1 a_2) = isFalse ⋯
• PhraseStructure.Tree.instDecidableEqLabel.decEq (PhraseStructure.Tree.Label.segment a) (PhraseStructure.Tree.Label.bind a_1 a_2) = isFalse ⋯
• PhraseStructure.Tree.instDecidableEqLabel.decEq (PhraseStructure.Tree.Label.trace a a_1) (PhraseStructure.Tree.Label.terminal a_2 a_3) = isFalse ⋯
• PhraseStructure.Tree.instDecidableEqLabel.decEq (PhraseStructure.Tree.Label.trace a a_1) (PhraseStructure.Tree.Label.node a_2) = isFalse ⋯
• PhraseStructure.Tree.instDecidableEqLabel.decEq (PhraseStructure.Tree.Label.trace a a_1) (PhraseStructure.Tree.Label.segment a_2) = isFalse ⋯
• PhraseStructure.Tree.instDecidableEqLabel.decEq (PhraseStructure.Tree.Label.trace a a_1) (PhraseStructure.Tree.Label.bind a_2 a_3) = isFalse ⋯
• PhraseStructure.Tree.instDecidableEqLabel.decEq (PhraseStructure.Tree.Label.bind a a_1) (PhraseStructure.Tree.Label.terminal a_2 a_3) = isFalse ⋯
• PhraseStructure.Tree.instDecidableEqLabel.decEq (PhraseStructure.Tree.Label.bind a a_1) (PhraseStructure.Tree.Label.node a_2) = isFalse ⋯
• PhraseStructure.Tree.instDecidableEqLabel.decEq (PhraseStructure.Tree.Label.bind a a_1) (PhraseStructure.Tree.Label.segment a_2) = isFalse ⋯
• PhraseStructure.Tree.instDecidableEqLabel.decEq (PhraseStructure.Tree.Label.bind a a_1) (PhraseStructure.Tree.Label.trace a_2 a_3) = isFalse ⋯

@[instance_reducible]

instance PhraseStructure.Tree.instDecidableEqLabel {C✝ : Type u_1} {W✝ : Type u_2} [DecidableEq C✝] [DecidableEq W✝] : DecidableEq (Label C✝ W✝)

Equations

• PhraseStructure.Tree.instDecidableEqLabel = PhraseStructure.Tree.instDecidableEqLabel.decEq

@[instance_reducible]

instance PhraseStructure.Tree.instReprLabel {C✝ : Type u_1} {W✝ : Type u_2} [Repr C✝] [Repr W✝] : Repr (Label C✝ W✝)

Equations

• PhraseStructure.Tree.instReprLabel = { reprPrec := PhraseStructure.Tree.instReprLabel.repr }

def PhraseStructure.Tree.instReprLabel.repr {C✝ : Type u_1} {W✝ : Type u_2} [Repr C✝] [Repr W✝] : Label C✝ W✝ → ℕ → Std.Format

Equations

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

def PhraseStructure.Tree.Label.cat {C : Type u_1} {W : Type u_2} : Label C W → C

The category a label carries.

Equations

• (PhraseStructure.Tree.Label.terminal c a).cat = c
• (PhraseStructure.Tree.Label.node c).cat = c
• (PhraseStructure.Tree.Label.segment c).cat = c
• (PhraseStructure.Tree.Label.trace a c).cat = c
• (PhraseStructure.Tree.Label.bind a c).cat = c

def PhraseStructure.Tree.Label.terminal? {C : Type u_1} {W : Type u_2} : Label C W → Option (C × W)

A terminal label carries a category and a word; other labels carry none.

Equations

• (PhraseStructure.Tree.Label.terminal c w).terminal? = some (c, w)
• x✝.terminal? = none

def PhraseStructure.Tree.Label.mapWord {C : Type u_1} {W : Type u_2} {W' : Type u_3} (f : W → W') : Label C W → Label C W'

mapWord f relabels the word of a terminal label.

Equations

• PhraseStructure.Tree.Label.mapWord f (PhraseStructure.Tree.Label.terminal c a) = PhraseStructure.Tree.Label.terminal c (f a)
• PhraseStructure.Tree.Label.mapWord f (PhraseStructure.Tree.Label.node c) = PhraseStructure.Tree.Label.node c
• PhraseStructure.Tree.Label.mapWord f (PhraseStructure.Tree.Label.segment c) = PhraseStructure.Tree.Label.segment c
• PhraseStructure.Tree.Label.mapWord f (PhraseStructure.Tree.Label.trace a c) = PhraseStructure.Tree.Label.trace a c
• PhraseStructure.Tree.Label.mapWord f (PhraseStructure.Tree.Label.bind a c) = PhraseStructure.Tree.Label.bind a c

@[simp]

theorem PhraseStructure.Tree.Label.cat_mapWord {C : Type u_1} {W : Type u_2} {W' : Type u_3} (f : W → W') (l : Label C W) : (mapWord f l).cat = l.cat

@[simp]

theorem PhraseStructure.Tree.Label.mapWord_id {C : Type u_1} {W : Type u_2} (l : Label C W) : mapWord id l = l

@[simp]

theorem PhraseStructure.Tree.Label.mapWord_mapWord {C : Type u_1} {W : Type u_2} {W' : Type u_3} {W'' : Type u_4} (g : W' → W'') (f : W → W') (l : Label C W) : mapWord g (mapWord f l) = mapWord (g ∘ f) l

def PhraseStructure.Tree.Label.Licenses {C : Type u_1} {W : Type u_2} : Label C W → List (Label C W) → Prop

A label licenses its daughters when a terminal or a trace has none and a binder has one.

Equations

• (PhraseStructure.Tree.Label.terminal a a_1).Licenses x✝ = (x✝ = [])
• (PhraseStructure.Tree.Label.node a).Licenses x✝ = True
• (PhraseStructure.Tree.Label.segment a).Licenses x✝ = True
• (PhraseStructure.Tree.Label.trace a a_1).Licenses x✝ = (x✝ = [])
• (PhraseStructure.Tree.Label.bind a a_1).Licenses x✝ = (x✝.length = 1)

@[instance_reducible]

instance PhraseStructure.Tree.Label.instDecidableLicenses {C : Type u_1} {W : Type u_2} (l : Label C W) (ks : List (Label C W)) : Decidable (l.Licenses ks)

Equations

• (PhraseStructure.Tree.Label.terminal a a_1).instDecidableLicenses x✝ = PhraseStructure.Tree.Label.instDecidableLicenses._aux_1 a a_1 x✝
• (PhraseStructure.Tree.Label.node a).instDecidableLicenses x✝ = { decide := true, reflects_decide := ⋯ }
• (PhraseStructure.Tree.Label.segment a).instDecidableLicenses x✝ = { decide := true, reflects_decide := ⋯ }
• (PhraseStructure.Tree.Label.trace a a_1).instDecidableLicenses x✝ = PhraseStructure.Tree.Label.instDecidableLicenses._aux_5 a a_1 x✝
• (PhraseStructure.Tree.Label.bind a a_1).instDecidableLicenses x✝ = { decide := x✝.length.beq 1, reflects_decide := ⋯ }

def PhraseStructure.Tree.Label.IsPhrase {C : Type u_1} {W : Type u_2} : Label C W → Prop

A label is phrasal when it puts a category over daughters, as a node's or an adjunction mother's does.

Equations

• (PhraseStructure.Tree.Label.node a).IsPhrase = True
• (PhraseStructure.Tree.Label.segment a).IsPhrase = True
• x✝.IsPhrase = False

@[instance_reducible]

instance PhraseStructure.Tree.Label.instDecidablePredIsPhrase {C : Type u_1} {W : Type u_2} : DecidablePred IsPhrase

Equations

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

def PhraseStructure.Tree.Label.IsSegment {C : Type u_1} {W : Type u_2} : Label C W → Prop

A label is a segment label when it marks the mother of an adjunction.

Equations

• (PhraseStructure.Tree.Label.segment a).IsSegment = True
• x✝.IsSegment = False

@[instance_reducible]

instance PhraseStructure.Tree.Label.instDecidablePredIsSegment {C : Type u_1} {W : Type u_2} : DecidablePred IsSegment

Equations

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

@[simp]

theorem PhraseStructure.Tree.Label.licenses_mapWord {C : Type u_1} {W : Type u_2} {W' : Type u_3} (f : W → W') (l : Label C W) (ks : List (Label C W)) : (mapWord f l).Licenses (List.map (mapWord f) ks) ↔ l.Licenses ks

Relabelling the words changes no label's licensed daughters.

@[reducible, inline]

abbrev PhraseStructure.Tree (C : Type u_1) (W : Type u_2) : Type (max u_2 u_1)

In a constituency tree each node is labelled by a Tree.Label.

Equations

• PhraseStructure.Tree C W = RoseTree (PhraseStructure.Tree.Label C W)

The shapes

@[reducible, match_pattern, inline]

abbrev PhraseStructure.Tree.terminal {C : Type u_1} {W : Type u_2} (c : C) (w : W) : Tree C W

terminal c w is the word w under category c.

Equations

• PhraseStructure.Tree.terminal c w = RoseTree.node (PhraseStructure.Tree.Label.terminal c w) []

@[reducible, match_pattern, inline]

abbrev PhraseStructure.Tree.node {C : Type u_1} {W : Type u_2} (c : C) (cs : List (Tree C W)) : Tree C W

node c cs is the category c over daughters cs.

Equations

• PhraseStructure.Tree.node c cs = RoseTree.node (PhraseStructure.Tree.Label.node c) cs

@[reducible, match_pattern, inline]

abbrev PhraseStructure.Tree.adjoin {C : Type u_1} {W : Type u_2} (c : C) (cs : List (Tree C W)) : Tree C W

adjoin c cs is the category c over daughters cs, one of which is its host of category c, the others adjoined to it.

Equations

• PhraseStructure.Tree.adjoin c cs = RoseTree.node (PhraseStructure.Tree.Label.segment c) cs

@[reducible, match_pattern, inline]

abbrev PhraseStructure.Tree.trace {C : Type u_1} {W : Type u_2} (n : ℕ) (c : C) : Tree C W

trace n c is a trace of index n.

Equations

• PhraseStructure.Tree.trace n c = RoseTree.node (PhraseStructure.Tree.Label.trace n c) []

@[reducible, match_pattern, inline]

abbrev PhraseStructure.Tree.bind {C : Type u_1} {W : Type u_2} (n : ℕ) (c : C) (t : Tree C W) : Tree C W

bind n c t is a binder of index n over t.

Equations

• PhraseStructure.Tree.bind n c t = RoseTree.node (PhraseStructure.Tree.Label.bind n c) [t]

@[reducible, match_pattern, inline]

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

Equations

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

@[reducible, match_pattern, inline]

abbrev PhraseStructure.Tree.bin {W : Type u_2} (t₁ t₂ : Tree Unit W) : Tree Unit W

Equations

• t₁.bin t₂ = PhraseStructure.Tree.node () [t₁, t₂]

@[reducible, match_pattern, inline]

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

Equations

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

@[reducible, match_pattern, inline]

abbrev PhraseStructure.Tree.binder {W : Type u_2} (n : ℕ) (t : Tree Unit W) : Tree Unit W

Equations

• PhraseStructure.Tree.binder n t = PhraseStructure.Tree.bind n () t

def PhraseStructure.Tree.cat {C : Type u_1} {W : Type u_2} (t : Tree C W) : C

The category at the root.

Equations

• t.cat = (RoseTree.value t).cat

@[simp]

theorem PhraseStructure.Tree.cat_terminal {C : Type u_1} {W : Type u_2} (c : C) (w : W) : (terminal c w).cat = c

@[simp]

theorem PhraseStructure.Tree.cat_node {C : Type u_1} {W : Type u_2} (c : C) (cs : List (Tree C W)) : (node c cs).cat = c

@[simp]

theorem PhraseStructure.Tree.cat_adjoin {C : Type u_1} {W : Type u_2} (c : C) (cs : List (Tree C W)) : (adjoin c cs).cat = c

@[simp]

theorem PhraseStructure.Tree.cat_trace {C : Type u_1} {W : Type u_2} (n : ℕ) (c : C) : (trace n c).cat = c

@[simp]

theorem PhraseStructure.Tree.cat_bind {C : Type u_1} {W : Type u_2} (n : ℕ) (c : C) (t : Tree C W) : (bind n c t).cat = c

def PhraseStructure.Tree.IsWellFormed {C : Type u_1} {W : Type u_2} (t : Tree C W) : Prop

A tree is well formed when every node has the daughters its label licenses.

Equations

• t.IsWellFormed = RoseTree.Licensed PhraseStructure.Tree.Label.Licenses t

@[instance_reducible]

instance PhraseStructure.Tree.instDecidableIsWellFormed {C : Type u_1} {W : Type u_2} (t : Tree C W) : Decidable t.IsWellFormed

Equations

• t.instDecidableIsWellFormed = { decide := decide (∀ e ∈ RoseTree.localTrees t, e.1.Licenses e.2), reflects_decide := ⋯ }

Induction

def PhraseStructure.Tree.rec' {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)) (adjoin : (c : C) → (cs : List (Tree C W)) → ((t : Tree C W) → t ∈ cs → motive t) → motive (adjoin c cs)) (trace : (n : ℕ) → (c : C) → motive (trace n c)) (bind : (n : ℕ) → (c : C) → (t : Tree C W) → motive t → motive (bind n c t)) (junk : (l : Label C W) → (cs : List (RoseTree (Label C W))) → ¬l.Licenses (List.map RoseTree.value cs) → ((t : Tree C W) → t ∈ cs → motive t) → motive (RoseTree.node l cs)) (t : Tree C W) : motive t

Induction over the five shapes, with the hypothesis at every daughter, and a case for the nodes whose daughters their label does not license.

Equations

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

Relabelling the words

def PhraseStructure.Tree.map {C : Type u_1} {W : Type u_2} {W' : Type u_3} (f : W → W') (t : Tree C W) : Tree C W'

Relabel the words, keeping the shape.

Equations

• PhraseStructure.Tree.map f t = RoseTree.map (PhraseStructure.Tree.Label.mapWord f) t

theorem PhraseStructure.Tree.map_rose {C : Type u_1} {W : Type u_2} {W' : Type u_3} (f : W → W') (l : Label C W) (cs : List (Tree C W)) : map f (RoseTree.node l cs) = RoseTree.node (Label.mapWord f l) (List.map (map f) cs)

@[simp]

theorem PhraseStructure.Tree.value_map {C : Type u_1} {W : Type u_2} {W' : Type u_3} (f : W → W') (t : Tree C W) : RoseTree.value (map f t) = Label.mapWord f (RoseTree.value t)

@[simp]

theorem PhraseStructure.Tree.map_terminal {C : Type u_1} {W : Type u_2} {W' : Type u_3} (f : W → W') (c : C) (w : W) : map f (terminal c w) = terminal c (f w)

@[simp]

theorem PhraseStructure.Tree.map_node {C : Type u_1} {W : Type u_2} {W' : Type u_3} (f : W → W') (c : C) (cs : List (Tree C W)) : map f (node c cs) = node c (List.map (map f) cs)

@[simp]

theorem PhraseStructure.Tree.map_adjoin {C : Type u_1} {W : Type u_2} {W' : Type u_3} (f : W → W') (c : C) (cs : List (Tree C W)) : map f (adjoin c cs) = adjoin c (List.map (map f) cs)

@[simp]

theorem PhraseStructure.Tree.map_trace {C : Type u_1} {W : Type u_2} {W' : Type u_3} (f : W → W') (n : ℕ) (c : C) : map f (trace n c) = trace n c

@[simp]

theorem PhraseStructure.Tree.map_bind {C : Type u_1} {W : Type u_2} {W' : Type u_3} (f : W → W') (n : ℕ) (c : C) (t : Tree C W) : map f (bind n c t) = bind n c (map f t)

@[simp]

theorem PhraseStructure.Tree.map_id {C : Type u_1} {W : Type u_2} (t : Tree C W) : map id t = t

@[simp]

theorem PhraseStructure.Tree.map_map {C : Type u_1} {W : Type u_2} {W' : Type u_3} {W'' : Type u_4} (g : W' → W'') (f : W → W') (t : Tree C W) : map g (map f t) = map (g ∘ f) t

@[simp]

theorem PhraseStructure.Tree.cat_map {C : Type u_1} {W : Type u_2} {W' : Type u_3} (f : W → W') (t : Tree C W) : (map f t).cat = t.cat

The frontier

def PhraseStructure.Tree.terminals {C : Type u_1} {W : Type u_2} (t : Tree C W) : List (C × W)

The terminals, left to right, each with its category, are the word-bearing leaves.

Equations

• t.terminals = List.filterMap PhraseStructure.Tree.Label.terminal? (RoseTree.leafList t)

def PhraseStructure.Tree.yield {C : Type u_1} {W : Type u_2} (t : Tree C W) : List W

The yield of a tree is the words at its terminals, left to right.

Equations

• t.yield = List.map Prod.snd t.terminals

@[simp]

theorem PhraseStructure.Tree.terminals_terminal {C : Type u_1} {W : Type u_2} (c : C) (w : W) : (terminal c w).terminals = [(c, w)]

@[simp]

theorem PhraseStructure.Tree.terminals_node {C : Type u_1} {W : Type u_2} (c : C) (cs : List (Tree C W)) : (node c cs).terminals = List.flatMap terminals cs

@[simp]

theorem PhraseStructure.Tree.terminals_adjoin {C : Type u_1} {W : Type u_2} (c : C) (cs : List (Tree C W)) : (adjoin c cs).terminals = List.flatMap terminals cs

@[simp]

theorem PhraseStructure.Tree.terminals_trace {C : Type u_1} {W : Type u_2} (n : ℕ) (c : C) : (trace n c).terminals = []

@[simp]

theorem PhraseStructure.Tree.terminals_bind {C : Type u_1} {W : Type u_2} (n : ℕ) (c : C) (t : Tree C W) : (bind n c t).terminals = t.terminals

@[simp]

theorem PhraseStructure.Tree.yield_terminal {C : Type u_1} {W : Type u_2} (c : C) (w : W) : (terminal c w).yield = [w]

@[simp]

theorem PhraseStructure.Tree.yield_node {C : Type u_1} {W : Type u_2} (c : C) (cs : List (Tree C W)) : (node c cs).yield = List.flatMap yield cs

@[simp]

theorem PhraseStructure.Tree.yield_adjoin {C : Type u_1} {W : Type u_2} (c : C) (cs : List (Tree C W)) : (adjoin c cs).yield = List.flatMap yield cs

@[simp]

theorem PhraseStructure.Tree.yield_trace {C : Type u_1} {W : Type u_2} (n : ℕ) (c : C) : (trace n c).yield = []

@[simp]

theorem PhraseStructure.Tree.yield_bind {C : Type u_1} {W : Type u_2} (n : ℕ) (c : C) (t : Tree C W) : (bind n c t).yield = t.yield

Categories and subtrees

def PhraseStructure.Tree.cats {C : Type u_1} {W : Type u_2} (t : Tree C W) : List C

The categories at the nodes, in pre-order.

Equations

• t.cats = List.map PhraseStructure.Tree.Label.cat (RoseTree.values t)

theorem PhraseStructure.Tree.cats_rose {C : Type u_1} {W : Type u_2} (l : Label C W) (cs : List (Tree C W)) : cats (RoseTree.node l cs) = l.cat :: List.flatMap cats cs

theorem PhraseStructure.Tree.mem_cats_rose {C : Type u_1} {W : Type u_2} {c : C} {l : Label C W} {cs : List (Tree C W)} : c ∈ cats (RoseTree.node l cs) ↔ c = l.cat ∨ ∃ t ∈ cs, c ∈ t.cats

@[simp]

theorem PhraseStructure.Tree.cats_terminal {C : Type u_1} {W : Type u_2} (c : C) (w : W) : (terminal c w).cats = [c]

@[simp]

theorem PhraseStructure.Tree.cats_node {C : Type u_1} {W : Type u_2} (c : C) (cs : List (Tree C W)) : (node c cs).cats = c :: List.flatMap cats cs

@[simp]

theorem PhraseStructure.Tree.cats_adjoin {C : Type u_1} {W : Type u_2} (c : C) (cs : List (Tree C W)) : (adjoin c cs).cats = c :: List.flatMap cats cs

@[simp]

theorem PhraseStructure.Tree.cats_trace {C : Type u_1} {W : Type u_2} (n : ℕ) (c : C) : (trace n c).cats = [c]

@[simp]

theorem PhraseStructure.Tree.cats_bind {C : Type u_1} {W : Type u_2} (n : ℕ) (c : C) (t : Tree C W) : (bind n c t).cats = c :: t.cats

theorem PhraseStructure.Tree.mem_cats_node {C : Type u_1} {W : Type u_2} {c' c : C} {cs : List (Tree C W)} : c' ∈ (node c cs).cats ↔ c' = c ∨ ∃ t ∈ cs, c' ∈ t.cats

theorem PhraseStructure.Tree.mem_cats_bind {C : Type u_1} {W : Type u_2} {c' : C} {n : ℕ} {c : C} {t : Tree C W} : c' ∈ (bind n c t).cats ↔ c' = c ∨ c' ∈ t.cats

@[simp]

theorem PhraseStructure.Tree.subtrees_terminal {C : Type u_1} {W : Type u_2} (c : C) (w : W) : RoseTree.subtrees (terminal c w) = [terminal c w]

@[simp]

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

@[simp]

theorem PhraseStructure.Tree.subtrees_adjoin {C : Type u_1} {W : Type u_2} (c : C) (cs : List (Tree C W)) : RoseTree.subtrees (adjoin c cs) = adjoin c cs :: List.flatMap RoseTree.subtrees cs

@[simp]

theorem PhraseStructure.Tree.subtrees_trace {C : Type u_1} {W : Type u_2} (n : ℕ) (c : C) : RoseTree.subtrees (trace n c) = [trace n c]

@[simp]

theorem PhraseStructure.Tree.subtrees_bind {C : Type u_1} {W : Type u_2} (n : ℕ) (c : C) (t : Tree C W) : RoseTree.subtrees (bind n c t) = bind n c t :: RoseTree.subtrees t

Free traces

def PhraseStructure.Tree.freeIndices {C : Type u_1} {W : Type u_2} : Tree C W → Finset ℕ

The free indices of a tree are the indices of its traces, less those a dominating binder of the same index binds.

Equations

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

@[simp]

theorem PhraseStructure.Tree.freeIndices_terminal {C : Type u_1} {W : Type u_2} (c : C) (w : W) : (terminal c w).freeIndices = ∅

theorem PhraseStructure.Tree.freeIndices_node {C : Type u_1} {W : Type u_2} (c : C) (cs : List (Tree C W)) : (node c cs).freeIndices = List.foldr (fun (x1 x2 : Finset ℕ) => x1 ∪ x2) ∅ (List.map freeIndices cs)

theorem PhraseStructure.Tree.freeIndices_adjoin {C : Type u_1} {W : Type u_2} (c : C) (cs : List (Tree C W)) : (adjoin c cs).freeIndices = List.foldr (fun (x1 x2 : Finset ℕ) => x1 ∪ x2) ∅ (List.map freeIndices cs)

@[simp]

theorem PhraseStructure.Tree.freeIndices_trace {C : Type u_1} {W : Type u_2} (n : ℕ) (c : C) : (trace n c).freeIndices = {n}

@[simp]

theorem PhraseStructure.Tree.freeIndices_bind {C : Type u_1} {W : Type u_2} (n : ℕ) (c : C) (t : Tree C W) : (bind n c t).freeIndices = t.freeIndices.erase n

@[simp]

theorem PhraseStructure.Tree.mem_freeIndices_node {C : Type u_1} {W : Type u_2} {i : ℕ} {c : C} {cs : List (Tree C W)} : i ∈ (node c cs).freeIndices ↔ ∃ t ∈ cs, i ∈ t.freeIndices

@[simp]

theorem PhraseStructure.Tree.mem_freeIndices_adjoin {C : Type u_1} {W : Type u_2} {i : ℕ} {c : C} {cs : List (Tree C W)} : i ∈ (adjoin c cs).freeIndices ↔ ∃ t ∈ cs, i ∈ t.freeIndices

def PhraseStructure.Tree.Closed {C : Type u_1} {W : Type u_2} (t : Tree C W) : Prop

A tree is closed when no trace is free in it.

Equations

• t.Closed = (t.freeIndices = ∅)

@[instance_reducible]

instance PhraseStructure.Tree.instDecidableClosedOfDecidableEq {C : Type u_1} {W : Type u_2} [DecidableEq C] [DecidableEq W] (t : Tree C W) : Decidable t.Closed

Equations

• t.instDecidableClosedOfDecidableEq = { decide := decide (t.freeIndices.val = ∅.val), reflects_decide := ⋯ }

Word substitution

def PhraseStructure.Tree.leafSubst {C : Type u_1} {W : Type u_2} [DecidableEq C] [DecidableEq W] (w w' : W) (c : C) (t : Tree C W) : Tree C W

Replace the word w by w' at every terminal of category c.

Equations

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

@[simp]

theorem PhraseStructure.Tree.leafSubst_terminal {C : Type u_1} {W : Type u_2} [DecidableEq C] [DecidableEq W] (w w' : W) (c c' : C) (v : W) : leafSubst w w' c (terminal c' v) = terminal c' (if c = c' ∧ v = w then w' else v)

@[simp]

theorem PhraseStructure.Tree.leafSubst_node {C : Type u_1} {W : Type u_2} [DecidableEq C] [DecidableEq W] (w w' : W) (c c' : C) (cs : List (Tree C W)) : leafSubst w w' c (node c' cs) = node c' (List.map (leafSubst w w' c) cs)

@[simp]

theorem PhraseStructure.Tree.leafSubst_adjoin {C : Type u_1} {W : Type u_2} [DecidableEq C] [DecidableEq W] (w w' : W) (c c' : C) (cs : List (Tree C W)) : leafSubst w w' c (adjoin c' cs) = adjoin c' (List.map (leafSubst w w' c) cs)

@[simp]

theorem PhraseStructure.Tree.leafSubst_trace {C : Type u_1} {W : Type u_2} [DecidableEq C] [DecidableEq W] (w w' : W) (c : C) (n : ℕ) (c' : C) : leafSubst w w' c (trace n c') = trace n c'

@[simp]

theorem PhraseStructure.Tree.leafSubst_bind {C : Type u_1} {W : Type u_2} [DecidableEq C] [DecidableEq W] (w w' : W) (c : C) (n : ℕ) (c' : C) (t : Tree C W) : leafSubst w w' c (bind n c' t) = bind n c' (leafSubst w w' c t)

Positions

A tree takes Gorn addresses as a rose tree, and with them the dominance order on its positions and, in Syntax/Command.lean, the command relations.

@[simp]

theorem PhraseStructure.Tree.children_terminal {C : Type u_1} {W : Type u_2} (c : C) (w : W) : RoseTree.children (terminal c w) = []

@[simp]

theorem PhraseStructure.Tree.children_node {C : Type u_1} {W : Type u_2} (c : C) (cs : List (Tree C W)) : RoseTree.children (node c cs) = cs

@[simp]

theorem PhraseStructure.Tree.children_adjoin {C : Type u_1} {W : Type u_2} (c : C) (cs : List (Tree C W)) : RoseTree.children (adjoin c cs) = cs

@[simp]

theorem PhraseStructure.Tree.children_trace {C : Type u_1} {W : Type u_2} (n : ℕ) (c : C) : RoseTree.children (trace n c) = []

@[simp]

theorem PhraseStructure.Tree.children_bind {C : Type u_1} {W : Type u_2} (n : ℕ) (c : C) (t : Tree C W) : RoseTree.children (bind n c t) = [t]

Positions of the terminals

The terminals, paired with their positions, are the word-bearing leaves, so the order of the yield is precedence (RoseTree.pairwise_precedes_positionedLeaves).

def PhraseStructure.Tree.positionedTerminals {C : Type u_1} {W : Type u_2} (t : Tree C W) : List (Core.Order.TreePath × C × W)

The terminals, left to right, each paired with its position.

Equations

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

theorem PhraseStructure.Tree.map_snd_positionedTerminals {C : Type u_1} {W : Type u_2} (t : Tree C W) : List.map Prod.snd t.positionedTerminals = t.terminals

Forgetting the positions leaves the terminals.

theorem PhraseStructure.Tree.subtreeAt_of_mem_positionedTerminals {C : Type u_1} {W : Type u_2} {t : Tree C W} {x : Core.Order.TreePath × C × W} (h : x ∈ t.positionedTerminals) : RoseTree.subtreeAt t x.1.toList = some (terminal x.2.1 x.2.2)

Each listed position holds its terminal.

theorem PhraseStructure.Tree.mem_positionedTerminals_of_subtreeAt {C : Type u_1} {W : Type u_2} {t : Tree C W} {p : List ℕ} {c : C} {w : W} (h : RoseTree.subtreeAt t p = some (terminal c w)) : ({ toList := p }, c, w) ∈ t.positionedTerminals

Every terminal position is listed.

theorem PhraseStructure.Tree.pairwise_precedes_positionedTerminals {C : Type u_1} {W : Type u_2} (t : Tree C W) : List.Pairwise (fun (x y : Core.Order.TreePath × C × W) => x.1.Precedes y.1) t.positionedTerminals

The terminal positions, in the order of the yield, ascend in precedence.