definition
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
Definition
A ranked alphabet is a finite type of symbols together with a natural-number rank for every symbol. A tree over a ranked alphabet is a finite term: a node labelled by a symbol of rank has exactly ordered children.
Nodes are occurrences of symbols in a particular tree. They carry their labels and their indexed immediate-child relation intrinsically, independently of any logical presentation of trees.
Lean source view on GitHub
| 1 | import Mathlib.Data.Fintype.Basic |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Finite ranked trees |
| 6 | type: definition |
| 7 | --- |
| 8 | |
| 9 | A ranked alphabet is a finite type of symbols together with a natural-number |
| 10 | rank for every symbol. A tree over a ranked alphabet is a finite term: a node |
| 11 | labelled by a symbol of rank has exactly ordered children. |
| 12 | |
| 13 | Nodes are occurrences of symbols in a particular tree. They carry their |
| 14 | labels and their indexed immediate-child relation intrinsically, independently |
| 15 | of any logical presentation of trees. |
| 16 | |
| 17 | -/ |
| 18 | |
| 19 | namespace Lax53.RankedTree |
| 20 | |
| 21 | universe u |
| 22 | |
| 23 | /-- A finite alphabet whose symbols have prescribed arities. -/ |
| 24 | structure RankedAlphabet where |
| 25 | Symbol : Type u |
| 26 | [symbolsFintype : Fintype Symbol] |
| 27 | [symbolsDecidableEq : DecidableEq Symbol] |
| 28 | rank : Symbol → Nat |
| 29 | |
| 30 | attribute [instance] RankedAlphabet.symbolsFintype |
| 31 | attribute [instance] RankedAlphabet.symbolsDecidableEq |
| 32 | |
| 33 | /-- Finite terms over a ranked alphabet. A node labelled by `a` has one |
| 34 | ordered child for each element of `Fin (A.rank a)`. -/ |
| 35 | inductive Tree (A : RankedAlphabet.{u}) : Type u |
| 36 | | node (a : A.Symbol) (children : Fin (A.rank a) → Tree A) : Tree A |
| 37 | |
| 38 | /-- The set of child slots occurring in the alphabet. Its zero-based index |
| 39 | `i` represents the slot customarily numbered `i+1`. -/ |
| 40 | def ChildIndex (A : RankedAlphabet.{u}) : Type := |
| 41 | {i : Nat // ∃ a : A.Symbol, i < A.rank a} |
| 42 | |
| 43 | namespace ChildIndex |
| 44 | |
| 45 | /-- Regard a child slot of a particular symbol as a child slot of the whole |
| 46 | alphabet. -/ |
| 47 | def ofSymbolIndex {A : RankedAlphabet.{u}} (a : A.Symbol) |
| 48 | (i : Fin (A.rank a)) : ChildIndex A := |
| 49 | ⟨i, ⟨a, i.isLt⟩⟩ |
| 50 | |
| 51 | end ChildIndex |
| 52 | |
| 53 | /-- The nodes occurring in a particular ranked tree. -/ |
| 54 | inductive Node {A : RankedAlphabet.{u}} : Tree A → Type u |
| 55 | | root {a : A.Symbol} {children : Fin (A.rank a) → Tree A} : |
| 56 | Node (.node a children) |
| 57 | | inChild {a : A.Symbol} {children : Fin (A.rank a) → Tree A} |
| 58 | (i : Fin (A.rank a)) (p : Node (children i)) : |
| 59 | Node (.node a children) |
| 60 | |
| 61 | namespace Node |
| 62 | |
| 63 | /-- The root node of a tree. -/ |
| 64 | def rootOf {A : RankedAlphabet.{u}} : (t : Tree A) → Node t |
| 65 | | .node _ _ => .root |
| 66 | |
| 67 | /-- The symbol labelling a node. -/ |
| 68 | def label {A : RankedAlphabet.{u}} : {t : Tree A} → Node t → A.Symbol |
| 69 | | .node a _, .root => a |
| 70 | | .node _ _, .inChild _ p => label p |
| 71 | |
| 72 | /-- The `i`th child of a node, as a node of the same ambient tree. -/ |
| 73 | def child {A : RankedAlphabet.{u}} : |
| 74 | {t : Tree A} → (p : Node t) → Fin (A.rank p.label) → Node t |
| 75 | | .node _ children, .root, i => .inChild i (rootOf (children i)) |
| 76 | | .node _ _, .inChild j p, i => .inChild j (child p i) |
| 77 | |
| 78 | /-- `ChildAt i p q` says that `q` is the immediate child of `p` in the |
| 79 | alphabet-wide child slot `i`. -/ |
| 80 | def ChildAt {A : RankedAlphabet.{u}} (i : ChildIndex A) {t : Tree A} |
| 81 | (p q : Node t) : Prop := |
| 82 | ∃ j : Fin (A.rank p.label), |
| 83 | ChildIndex.ofSymbolIndex p.label j = i ∧ q = child p j |
| 84 | |
| 85 | end Node |
| 86 | |
| 87 | /-- A language of ranked trees. -/ |
| 88 | abbrev TreeLanguage (A : RankedAlphabet.{u}) := Set (Tree A) |
| 89 | |
| 90 | end Lax53.RankedTree |
| 91 |
Community review
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.
0 comments