Halting of a drawn partial recursive code
Lax624099.CodeHalting · concepts/Lax624099/CodeHalting.lean · lax-624099
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
An instance is the syntax tree of a partial recursive code of Mathlib, drawn with one element per node: a node carries one of the eight constructor marks, zero, successor, left, right, pair, composition, primitive recursion and unbounded search, its children are given by two binary relations, and one node is marked as the root. A node decodes to a code by recursion on the code: it carries the code's constructor mark and its children decode to the constructor's arguments. CODEHALT is the decision problem of the structures isomorphic to one whose root decodes to a code that halts on input zero.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.Computability.PartrecCode |
| 2 | import Mathlib.ModelTheory.Semantics |
| 3 | import Mathlib.ModelTheory.Complexity |
| 4 | import Mathlib.Tactic.FinCases |
| 5 | import Lax904597.Classes |
| 6 | import Lax624099.Problems |
| 7 | |
| 8 | /-! |
| 9 | --- |
| 10 | title: Halting of a drawn partial recursive code |
| 11 | type: definition |
| 12 | --- |
| 13 | An instance is the syntax tree of a partial recursive code of Mathlib, |
| 14 | drawn with one element per node: a node carries one of the eight constructor |
| 15 | marks, zero, successor, left, right, pair, composition, primitive recursion |
| 16 | and unbounded search, its children are given by two binary relations, and |
| 17 | one node is marked as the root. A node decodes to a code by recursion on the |
| 18 | code: it carries the code's constructor mark and its children decode to the |
| 19 | constructor's arguments. CODEHALT is the decision problem of the structures |
| 20 | isomorphic to one whose root decodes to a code that halts on input zero. |
| 21 | -/ |
| 22 | |
| 23 | namespace Lax624099.CodeHalting |
| 24 | |
| 25 | open FirstOrder |
| 26 | |
| 27 | open FirstOrder.Language |
| 28 | |
| 29 | /-- Relation symbols of code instances. -/ |
| 30 | inductive codeRel : ℕ → Type |
| 31 | /-- `croot n`: `n` is the root of the syntax tree. -/ |
| 32 | | croot : codeRel 1 |
| 33 | /-- `czero n`: `n` draws the constructor `zero`. -/ |
| 34 | | czero : codeRel 1 |
| 35 | /-- `csucc n`: `n` draws the constructor `succ`. -/ |
| 36 | | csucc : codeRel 1 |
| 37 | /-- `cleft n`: `n` draws the constructor `left`. -/ |
| 38 | | cleft : codeRel 1 |
| 39 | /-- `cright n`: `n` draws the constructor `right`. -/ |
| 40 | | cright : codeRel 1 |
| 41 | /-- `cpair n`: `n` draws the constructor `pair`. -/ |
| 42 | | cpair : codeRel 1 |
| 43 | /-- `ccomp n`: `n` draws the constructor `comp`. -/ |
| 44 | | ccomp : codeRel 1 |
| 45 | /-- `cprec n`: `n` draws the constructor `prec`. -/ |
| 46 | | cprec : codeRel 1 |
| 47 | /-- `crfind n`: `n` draws the constructor `rfind'`. -/ |
| 48 | | crfind : codeRel 1 |
| 49 | /-- `carg1 n m`: `m` is the first child of `n`. -/ |
| 50 | | carg1 : codeRel 2 |
| 51 | /-- `carg2 n m`: `m` is the second child of `n`. -/ |
| 52 | | carg2 : codeRel 2 |
| 53 | deriving DecidableEq |
| 54 | |
| 55 | /-- The relational language of code instances: the eight constructor marks, |
| 56 | the mark of the root, and the two child relations. -/ |
| 57 | def code : Language := |
| 58 | ⟨fun _ => Empty, codeRel⟩ |
| 59 | |
| 60 | instance instIsRelationalCode : IsRelational code := |
| 61 | fun _ => ⟨fun f => Empty.elim f⟩ |
| 62 | |
| 63 | /-- The root symbol. -/ |
| 64 | abbrev cRoot : code.Relations 1 := .croot |
| 65 | |
| 66 | /-- The `zero` symbol. -/ |
| 67 | abbrev cZero : code.Relations 1 := .czero |
| 68 | |
| 69 | /-- The `succ` symbol. -/ |
| 70 | abbrev cSucc : code.Relations 1 := .csucc |
| 71 | |
| 72 | /-- The `left` symbol. -/ |
| 73 | abbrev cLeft : code.Relations 1 := .cleft |
| 74 | |
| 75 | /-- The `right` symbol. -/ |
| 76 | abbrev cRight : code.Relations 1 := .cright |
| 77 | |
| 78 | /-- The `pair` symbol. -/ |
| 79 | abbrev cPair : code.Relations 1 := .cpair |
| 80 | |
| 81 | /-- The `comp` symbol. -/ |
| 82 | abbrev cComp : code.Relations 1 := .ccomp |
| 83 | |
| 84 | /-- The `prec` symbol. -/ |
| 85 | abbrev cPrec : code.Relations 1 := .cprec |
| 86 | |
| 87 | /-- The `rfind'` symbol. -/ |
| 88 | abbrev cRfind : code.Relations 1 := .crfind |
| 89 | |
| 90 | /-- The first-child symbol. -/ |
| 91 | abbrev cArg1 : code.Relations 2 := .carg1 |
| 92 | |
| 93 | /-- The second-child symbol. -/ |
| 94 | abbrev cArg2 : code.Relations 2 := .carg2 |
| 95 | |
| 96 | open FirstOrder |
| 97 | |
| 98 | open Language Structure |
| 99 | |
| 100 | section Shorthands |
| 101 | |
| 102 | variable {A : Type} [code.Structure A] |
| 103 | |
| 104 | /-- Being the root. -/ |
| 105 | def CRoot (a : A) : Prop := RelMap cRoot ![a] |
| 106 | |
| 107 | /-- Drawing the constructor `zero`. -/ |
| 108 | def CZero (a : A) : Prop := RelMap cZero ![a] |
| 109 | |
| 110 | /-- Drawing the constructor `succ`. -/ |
| 111 | def CSucc (a : A) : Prop := RelMap cSucc ![a] |
| 112 | |
| 113 | /-- Drawing the constructor `left`. -/ |
| 114 | def CLeft (a : A) : Prop := RelMap cLeft ![a] |
| 115 | |
| 116 | /-- Drawing the constructor `right`. -/ |
| 117 | def CRight (a : A) : Prop := RelMap cRight ![a] |
| 118 | |
| 119 | /-- Drawing the constructor `pair`. -/ |
| 120 | def CPair (a : A) : Prop := RelMap cPair ![a] |
| 121 | |
| 122 | /-- Drawing the constructor `comp`. -/ |
| 123 | def CComp (a : A) : Prop := RelMap cComp ![a] |
| 124 | |
| 125 | /-- Drawing the constructor `prec`. -/ |
| 126 | def CPrec (a : A) : Prop := RelMap cPrec ![a] |
| 127 | |
| 128 | /-- Drawing the constructor `rfind'`. -/ |
| 129 | def CRfind (a : A) : Prop := RelMap cRfind ![a] |
| 130 | |
| 131 | /-- Being the first child. -/ |
| 132 | def CArg1 (a b : A) : Prop := RelMap cArg1 ![a, b] |
| 133 | |
| 134 | /-- Being the second child. -/ |
| 135 | def CArg2 (a b : A) : Prop := RelMap cArg2 ![a, b] |
| 136 | |
| 137 | end Shorthands |
| 138 | |
| 139 | section Decode |
| 140 | |
| 141 | variable {A : Type} [code.Structure A] |
| 142 | |
| 143 | /-- **The node `n` draws the code `c`.** A recursion on the code: the mark of |
| 144 | the node must be the constructor's, and its children must draw the |
| 145 | constructor's arguments. -/ |
| 146 | def DecodesTo (n : A) : Nat.Partrec.Code → Prop |
| 147 | | .zero => CZero n |
| 148 | | .succ => CSucc n |
| 149 | | .left => CLeft n |
| 150 | | .right => CRight n |
| 151 | | .pair cf cg => |
| 152 | CPair n ∧ ∃ a b, CArg1 n a ∧ CArg2 n b ∧ DecodesTo a cf ∧ DecodesTo b cg |
| 153 | | .comp cf cg => |
| 154 | CComp n ∧ ∃ a b, CArg1 n a ∧ CArg2 n b ∧ DecodesTo a cf ∧ DecodesTo b cg |
| 155 | | .prec cf cg => |
| 156 | CPrec n ∧ ∃ a b, CArg1 n a ∧ CArg2 n b ∧ DecodesTo a cf ∧ DecodesTo b cg |
| 157 | | .rfind' cf => CRfind n ∧ ∃ a, CArg1 n a ∧ DecodesTo a cf |
| 158 | |
| 159 | end Decode |
| 160 | |
| 161 | open Lax904597.Problems Lax624099.Problems |
| 162 | |
| 163 | /-- The root of the instance draws a code halting on `0`. -/ |
| 164 | def CodeHaltsOn (A : Type) [code.Structure A] : Prop := |
| 165 | ∃ (n : A) (c : Nat.Partrec.Code), CRoot n ∧ DecodesTo n c ∧ (Nat.Partrec.Code.eval c 0).Dom |
| 166 | |
| 167 | /-- CODEHALT: does the partial recursive code drawn in the instance halt on |
| 168 | `0`? -/ |
| 169 | def CODEHALT : DecisionProblem code := |
| 170 | DecisionProblem.ofPred CodeHaltsOn |
| 171 | |
| 172 | end Lax624099.CodeHalting |
| 173 |
Builds on
Used by
Lax624099.CodeHaltingInvarianceLax624099.CodehaltRECompleteLax624099.ConcreteInstancesLax624099.FiniteSatisfiabilityInvarianceLax624099.FinsatRECompleteLax624099.HaltingInvarianceLax624099.HaltingUndecidableLax624099.HaltRECompleteLax624099.NPSubsetRELax624099.PcpRECompleteLax624099.PcpUndecidableLax624099.PostCorrespondenceInvarianceLax624099.REClosureLax624099.ReductionsComputableLax624099.REFiniteLax624099.REHardUndecidableLax624099.REIsRecursivelyEnumerableLax624099.RENeCoRELax624099.Trakhtenbrot
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments