feat(Computability): define oracle computability and Turing degrees #20219
+355
−0
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
tannerduve
changed the title
| A partial function `f` is partial recursive if and only if | ||
| it is recursive in the constant zero function. | ||
| -/ | ||
| lemma partrec_iff_partrec_in_zero |
There was a problem hiding this comment.
Perhaps the definition of Nat.Partrec should be changed to this, otherwise there's unnecessary duplication.
There was a problem hiding this comment.
Going to add an alternative definition, Partrec_0, defined in this way
There was a problem hiding this comment.
That's not a good solution, it would just mean we have two duplicate definitions
There was a problem hiding this comment.
Is it best to just remove these equivalence lemmas then? I don't want to mess too much with the existing computability set up. These lemmas end up being useful for some proofs I'm currently working on.
Command-Master
added
the
awaiting-author
eric-wieser
reviewed
Dec 24, 2024
eric-wieser
reviewed
Dec 24, 2024
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
eric-wieser
reviewed
Dec 24, 2024
Comment on lines
+102
to
+105
| lemma partrec_implies_recursive_in_everything | ||
| (f : ℕ →. ℕ) : Nat.Partrec f → (∀ g, RecursiveIn f g) := by | ||
| intro pF | ||
| intro g |
There was a problem hiding this comment.
This can be renamed to allow for dot-notation
Suggested change
| lemma partrec_implies_recursive_in_everything | |
| (f : ℕ →. ℕ) : Nat.Partrec f → (∀ g, RecursiveIn f g) := by | |
| intro pF | |
| intro g | |
| lemma Nat.Partrec.recursiveIn (f : ℕ →. ℕ) (pF : Nat.Partrec f) (g : ℕ →. ℕ) : RecursiveIn f g := by |
Comment on lines
+128
to
+130
| lemma partrec_in_zero_implies_partrec | ||
| (f : ℕ →. ℕ) : RecursiveIn f (fun _ => Part.some 0) → Nat.Partrec f := by | ||
| intro fRecInZero |
There was a problem hiding this comment.
This can be renamed to allow for dot-notation
Suggested change
| lemma partrec_in_zero_implies_partrec | |
| (f : ℕ →. ℕ) : RecursiveIn f (fun _ => Part.some 0) → Nat.Partrec f := by | |
| intro fRecInZero | |
| lemma RecursiveIn.partrec_of_zero (f : ℕ →. ℕ) (fRecInZero : RecursiveIn f fun _ => Part.some 0) : | |
| Nat.Partrec f := by |
Comment on lines
+171
to
+178
| theorem partrec_iff_partrec_in_everything | ||
| (f : ℕ →. ℕ) : Nat.Partrec f ↔ (∀ g, RecursiveIn f g) := by | ||
| constructor | ||
| · exact partrec_implies_recursive_in_everything f | ||
| · intro H | ||
| have lem : RecursiveIn f (fun _ => Part.some 0) := H (fun _ => Part.some 0) | ||
| have lem : Nat.Partrec f := partrec_in_zero_implies_partrec f lem | ||
| exact lem |
There was a problem hiding this comment.
This is mostly stylistic, but this can be golfed to
Suggested change
| theorem partrec_iff_partrec_in_everything | |
| (f : ℕ →. ℕ) : Nat.Partrec f ↔ (∀ g, RecursiveIn f g) := by | |
| constructor | |
| · exact partrec_implies_recursive_in_everything f | |
| · intro H | |
| have lem : RecursiveIn f (fun _ => Part.some 0) := H (fun _ => Part.some 0) | |
| have lem : Nat.Partrec f := partrec_in_zero_implies_partrec f lem | |
| exact lem | |
| theorem partrec_iff_partrec_in_everything (f : ℕ →. ℕ) : Nat.Partrec f ↔ ∀ g, RecursiveIn f g := | |
| ⟨(·.recursiveIn), (· _ |>.partrec_of_zero)⟩ |
Comment on lines
+190
to
+191
| theorem TuringEquivalent.refl (f : ℕ →. ℕ) : f ≡ᵀ f := | ||
| ⟨RecursiveIn.refl f, RecursiveIn.refl f⟩ |
There was a problem hiding this comment.
If you provide an IsRefl instance for RecursiveIn this can be antisymmRel_refl
Comment on lines
+196
to
+198
| @[symm] | ||
| theorem TuringEquivalent.symm {f g : ℕ →. ℕ} (h : f ≡ᵀ g) : g ≡ᵀ f := | ||
| ⟨h.2, h.1⟩ |
There was a problem hiding this comment.
This can be AntisymmRel.symm
Comment on lines
+294
to
+355
| /-- | ||
| For any partial functions `a`, `b₁`, and `b₂`, if `b₁` is Turing equivalent to `b₂`, | ||
| then `a` is Turing reducible to `b₁` if and only if `a` is Turing reducible to `b₂`. | ||
| -/ | ||
| lemma reduce_lifts₁ : ∀ (a b₁ b₂ : ℕ →. ℕ), b₁≡ᵀb₂ → (RecursiveIn a b₁) = (RecursiveIn a b₂) := by | ||
| intros a b₁ b₂ bEqb | ||
| apply propext | ||
| constructor | ||
| · intro aRedb₁ | ||
| apply RecursiveIn.trans aRedb₁ bEqb.1 | ||
| · intro aRedb₂ | ||
| apply RecursiveIn.trans aRedb₂ bEqb.2 | ||
|
|
||
| /-- | ||
| For any partial functions `f`, `g`, and `h`, if `f` is Turing equivalent to `g`, | ||
| then `f` is Turing reducible to `h` if and only if `g` is Turing reducible to `h`. | ||
| -/ | ||
| lemma reduce_lifts₂ : ∀ (f g h : ℕ →. ℕ), | ||
| f ≡ᵀ g → (RecursiveIn f h = RecursiveIn g h) := by | ||
| intros f g h fEqg | ||
| apply propext | ||
| constructor | ||
| · intro fRedh | ||
| apply RecursiveIn.trans fEqg.2 fRedh | ||
| · intro gRedh | ||
| apply RecursiveIn.trans fEqg.1 gRedh | ||
|
|
||
| /-- | ||
| Here we show how to lift the Turing reducibility relation from | ||
| partial functions to their Turing degrees, using the above lemmas. | ||
| -/ | ||
| def TuringDegree.turing_red (d₁ d₂ : TuringDegree) : Prop := | ||
| @Quot.lift₂ _ _ Prop (TuringEquivalent) | ||
| (TuringEquivalent) (RecursiveIn) (reduce_lifts₁) (reduce_lifts₂) d₁ d₂ | ||
|
|
||
| /-- | ||
| Instance declaring that `TuringDegree.turing_red` is a partial order. | ||
| -/ | ||
| instance : PartialOrder TuringDegree where | ||
| le := TuringDegree.turing_red | ||
| le_refl := by | ||
| apply Quot.ind | ||
| intro a | ||
| apply RecursiveIn.refl | ||
| le_trans := by | ||
| apply Quot.ind | ||
| intro a | ||
| apply Quot.ind | ||
| intro b | ||
| apply Quot.ind | ||
| intro c | ||
| exact RecursiveIn.trans | ||
| le_antisymm := by | ||
| apply Quot.ind | ||
| intro a | ||
| apply Quot.ind | ||
| intro b | ||
| intros aRedb bReda | ||
| apply Quot.sound | ||
| constructor | ||
| · exact aRedb | ||
| · exact bReda |
There was a problem hiding this comment.
All of this can be rewritten to use existing Antisymmetrization stuff, like
instance : PartialOrder TuringDegree :=
@instPartialOrderAntisymmetrization (ℕ →. ℕ)
{le := RecursiveIn, le_refl := .refl, le_trans _ _ _ := RecursiveIn.trans}
Comment on lines
+207
to
+239
| induction hg | ||
| case zero => | ||
| apply RecursiveIn.zero | ||
| case succ => | ||
| apply RecursiveIn.succ | ||
| case left => | ||
| apply RecursiveIn.left | ||
| case right => | ||
| apply RecursiveIn.right | ||
| case oracle => | ||
| exact hh | ||
| case pair f' h' _ _ hf_ih hh_ih => | ||
| apply RecursiveIn.pair | ||
| · apply hf_ih | ||
| apply hh | ||
| · apply hh_ih | ||
| apply hh | ||
| case comp f' h' _ _ hf_ih hh_ih => | ||
| apply RecursiveIn.comp | ||
| · apply hf_ih | ||
| apply hh | ||
| · apply hh_ih | ||
| apply hh | ||
| case prec f' h' _ _ hf_ih hh_ih => | ||
| apply RecursiveIn.prec | ||
| · apply hf_ih | ||
| apply hh | ||
| · apply hh_ih | ||
| apply hh | ||
| case rfind f' _ hf_ih => | ||
| apply RecursiveIn.rfind | ||
| · apply hf_ih | ||
| apply hh |
There was a problem hiding this comment.
The indentation of this is incorrect, it should be indented by two spaces
Comment on lines
+203
to
+206
| @[trans] | ||
| theorem RecursiveIn.trans {f g h : ℕ →. ℕ} : | ||
| RecursiveIn f g → RecursiveIn g h → RecursiveIn f h := by | ||
| intro hg hh |
There was a problem hiding this comment.
In general instead of writing function types and then using intro you can introduce values directly as arguments - often this is cleaner.
Suggested change
| @[trans] | |
| theorem RecursiveIn.trans {f g h : ℕ →. ℕ} : | |
| RecursiveIn f g → RecursiveIn g h → RecursiveIn f h := by | |
| intro hg hh | |
| @[trans] | |
| theorem RecursiveIn.trans {f g h : ℕ →. ℕ} (hg : RecursiveIn f g) (hh : RecursiveIn g h) : | |
| RecursiveIn f h := by |
Comment on lines
+244
to
+247
| theorem TuringEquivalent.trans : | ||
| Transitive TuringEquivalent := | ||
| fun _ _ _ ⟨fg₁, fg₂⟩ ⟨gh₁, gh₂⟩ => | ||
| ⟨RecursiveIn.trans fg₁ gh₁, RecursiveIn.trans gh₂ fg₂⟩ |
There was a problem hiding this comment.
If you provide an IsTrans instance for RecursiveIn this can be AntisymmRel.trans
Comment on lines
+252
to
+257
| instance : Equivalence TuringEquivalent := | ||
| { | ||
| refl := TuringEquivalent.refl, | ||
| symm := TuringEquivalent.symm, | ||
| trans := @TuringEquivalent.trans | ||
| } |
There was a problem hiding this comment.
If you provide an IsPreorder instance for RecursiveIn this can be (AntisymmRel.setoid _ _).iseqv
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Some initial definitions introducing a model of oracle computability via partial recursive functions, define Turing reducibility and equivalence, and prove that Turing equivalence is an equivalence relation. Define the type of Turing degrees as equivalence classes under Turing equivalence. This PR includes:
RecursiveIn g f: An inductive definition representing that a partial functionfis recursive in oracleg.turing_reducible: A relation defining Turing reducibility between partial functions.turing_equivalent: A relation defining Turing equivalence between partial functions.TuringDegree: The type of Turing degrees, defined as equivalence classes underturing_equivalent.Implementation Notes
The type
RecursiveIn g fis inductively defined to include basic functions such aszero,succ, projections, and the oracleg, and is closed under pairing, composition, primitive recursion, and μ-recursion. Thejoinoperation combines two partial functions by mapping even and odd numbers to the respective functions.Notation
f ≤ᵀ g:fis Turing reducible tog.f ≡ᵀ g:fis Turing equivalent tog.f ⊔ g: The join of partial functionsfandg.In Progress
The work here is just the basic definitions for the theory being developed. Some current in-progress work involves proving the upper-semilattice structure of Turing degrees, proving the existence of a relativized universal partial recursive function, and proving properties of the jump operator.
References
Tags
Computability, Oracle, Turing Degrees, Reducibility, Equivalence Relation