Lax52.WordStructure
Words as finite relational structures
concepts/Lax52/WordStructure.lean · lax-52
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
Definition
A word over an alphabet is viewed as a structure whose elements are its positions, ordered by their natural order, with one unary predicate for each letter. The predicate belonging to holds exactly at positions carrying the letter . These properties uniquely determine the structure; no particular construction of it is part of the concept.
Lean source view on GitHub
| 1 | import Lax52.MSOSemantics |
| 2 | import Mathlib.Computability.NFA |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Words as finite relational structures |
| 7 | type: definition |
| 8 | --- |
| 9 | |
| 10 | A word over an alphabet `Sigma` is viewed as a structure whose elements are its |
| 11 | positions, ordered by their natural order, with one unary predicate for each |
| 12 | letter. The predicate belonging to `a` holds exactly at positions carrying |
| 13 | the letter `a`. These properties uniquely determine the structure; no |
| 14 | particular construction of it is part of the concept. |
| 15 | -/ |
| 16 | |
| 17 | namespace Lax52.WordStructure |
| 18 | |
| 19 | open FirstOrder |
| 20 | open FirstOrder.Language |
| 21 | open Lax52.MSOSyntax |
| 22 | open Lax52.MSOSemantics |
| 23 | |
| 24 | universe u |
| 25 | |
| 26 | /-- Relation symbols of the language of words over `Sigma`. -/ |
| 27 | inductive WordRelation (Sigma : Type u) : Nat → Type u |
| 28 | | letter (a : Sigma) : WordRelation Sigma 1 |
| 29 | | le : WordRelation Sigma 2 |
| 30 | |
| 31 | /-- The first-order language with order and one unary predicate per letter. -/ |
| 32 | def wordLanguage (Sigma : Type u) : FirstOrder.Language.{0, u} where |
| 33 | Functions := fun _ => Empty |
| 34 | Relations := WordRelation Sigma |
| 35 | |
| 36 | /-- A structure has the relational content of `w` when its unary letter |
| 37 | relations record exactly the letters of `w` and its order relation is the |
| 38 | natural order on positions. -/ |
| 39 | def IsWordStructure {Sigma : Type u} (w : List Sigma) |
| 40 | (S : (wordLanguage Sigma).Structure (Fin w.length)) : Prop := |
| 41 | (∀ (a : Sigma) (xs : Fin 1 → Fin w.length), |
| 42 | @FirstOrder.Language.Structure.RelMap |
| 43 | (wordLanguage Sigma) (Fin w.length) S 1 (WordRelation.letter a) xs ↔ |
| 44 | w.get (xs 0) = a) ∧ |
| 45 | (∀ xs : Fin 2 → Fin w.length, |
| 46 | @FirstOrder.Language.Structure.RelMap |
| 47 | (wordLanguage Sigma) (Fin w.length) S 2 WordRelation.le xs ↔ |
| 48 | xs 0 ≤ xs 1) |
| 49 | |
| 50 | /-- The relational content of a word determines a unique first-order |
| 51 | structure on its positions. -/ |
| 52 | axiom existsUnique_wordStructure {Sigma : Type u} (w : List Sigma) : |
| 53 | ∃! S : (wordLanguage Sigma).Structure (Fin w.length), IsWordStructure w S |
| 54 | |
| 55 | /-- Satisfaction of a closed MSO sentence by a word, expressed using any |
| 56 | structure with the uniquely determined relational content of that word. -/ |
| 57 | def WordModels {Sigma : Type u} (w : List Sigma) |
| 58 | (phi : MSOSyntax.Sentence (wordLanguage Sigma)) : Prop := |
| 59 | ∀ S : (wordLanguage Sigma).Structure (Fin w.length), IsWordStructure w S → |
| 60 | @MSOSemantics.Realize (wordLanguage Sigma) (Fin w.length) S 0 0 phi |
| 61 | (fun i : Fin 0 => Fin.elim0 i) (fun i : Fin 0 => Fin.elim0 i) |
| 62 | |
| 63 | /-- The language of words satisfying an MSO sentence. -/ |
| 64 | def sentenceLanguage {Sigma : Type u} (phi : MSOSyntax.Sentence (wordLanguage Sigma)) : |
| 65 | _root_.Language Sigma := |
| 66 | {w | WordModels w phi} |
| 67 | |
| 68 | end Lax52.WordStructure |
| 69 |
Builds on
Used by
From Mathlib
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