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 r free
variables is a Formula (Fin r), realized via Formula.Realize. The
color expansion is the sum of L with a language of k unary relation
symbols; RealizeIn confines the instance plumbing (mathlib treats
structures as instances, this submission treats them as data) to a
single definition.
In Transduces, the embedding f 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.
Imported
none