Lax53.TreeStructure
Ranked trees as finite relational structures
concepts/Lax53/TreeStructure.lean · lax-53
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
Definition
A ranked tree is viewed as a relational structure on its nodes. For every alphabet symbol there is a unary predicate selecting the nodes carrying that symbol. For every child slot up to the maximum rank of the alphabet there is a binary relation connecting a node to its child in that slot.
The label and child relations directly define the canonical structure of each tree. An MSO sentence defines the language of all ranked trees whose canonical structure satisfies it.
Lean source view on GitHub
| 1 | import Lax52.MSOSyntax |
| 2 | import Lax52.MSOSemantics |
| 3 | import Lax53.RankedTree |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Ranked trees as finite relational structures |
| 8 | type: definition |
| 9 | --- |
| 10 | |
| 11 | A ranked tree is viewed as a relational structure on its nodes. For every |
| 12 | alphabet symbol there is a unary predicate selecting the nodes carrying that |
| 13 | symbol. For every child slot up to the maximum rank of the alphabet there is a |
| 14 | binary relation connecting a node to its child in that slot. |
| 15 | |
| 16 | The label and child relations directly define the canonical structure of each |
| 17 | tree. An MSO sentence defines the language of all ranked trees whose canonical |
| 18 | structure satisfies it. |
| 19 | -/ |
| 20 | |
| 21 | namespace Lax53.TreeStructure |
| 22 | |
| 23 | open FirstOrder |
| 24 | open FirstOrder.Language |
| 25 | open Lax53.RankedTree |
| 26 | |
| 27 | universe u |
| 28 | |
| 29 | /-- Relation symbols for ranked trees. -/ |
| 30 | inductive TreeRelation (A : RankedAlphabet.{u}) : Nat → Type u |
| 31 | | label (a : A.Symbol) : TreeRelation A 1 |
| 32 | | child (i : ChildIndex A) : TreeRelation A 2 |
| 33 | |
| 34 | /-- The first-order language of ranked trees over `A`. -/ |
| 35 | def treeSignature (A : RankedAlphabet.{u}) : FirstOrder.Language.{0, u} where |
| 36 | Functions := fun _ => Empty |
| 37 | Relations := TreeRelation A |
| 38 | |
| 39 | /-- The canonical first-order structure of a ranked tree. -/ |
| 40 | @[implicit_reducible] |
| 41 | def treeStructure {A : RankedAlphabet.{u}} (t : Tree A) : |
| 42 | (treeSignature A).Structure (Node t) where |
| 43 | funMap f := nomatch f |
| 44 | RelMap |
| 45 | | .label a, xs => Node.label (xs 0) = a |
| 46 | | .child i, xs => Node.ChildAt i (xs 0) (xs 1) |
| 47 | |
| 48 | /-- Satisfaction of a closed MSO sentence by the canonical structure of a |
| 49 | ranked tree. -/ |
| 50 | def TreeModels {A : RankedAlphabet.{u}} (t : Tree A) |
| 51 | (phi : Lax52.MSOSyntax.Sentence (treeSignature A)) : Prop := |
| 52 | @Lax52.MSOSemantics.Realize (treeSignature A) (Node t) (treeStructure t) 0 0 phi |
| 53 | (fun i : Fin 0 => Fin.elim0 i) (fun i : Fin 0 => Fin.elim0 i) |
| 54 | |
| 55 | /-- The ranked-tree language defined by an MSO sentence. -/ |
| 56 | def sentenceLanguage {A : RankedAlphabet.{u}} |
| 57 | (phi : Lax52.MSOSyntax.Sentence (treeSignature A)) : TreeLanguage A := |
| 58 | {t | TreeModels t phi} |
| 59 | |
| 60 | end Lax53.TreeStructure |
| 61 |
From Mathlib
none
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