AdditionGraphDegree.lean

1 import RealizationBoundaries.CanonicalOperationDegree
2 
3 /-! # Total function graph oracles and exact operation degrees -/
4 set_option autoImplicit false
5 set_option backward.isDefEq.respectTransparency false
6 noncomputable section
7 namespace RealizationBoundaries
8 
9 /-- The ordinary membership oracle for the graph of a total natural function. -/
10 def operationGraphOracle (op : ℕ → ℕ) (k : ℕ) : Bool :=
11   decide (op k.unpair.1 = k.unpair.2)
12 
13 /-- A total function is computed from its graph by a terminating positive
14 search for the unique output. -/
15 theorem operationGraph_computes_function (op : ℕ → ℕ) :
16     OracleComputable (operationGraphOracle op) op := by
17   let test : ℕ → ℕ := fun k => if op k.unpair.1 = k.unpair.2 then 0 else 1
18   have ht : OracleComputable (operationGraphOracle op) test := by
19     exact (OracleComputable.oracle.isZero).of_eq (fun k => by
20       by_cases h : op k.unpair.1 = k.unpair.2 <;> simp [test, operationGraphOracle, h])
21   have total : ∀ n, ∃ t, test (Nat.pair n t) = 0 := by
22     intro n
23     exact ⟨op n, by simp [test]⟩
24   apply (OracleComputable.find ht total).of_eq
25   intro n
26   have hh := Nat.find_spec (total n)
27   have he : op n = Nat.find (total n) := by simpa [test] using hh
28   exact he.symm
29 
30 /-- Computing a function computes its graph by a finite equality test. -/
31 theorem operationGraph_reduces_of_computable (op : ℕ → ℕ) (X : ℕ → Bool)
32     (hop : OracleComputable X op) : SelectorReducible (operationGraphOracle op) X := by
33   apply RecursiveIn.iff_nat.mpr
34   have hh := (hop.comp OracleComputable.left).ncEq OracleComputable.right
35   exact hh.of_eq (fun k => by simp [operationGraphOracle])
36 
37 /-- The graph and operation conventions define the same relative total
38 computability contract. -/
39 theorem operationGraph_reducible_iff (op : ℕ → ℕ) (X : ℕ → Bool) :
40     SelectorReducible (operationGraphOracle op) X ↔ OracleComputable X op := by
41   constructor
42   · intro h
43     exact (operationGraph_computes_function op).change_oracle h
44   · exact operationGraph_reduces_of_computable op X
45 
46 /-- The graph of the fixed canonical addition operation has exactly the selector
47 oracle's Turing degree, in the official native relation. -/
48 theorem canonicalPairedAddition_graph_equivalent (a : ℕ → Bool) :
49     TuringEquivalent (selectorOracle (operationGraphOracle (canonicalPairedAddition a)))
50       (selectorOracle a) := by
51   constructor
52   · exact operationGraph_reduces_of_computable _ a
53       ((canonicalPairedAddition_oracle_iff a a).mpr (TuringReducible.refl _))
54   · exact (canonicalPairedAddition_oracle_iff a _).mp
55       (operationGraph_computes_function _)
56 
57 /-- Equivalently, the operation graph is computable in exactly the oracles that
58 compute the selector. -/
59 theorem canonicalPairedAddition_graph_oracle_iff (a X : ℕ → Bool) :
60     SelectorReducible (operationGraphOracle (canonicalPairedAddition a)) X ↔
61       SelectorReducible a X :=
62   (operationGraph_reducible_iff _ _).trans (canonicalPairedAddition_oracle_iff a X)
63 
64 end RealizationBoundaries

Back to source controls