Lax678846.FiniteStructures
Finite relational structures and their properties
concepts/Lax678846/FiniteStructures.lean · lax-678846
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
Definition
A finite relational vocabulary is a finite list of relation arities. A structure has universe and an interpretation of each relation. The numbering is used for binary input encodings; it is not available as an order predicate in the logic. Properties are required to be invariant under isomorphism, so they do not depend on the numbering.
The representation and dense binary encoding are reused from the Immerman–Vardi submission. Here we forget its distinguished order. Empty universes and nullary relations are allowed.
Lean source view on GitHub
| 1 | import Lax979537.OrderedStructures |
| 2 | import Lax979537.StructureEncoding |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Finite relational structures and their properties |
| 7 | type: definition |
| 8 | --- |
| 9 | A finite relational vocabulary is a finite list of relation arities. A |
| 10 | structure has universe `Fin n` and an interpretation of each relation. |
| 11 | The numbering is used for binary input encodings; it is not available as |
| 12 | an order predicate in the logic. Properties are required to be invariant |
| 13 | under isomorphism, so they do not depend on the numbering. |
| 14 | |
| 15 | The representation and dense binary encoding are reused from the |
| 16 | Immerman–Vardi submission. Here we forget its distinguished order. Empty |
| 17 | universes and nullary relations are allowed. |
| 18 | -/ |
| 19 | |
| 20 | namespace Lax678846.FiniteStructures |
| 21 | |
| 22 | abbrev Vocabulary := Lax979537.OrderedStructures.Vocabulary |
| 23 | abbrev Symbol := Lax979537.OrderedStructures.Symbol |
| 24 | abbrev Structure := Lax979537.OrderedStructures.OrderedStructure |
| 25 | abbrev Interpretation (σ : Vocabulary) (n : Nat) := |
| 26 | (r : Symbol σ) → (Fin (σ.get r) → Fin n) → Bool |
| 27 | abbrev Property (σ : Vocabulary) := Structure σ → Prop |
| 28 | |
| 29 | structure Isomorphism {σ : Vocabulary} (A B : Structure σ) where |
| 30 | equivalence : Fin A.size ≃ Fin B.size |
| 31 | preserves : ∀ (r : Symbol σ) (a : Fin (σ.get r) → Fin A.size), |
| 32 | B.relation r (equivalence ∘ a) = A.relation r a |
| 33 | |
| 34 | def IsomorphismInvariant {σ : Vocabulary} (Q : Property σ) : Prop := |
| 35 | ∀ A B : Structure σ, Nonempty (Isomorphism A B) → (Q A ↔ Q B) |
| 36 | |
| 37 | def encode {σ : Vocabulary} (A : Structure σ) : List Bool := |
| 38 | Lax979537.StructureEncoding.encode ⟨A, Fin.elim0⟩ |
| 39 | |
| 40 | def language {σ : Vocabulary} (Q : Property σ) (w : List Bool) : Prop := |
| 41 | ∃ A : Structure σ, encode A = w ∧ Q A |
| 42 | |
| 43 | end Lax678846.FiniteStructures |
| 44 |
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