Problems as sets of concrete finite structures
Lax624099.ConcreteInstances · concepts/Lax624099/ConcreteInstances.lean · lax-624099
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
A problem on finite structures read as a set of concrete data. A presented vocabulary numbers the finitely many relation symbols of a vocabulary with their arities, so that reading a symbol off its number and numbering a symbol are inverse; every vocabulary of the catalog is presented this way, and the vocabularies of machine instances, of encoded sentences and of code instances are presented here. A concrete finite structure over a presented vocabulary is a universe size and a table of Booleans, one row per symbol, the row of an -ary symbol read at the number of a tuple written in base the size of the universe; out-of-range lookups read false, so every such piece of data denotes a structure, on a nonempty linearly ordered universe. The predicate a decision problem defines on concrete structures holds of a piece of data when the structure it denotes is a yes-instance. This is the type on which Mathlib's computability notions, decidability and recursive enumerability, are read.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.Order.PiLex |
| 2 | import Mathlib.Data.Prod.Lex |
| 3 | import Mathlib.Data.Fintype.EquivFin |
| 4 | import Mathlib.ModelTheory.Order |
| 5 | import Mathlib.ModelTheory.Semantics |
| 6 | import Mathlib.ModelTheory.Complexity |
| 7 | import Mathlib.Tactic.FinCases |
| 8 | import Mathlib.Logic.Equiv.Fin.Basic |
| 9 | import Mathlib.Data.Finite.Sigma |
| 10 | import Mathlib.Data.Fintype.Lattice |
| 11 | import Mathlib.Data.Set.Card |
| 12 | import Mathlib.ModelTheory.Syntax |
| 13 | import Mathlib.Algebra.BigOperators.Finprod |
| 14 | import Mathlib.Data.Set.Finite.Lemmas |
| 15 | import Mathlib.SetTheory.Cardinal.Finite |
| 16 | import Mathlib.Logic.Equiv.Prod |
| 17 | import Mathlib.Algebra.Order.BigOperators.Group.Finset |
| 18 | import Mathlib.Order.Lattice.Nat |
| 19 | import Mathlib.Data.Fintype.Pigeonhole |
| 20 | import Mathlib.Dynamics.FixedPoints.Basic |
| 21 | import Mathlib.Data.Fintype.Card |
| 22 | import Mathlib.Logic.Relation |
| 23 | import Mathlib.Computability.RE |
| 24 | import Mathlib.Data.List.NodupEquivFin |
| 25 | import Mathlib.Logic.Equiv.Sum |
| 26 | import Mathlib.Computability.Primrec.List |
| 27 | import Mathlib.Data.Fintype.Pi |
| 28 | import Mathlib.Computability.Halting |
| 29 | import Mathlib.Computability.PartrecCode |
| 30 | import Mathlib.Tactic.Ring |
| 31 | import Lax624099.CodeHalting |
| 32 | import Lax624099.FiniteSatisfiability |
| 33 | import Lax904597.Machines |
| 34 | import Lax904597.Problems |
| 35 | |
| 36 | /-! |
| 37 | --- |
| 38 | title: Problems as sets of concrete finite structures |
| 39 | type: definition |
| 40 | --- |
| 41 | A problem on finite structures read as a set of concrete data. A presented |
| 42 | vocabulary numbers the finitely many relation symbols of a vocabulary with |
| 43 | their arities, so that reading a symbol off its number and numbering a |
| 44 | symbol are inverse; every vocabulary of the catalog is presented this way, |
| 45 | and the vocabularies of machine instances, of encoded sentences and of code |
| 46 | instances are presented here. A concrete finite structure over a presented |
| 47 | vocabulary is a universe size and a table of Booleans, one row per symbol, |
| 48 | the row of an -ary symbol read at the number of a tuple written in base |
| 49 | the size of the universe; out-of-range lookups read false, so every such |
| 50 | piece of data denotes a structure, on a nonempty linearly ordered universe. |
| 51 | The predicate a decision problem defines on concrete structures holds of a |
| 52 | piece of data when the structure it denotes is a yes-instance. This is the |
| 53 | type on which Mathlib's computability notions, decidability and recursive |
| 54 | enumerability, are read. |
| 55 | -/ |
| 56 | |
| 57 | namespace Lax624099.ConcreteInstances |
| 58 | |
| 59 | open Lax904597.Problems |
| 60 | |
| 61 | open FirstOrder |
| 62 | |
| 63 | open FirstOrder.Language Structure |
| 64 | |
| 65 | section Digits |
| 66 | |
| 67 | /-- The number of a tuple of digits, little-endian in base `c`. -/ |
| 68 | def tupleIdx (c : ℕ) : List ℕ → ℕ |
| 69 | | [] => 0 |
| 70 | | a :: l => a + c * tupleIdx c l |
| 71 | |
| 72 | /-- The `j`-th digit of `t` in base `c`. -/ |
| 73 | def digitAt (c t j : ℕ) : ℕ := t / c ^ j % c |
| 74 | |
| 75 | end Digits |
| 76 | |
| 77 | /-- A **finitely presented relational vocabulary**: the relation symbols of `L` |
| 78 | numbered by `Fin numSyms`, with their arities. Reading a symbol off its number |
| 79 | (`sym`) and numbering a symbol (`index`) are mutually inverse, so the |
| 80 | presentation loses nothing. |
| 81 | |
| 82 | Every vocabulary of the catalog is of this shape: `Language.turing` has 12 |
| 83 | symbols of arity at most 2, `Language.finsat` 14 of arity at most 3. The |
| 84 | presentations are closed under `Language.sum` |
| 85 | (`FirstOrder.Language.FinVocab.sum`), which is what lets the second-order |
| 86 | machinery – whose vocabularies are sums of the instance's with a block's – be |
| 87 | encoded by the same means. -/ |
| 88 | structure FinVocab (L : Language.{0, 0}) where |
| 89 | /-- The number of relation symbols. -/ |
| 90 | numSyms : ℕ |
| 91 | /-- The symbol with a given number, together with its arity. -/ |
| 92 | symOf : Fin numSyms → ((n : ℕ) × L.Relations n) |
| 93 | /-- The number of a symbol. -/ |
| 94 | index : ∀ {n : ℕ}, L.Relations n → Fin numSyms |
| 95 | /-- Reading back the symbol with the number of a symbol gives it back. -/ |
| 96 | symOf_index : ∀ {n : ℕ} (R : L.Relations n), symOf (index R) = ⟨n, R⟩ |
| 97 | /-- Numbering the symbol with a given number gives that number back. -/ |
| 98 | index_symOf : ∀ i : Fin numSyms, index (symOf i).2 = i |
| 99 | |
| 100 | namespace FinVocab |
| 101 | |
| 102 | variable {L : Language.{0, 0}} (V : FinVocab L) |
| 103 | |
| 104 | /-- The arity of the symbol with a given number. -/ |
| 105 | abbrev arity (i : Fin V.numSyms) : ℕ := (V.symOf i).1 |
| 106 | |
| 107 | /-- The symbol with a given number. -/ |
| 108 | abbrev sym (i : Fin V.numSyms) : L.Relations (V.arity i) := (V.symOf i).2 |
| 109 | |
| 110 | end FinVocab |
| 111 | |
| 112 | /-- A **concrete finite structure** over the finitely presented vocabulary |
| 113 | `V`: a universe size and a table of Booleans, one row per relation symbol. |
| 114 | |
| 115 | The universe is `Fin (univSize + 1)`, so it is nonempty by construction; the |
| 116 | row of an `n`-ary symbol is read at the number of the tuple, little-endian in |
| 117 | base `card`. Anything out of range reads `false`, so every pair of a number |
| 118 | and a list of lists of Booleans denotes a structure. -/ |
| 119 | structure FinStruct {L : Language.{0, 0}} (V : FinVocab L) where |
| 120 | /-- One less than the size of the universe. -/ |
| 121 | univSize : ℕ |
| 122 | /-- The tables of the relations, one row per symbol. -/ |
| 123 | table : List (List Bool) |
| 124 | |
| 125 | namespace FinStruct |
| 126 | |
| 127 | variable {L : Language.{0, 0}} {V : FinVocab L} |
| 128 | |
| 129 | /-- The size of the universe of a concrete finite structure. -/ |
| 130 | abbrev card (s : FinStruct V) : ℕ := s.univSize + 1 |
| 131 | |
| 132 | /-- The universe of a concrete finite structure: nonempty and linearly ordered |
| 133 | by construction. -/ |
| 134 | abbrev Univ (s : FinStruct V) : Type := Fin s.card |
| 135 | |
| 136 | /-- The table lookup: does the relation `R` hold of the tuple `x`? -/ |
| 137 | def relMapBool (s : FinStruct V) {n : ℕ} (R : L.Relations n) (x : Fin n → s.Univ) : Bool := |
| 138 | (s.table.getD (V.index R) []).getD (tupleIdx s.card (List.ofFn fun j => (x j : ℕ))) false |
| 139 | |
| 140 | /-- **The structure a piece of data denotes.** -/ |
| 141 | instance instStructure [L.IsRelational] (s : FinStruct V) : L.Structure s.Univ where |
| 142 | funMap f := isEmptyElim f |
| 143 | RelMap R x := s.relMapBool R x = true |
| 144 | |
| 145 | /-- The concrete structure over a universe `Fin (k + 1)` whose relations are |
| 146 | given by the Boolean function `f`. -/ |
| 147 | def ofTable (V : FinVocab L) (k : ℕ) |
| 148 | (f : ∀ {n : ℕ}, L.Relations n → (Fin n → Fin (k + 1)) → Bool) : FinStruct V where |
| 149 | univSize := k |
| 150 | table := List.ofFn fun i : Fin V.numSyms => |
| 151 | (List.range ((k + 1) ^ V.arity i)).map fun t => |
| 152 | f (V.sym i) fun j => ⟨digitAt (k + 1) t j, Nat.mod_lt _ (Nat.succ_pos k)⟩ |
| 153 | |
| 154 | /-- The coding of a concrete finite structure as a pair. -/ |
| 155 | def equivProd (V : FinVocab L) : FinStruct V ≃ ℕ × List (List Bool) where |
| 156 | toFun s := (s.univSize, s.table) |
| 157 | invFun p := ⟨p.1, p.2⟩ |
| 158 | left_inv := fun ⟨_, _⟩ => rfl |
| 159 | right_inv := fun _ => rfl |
| 160 | |
| 161 | /-- **Concrete finite structures are a `Primcodable` type**: the object |
| 162 | `ComputablePred` and `REPred` are defined on. -/ |
| 163 | instance instPrimcodable (V : FinVocab L) : Primcodable (FinStruct V) := |
| 164 | Primcodable.ofEquiv _ (equivProd V) |
| 165 | |
| 166 | end FinStruct |
| 167 | |
| 168 | open FirstOrder Language Structure |
| 169 | |
| 170 | variable {L : Language.{0, 0}} [L.IsRelational] |
| 171 | |
| 172 | /-- **The set of concrete instances a decision problem denotes.** This is the |
| 173 | object `ComputablePred` and `REPred` are about: a problem is an |
| 174 | isomorphism-closed property of finite structures, and the numbering of |
| 175 | `FirstOrder.Language.FinStruct` turns it into a property of a `Primcodable` |
| 176 | type, with nothing to write per problem. -/ |
| 177 | def DecisionProblem.toPred (P : DecisionProblem L) (V : FinVocab L) : |
| 178 | FinStruct V → Prop := fun s => P s.Univ |
| 179 | |
| 180 | open FirstOrder |
| 181 | |
| 182 | open FirstOrder.Language |
| 183 | |
| 184 | namespace FinVocab |
| 185 | |
| 186 | variable {L L' : Language.{0, 0}} |
| 187 | |
| 188 | /-- **A numbering of the symbols is a presentation**, the converse of |
| 189 | `FirstOrder.Language.FinVocab.symEquiv`. -/ |
| 190 | def ofEquivSigma (k : ℕ) (e : Fin k ≃ ((n : ℕ) × L.Relations n)) : FinVocab L where |
| 191 | numSyms := k |
| 192 | symOf := e |
| 193 | index R := e.symm ⟨_, R⟩ |
| 194 | symOf_index R := e.apply_symm_apply _ |
| 195 | index_symOf i := by simp |
| 196 | |
| 197 | /-- **A vocabulary presented by a list of all its symbols**, without |
| 198 | repetitions: the way the vocabularies of the catalog, which are finite |
| 199 | enumerations, are presented. -/ |
| 200 | def ofList [DecidableEq ((n : ℕ) × L.Relations n)] (l : List ((n : ℕ) × L.Relations n)) |
| 201 | (nd : l.Nodup) (h : ∀ p : (n : ℕ) × L.Relations n, p ∈ l) : FinVocab L := |
| 202 | ofEquivSigma l.length (List.Nodup.getEquivOfForallMemList l nd h) |
| 203 | |
| 204 | end FinVocab |
| 205 | |
| 206 | open Lax904597.Machines Lax624099.FiniteSatisfiability Lax624099.CodeHalting |
| 207 | |
| 208 | instance instDecidableEqSigmaNatRelationsTuring : DecidableEq ((n : ℕ) × turing.Relations n) := by |
| 209 | show DecidableEq ((n : ℕ) × turingRel n) |
| 210 | infer_instance |
| 211 | |
| 212 | instance instDecidableEqSigmaNatRelationsFinsat : DecidableEq ((n : ℕ) × finsat.Relations n) := by |
| 213 | show DecidableEq ((n : ℕ) × finsatRel n) |
| 214 | infer_instance |
| 215 | |
| 216 | instance instDecidableEqSigmaNatRelationsCode : DecidableEq ((n : ℕ) × code.Relations n) := by |
| 217 | show DecidableEq ((n : ℕ) × codeRel n) |
| 218 | infer_instance |
| 219 | |
| 220 | /-- **The vocabulary of machine instances, presented**: twelve symbols, six |
| 221 | unary and six binary. -/ |
| 222 | def turingVocab : FinVocab turing := |
| 223 | FinVocab.ofList |
| 224 | [⟨1, .posn⟩, ⟨1, .tr⟩, ⟨1, .start⟩, ⟨1, .acc⟩, ⟨1, .blank⟩, ⟨1, .right⟩, |
| 225 | ⟨2, .le⟩, ⟨2, .tsrc⟩, ⟨2, .tread⟩, ⟨2, .tdst⟩, ⟨2, .twrite⟩, ⟨2, .inp⟩] |
| 226 | (by decide) (by rintro ⟨n, R⟩; cases R <;> simp) |
| 227 | |
| 228 | /-- **The vocabulary of first-order sentences as instances, presented**: |
| 229 | fourteen symbols of arity at most three. -/ |
| 230 | def finsatVocab : FinVocab finsat := |
| 231 | FinVocab.ofList |
| 232 | [⟨2, .le⟩, ⟨1, .andN⟩, ⟨1, .orN⟩, ⟨1, .allN⟩, ⟨1, .exN⟩, ⟨2, .child⟩, |
| 233 | ⟨2, .bind⟩, ⟨3, .eqL⟩, ⟨3, .neqL⟩, ⟨2, .posL⟩, ⟨2, .negL⟩, ⟨3, .arg⟩, |
| 234 | ⟨2, .sig⟩, ⟨1, .root⟩] |
| 235 | (by decide) (by rintro ⟨n, R⟩; cases R <;> simp) |
| 236 | |
| 237 | /-- **The vocabulary of code instances, presented**: eleven symbols, nine |
| 238 | unary and two binary. -/ |
| 239 | def codeVocab : FinVocab code := |
| 240 | FinVocab.ofList |
| 241 | [⟨1, .croot⟩, ⟨1, .czero⟩, ⟨1, .csucc⟩, ⟨1, .cleft⟩, ⟨1, .cright⟩, ⟨1, .cpair⟩, |
| 242 | ⟨1, .ccomp⟩, ⟨1, .cprec⟩, ⟨1, .crfind⟩, ⟨2, .carg1⟩, ⟨2, .carg2⟩] |
| 243 | (by decide) (by rintro ⟨n, R⟩; cases R <;> simp) |
| 244 | |
| 245 | end Lax624099.ConcreteInstances |
| 246 |
Used by
Lax624099.CodeHaltingInvarianceLax624099.CodehaltRECompleteLax624099.FiniteSatisfiabilityInvarianceLax624099.FinsatRECompleteLax624099.HaltingInvarianceLax624099.HaltingUndecidableLax624099.HaltRECompleteLax624099.NPSubsetRELax624099.PcpRECompleteLax624099.PcpUndecidableLax624099.PostCorrespondenceInvarianceLax624099.REClosureLax624099.ReductionsComputableLax624099.REFiniteLax624099.REHardUndecidableLax624099.REIsRecursivelyEnumerableLax624099.RENeCoRELax624099.Trakhtenbrot
From Mathlib
Mathlib.Algebra.BigOperators.FinprodMathlib.Algebra.Order.BigOperators.Group.FinsetMathlib.Computability.HaltingMathlib.Computability.PartrecCodeMathlib.Computability.Primrec.ListMathlib.Computability.REMathlib.Data.Finite.SigmaMathlib.Data.Fintype.CardMathlib.Data.Fintype.EquivFinMathlib.Data.Fintype.LatticeMathlib.Data.Fintype.PiMathlib.Data.Fintype.PigeonholeMathlib.Data.List.NodupEquivFinMathlib.Data.Prod.LexMathlib.Data.Set.CardMathlib.Data.Set.Finite.LemmasMathlib.Dynamics.FixedPoints.BasicMathlib.Logic.Equiv.Fin.BasicMathlib.Logic.Equiv.ProdMathlib.Logic.Equiv.SumMathlib.Logic.RelationMathlib.ModelTheory.ComplexityMathlib.ModelTheory.OrderMathlib.ModelTheory.SemanticsMathlib.ModelTheory.SyntaxMathlib.Order.Lattice.NatMathlib.Order.PiLexMathlib.SetTheory.Cardinal.FiniteMathlib.Tactic.FinCasesMathlib.Tactic.Ring
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments