feat(computability): strong reducibility and degrees (leanprover-comm…

…unity#1203) Co-authored-by: Mario Carneiro <[email protected]> Co-authored-by: Jeremy Avigad <[email protected]>
jsm28 · Apr 16, 2020 · c3d943e · c3d943e
1 parent a113d6e
commit c3d943e
Show file tree

Hide file tree

Showing 6 changed files with 448 additions and 6 deletions.
diff --git a/docs/references.bib b/docs/references.bib
@@ -189,3 +189,38 @@ @book {atiyah-macdonald
   MRNUMBER = {0242802},
 MRREVIEWER = {J. A. Johnson},
 }
+
+@book {soare1987,
+    AUTHOR = {Soare, Robert I.},
+     TITLE = {Recursively enumerable sets and degrees},
+    SERIES = {Perspectives in Mathematical Logic},
+      NOTE = {A study of computable functions and computably generated sets},
+ PUBLISHER = {Springer-Verlag, Berlin},
+      YEAR = {1987},
+     PAGES = {xviii+437},
+      ISBN = {3-540-15299-7},
+   MRCLASS = {03-02 (03D20 03D25 03D30)},
+  MRNUMBER = {882921},
+MRREVIEWER = {Peter G. Hinman},
+       DOI = {10.1007/978-3-662-02460-7}
+}
+
+@inproceedings{carneiro2019,
+  author    = {Mario M. Carneiro},
+  editor    = {John Harrison and
+               John O'Leary and
+               Andrew Tolmach},
+  title     = {Formalizing Computability Theory via Partial Recursive Functions},
+  booktitle = {10th International Conference on Interactive Theorem Proving, {ITP}
+               2019, September 9-12, 2019, Portland, OR, {USA}},
+  series    = {LIPIcs},
+  volume    = {141},
+  pages     = {12:1--12:17},
+  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
+  year      = {2019},
+  url       = {https://doi.org/10.4230/LIPIcs.ITP.2019.12},
+  doi       = {10.4230/LIPIcs.ITP.2019.12},
+  timestamp = {Fri, 27 Sep 2019 15:57:06 +0200},
+  biburl    = {https://dblp.org/rec/conf/itp/Carneiro19.bib},
+  bibsource = {dblp computer science bibliography, https://dblp.org}
+}
diff --git a/src/computability/halting.lean b/src/computability/halting.lean
@@ -2,12 +2,20 @@
 Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Mario Carneiro
-
-More partial recursive functions using a universal program;
-Rice's theorem and the halting problem.
 -/
+
 import computability.partrec_code
 
+/-!
+# Computability theory and the halting problem
+
+A universal partial recursive function, Rice's theorem, and the halting problem.
+
+## References
+
+* [Mario Carneiro, *Formalizing computability theory via partial recursive functions*][carneiro2019]
+-/
+
 open encodable denumerable
 
 namespace nat.partrec

diff --git a/src/computability/partrec.lean b/src/computability/partrec.lean
@@ -2,13 +2,22 @@
 Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Mario Carneiro
+-/
+
+import computability.primrec data.pfun
+
+/-!
+# The partial recursive functions
 
 The partial recursive functions are defined similarly to the primitive
 recursive functions, but now all functions are partial, implemented
 using the `roption` monad, and there is an additional operation, called
 μ-recursion, which performs unbounded minimization.
+
+## References
+
+* [Mario Carneiro, *Formalizing computability theory via partial recursive functions*][carneiro2019]
 -/
-import computability.primrec data.pfun
 
 open encodable denumerable roption
 

diff --git a/src/computability/partrec_code.lean b/src/computability/partrec_code.lean
@@ -51,6 +51,12 @@ protected def const : ℕ → code
 | 0     := zero
 | (n+1) := comp succ (const n)
 
+theorem injective_const : Π {n₁ n₂}, nat.partrec.code.const n₁ = nat.partrec.code.const n₂ → n₁ = n₂
+| 0 0 h := by simp
+| (n₁+1) (n₂+1) h := by { dsimp [nat.partrec.code.const] at h, 
+                          injection h with h₁ h₂, 
+                          simp only [injective_const h₂] }
+
 protected def id : code := pair left right
 
 def curry (c : code) (n : ℕ) : code :=
@@ -506,6 +512,16 @@ theorem curry_prim : primrec₂ curry :=
 comp_prim.comp primrec.fst $
 pair_prim.comp (const_prim.comp primrec.snd) (primrec.const code.id)
 
+theorem injective_curry {c₁ c₂ n₁ n₂} (h : curry c₁ n₁ = curry c₂ n₂) : c₁ = c₂ ∧ n₁ = n₂ :=
+⟨by injection h, by { injection h, 
+                      injection h with h₁ h₂, 
+                      injection h₂ with h₃ h₄, 
+                      exact injective_const h₃ }⟩
+
+theorem smn : ∃ f : code → ℕ → code, 
+  computable₂ f ∧ ∀ c n x, eval (f c n) x = eval c (mkpair n x) := 
+⟨curry, primrec₂.to_comp curry_prim, eval_curry⟩
+
 theorem exists_code {f : ℕ →. ℕ} : nat.partrec f ↔ ∃ c : code, eval c = f :=
 ⟨λ h, begin
   induction h,

diff --git a/src/computability/primrec.lean b/src/computability/primrec.lean
@@ -2,9 +2,14 @@
 Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Mario Carneiro
+-/
+import data.equiv.list
+
+/-!
+# The primitive recursive functions
 
 The primitive recursive functions are the least collection of functions
-nat → nat which are closed under projections (using the mkpair
+`nat → nat` which are closed under projections (using the mkpair
 pairing function), composition, zero, successor, and primitive recursion
 (i.e. nat.rec where the motive is C n := nat).
 
@@ -14,8 +19,11 @@ which we implement through the type class `encodable`. (More precisely,
 we need that the composition of encode with decode yields a
 primitive recursive function, so we have the `primcodable` type class
 for this.)
+
+## References
+
+* [Mario Carneiro, *Formalizing computability theory via partial recursive functions*][carneiro2019]
 -/
-import data.equiv.list
 
 open denumerable encodable