No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
Definition
A (non-copying) first-order transduction from structures of a language L to structures of a relational language L' consists of a number k of unary color predicates, a domain formula, and one formula per relation symbol of L', all over L expanded by the colors. Applied to an L-structure together with an arbitrary coloring of its elements, the transduction outputs the L'-structure whose universe is the set of elements satisfying the domain formula and whose relations are defined by the interpreting formulas.
A class C of structures transduces a class D if a single transduction produces every member of D, up to isomorphism, from some colored member of C.
Lean source view on GitHub
| 1 | import Mathlib.ModelTheory.Semantics |
| 2 | import Mathlib.Logic.Embedding.Basic |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: First-order transductions |
| 7 | type: definition |
| 8 | --- |
| 9 | A (non-copying) first-order transduction from structures of a language |
| 10 | *L* to structures of a relational language *L'* consists of a number *k* |
| 11 | of unary *color* predicates, a *domain* formula, and one formula per |
| 12 | relation symbol of *L'*, all over *L* expanded by the colors. Applied to |
| 13 | an *L*-structure together with an arbitrary coloring of its elements, |
| 14 | the transduction outputs the *L'*-structure whose universe is the set of |
| 15 | elements satisfying the domain formula and whose relations are defined |
| 16 | by the interpreting formulas. |
| 17 | |
| 18 | A class *C* of structures transduces a class *D* if a single |
| 19 | transduction produces every member of *D*, up to isomorphism, from some |
| 20 | colored member of *C*. |
| 21 | |
| 22 | # Formalization notes |
| 23 | |
| 24 | Languages, formulas and semantics are mathlib's: a formula with `r` free |
| 25 | variables is a `Formula (Fin r)`, realized via `Formula.Realize`. The |
| 26 | color expansion is the sum of `L` with a language of `k` unary relation |
| 27 | symbols; `RealizeIn` confines the instance plumbing (mathlib treats |
| 28 | structures as instances, this submission treats them as data) to a |
| 29 | single definition. |
| 30 | |
| 31 | In `Transduces`, the embedding `f` carries the isomorphism: its range |
| 32 | must be exactly the set defined by the domain formula, and each target |
| 33 | relation must be defined by its interpreting formula. The target |
| 34 | language is required to be relational because a transduction interprets |
| 35 | relations only; function symbols on the target side would be silently |
| 36 | unconstrained. Since colorings are existentially quantified, taking an |
| 37 | *arbitrary* induced substructure instead of a definable one yields the |
| 38 | same transduces relation — a fresh color can serve as the domain |
| 39 | formula. Only non-copying transductions are defined; the results of this |
| 40 | submission need nothing more. |
| 41 | -/ |
| 42 | |
| 43 | namespace Lax5.Transductions |
| 44 | |
| 45 | open FirstOrder |
| 46 | |
| 47 | universe u v u' v' |
| 48 | |
| 49 | /-- A class of finite structures of the language `L`: for each `n`, a |
| 50 | predicate on the `L`-structures over the canonical `n`-element type. -/ |
| 51 | abbrev StructureClass (L : Language.{u, v}) : Type (max u v) := |
| 52 | ∀ n : ℕ, L.Structure (Fin n) → Prop |
| 53 | |
| 54 | /-- The relation symbols of the color language: `k` unary predicates. -/ |
| 55 | inductive ColorRel (k : ℕ) : ℕ → Type |
| 56 | | color (i : Fin k) : ColorRel k 1 |
| 57 | |
| 58 | /-- The language consisting of `k` unary color predicates and nothing |
| 59 | else. -/ |
| 60 | def colorLanguage (k : ℕ) : Language := |
| 61 | ⟨fun _ => Empty, ColorRel k⟩ |
| 62 | deriving Language.IsRelational |
| 63 | |
| 64 | /-- The language `L` expanded by `k` unary color predicates. -/ |
| 65 | abbrev withColors (L : Language.{u, v}) (k : ℕ) : Language := |
| 66 | L.sum (colorLanguage k) |
| 67 | |
| 68 | /-- The color sets `colors` as a structure of the color language: |
| 69 | `.color i` holds of the elements of `colors i`. -/ |
| 70 | @[implicit_reducible] |
| 71 | def colorStructure {M : Type*} {k : ℕ} (colors : Fin k → Set M) : |
| 72 | (colorLanguage k).Structure M where |
| 73 | RelMap | .color i => fun x => x 0 ∈ colors i |
| 74 | |
| 75 | /-- The formula `φ` of the colored language holds of the tuple `v` in |
| 76 | the `L`-structure `M` expanded by the color sets `colors`. -/ |
| 77 | def RealizeIn {L : Language.{u, v}} {n k : ℕ} (M : L.Structure (Fin n)) |
| 78 | (colors : Fin k → Set (Fin n)) {α : Type*} |
| 79 | (φ : (withColors L k).Formula α) (v : α → Fin n) : Prop := |
| 80 | letI := M |
| 81 | letI := colorStructure colors |
| 82 | φ.Realize v |
| 83 | |
| 84 | /-- A non-copying transduction from `L`-structures to `L'`-structures: |
| 85 | finitely many unary colors, a domain formula selecting the output |
| 86 | universe, and one formula per relation symbol of the target language. -/ |
| 87 | structure Transduction (L : Language.{u, v}) (L' : Language.{u', v'}) where |
| 88 | /-- The number of unary color predicates. -/ |
| 89 | colors : ℕ |
| 90 | /-- The formula selecting the elements of the output structure. -/ |
| 91 | domain : (withColors L colors).Formula (Fin 1) |
| 92 | /-- The formula interpreting each relation symbol of the target. -/ |
| 93 | rel : ∀ {r : ℕ}, L'.Relations r → (withColors L colors).Formula (Fin r) |
| 94 | |
| 95 | /-- `C` transduces `D`: a single transduction produces every member of |
| 96 | `D` from some colored member of `C`, up to isomorphism — the embedding |
| 97 | `f` identifies the output structure with the substructure of elements |
| 98 | selected by the domain formula. -/ |
| 99 | def Transduces {L : Language.{u, v}} {L' : Language.{u', v'}} |
| 100 | [L'.IsRelational] (C : StructureClass L) (D : StructureClass L') : |
| 101 | Prop := |
| 102 | ∃ T : Transduction L L', |
| 103 | ∀ (m : ℕ) (N : L'.Structure (Fin m)), D m N → |
| 104 | ∃ (n : ℕ) (M : L.Structure (Fin n)), C n M ∧ |
| 105 | ∃ (colors : Fin T.colors → Set (Fin n)) (f : Fin m ↪ Fin n), |
| 106 | (∀ x : Fin n, |
| 107 | x ∈ Set.range f ↔ RealizeIn M colors T.domain ![x]) ∧ |
| 108 | ∀ {r : ℕ} (R : L'.Relations r) (v : Fin r → Fin m), |
| 109 | N.RelMap R v ↔ RealizeIn M colors (T.rel R) (f ∘ v) |
| 110 | |
| 111 | end Lax5.Transductions |
| 112 |
Formalization notes
Languages, formulas and semantics are mathlib's: a formula with free variables is a , realized via . The color expansion is the sum of with a language of unary relation symbols; confines the instance plumbing (mathlib treats structures as instances, this submission treats them as data) to a single definition.
In , the embedding carries the isomorphism: its range must be exactly the set defined by the domain formula, and each target relation must be defined by its interpreting formula. The target language is required to be relational because a transduction interprets relations only; function symbols on the target side would be silently unconstrained. Since colorings are existentially quantified, taking an arbitrary induced substructure instead of a definable one yields the same transduces relation — a fresh color can serve as the domain formula. Only non-copying transductions are defined; the results of this submission need nothing more.
Builds on
none
Used by
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