I'm trying to teach myself Coq by formalizing formalize a mathematical theorem I'm familiar with: the undecidability of the halting problem various theorems in computability theory.
Since I'm not interested in formalizing the details of computational models (e.g., Turing machines, register machines, lambda calculi, etc.), I'm trying to do this by "teaching Coq Church-Turing thesis", namely, assuming Axioms that state properties of functions that Coq thinks to be computable (i.e., definable functions of type nat -> nat).
For example, if I wanted to tell Coq that there is an effective enumeration of the partial computable functions, I could say
Definition partial := nat -> nat -> option nat.
Axiom Phi : nat -> partial.
Here partial computable functions are thought of as (total) computable functions that, given a first argument s, simulate the computation of the original partial computable functions for s many steps. I could also add other Axioms, like Padding Lemma, and I might be able to prove the undecidability of the halting problem, and some other theorems in computability theory.
My first questions is whether or not I'm on the right track so far. Isn't it the case that what I'm trying to do is obviously impossible for incompleteness phenomena or the nature of the type system of Coq?
My second question is about relativization. If I tried to prove more serious things in computability theory, I would want to consider computation in oracles. Since oftentimes oracles are constructed as limits of partial two-valued functions, it seems (at least naively) natural to make oracles having type nat -> bool. At the same time, for oracles to be nontrivial they have to be non-computable. Considering this, does an oracle having type nat -> bool make sense?
Here is another question about oracles: it would be really nice if, for each oracle, there were the type of partial computable functions relative to that particular oracle. Can I do this by exploiting dependent type system in Coq? Does this possibility depend on the choice some of formalization oracles as discussed in the paragraph above?
EDIT: The approach above surely doesn't work as is, since I need an additional axiom:
Axiom Phi_inverse: partial -> nat.
which should not be true for oracles. Is there an approach like the one I described above (I mean, the one not involving the formalization of computational models) at all?
EDIT: To clarify my intention, I edited the problem statement above. Also, to present the style of formalization I had in mind, I present an incomplete proof of the unsolvability of the halting problem here:
Require Import Arith.
Require Import Classical.
Definition ext_eq (A B : Set) (f g : A -> B) := forall (x : A), f x = g x.
Definition partial := nat -> nat -> option nat.
Axiom Phi : nat -> partial.
Axiom Phi_inverse : partial -> nat.
Axiom effective_enumeration :
forall (f : partial) (e : nat),
Phi e = f <-> Phi_inverse f = e.
Axiom modulus : partial -> nat -> nat.
Axiom persistence :
forall (f : partial) n s,
s >= modulus f n -> f s n = f (modulus f n) n.
Definition limit (f : partial) n := f (modulus f n) n.
Definition total (f : partial)
:= forall n, exists s, exists m, f s n = Some m.
Definition flip n := match n with O => 1 | S _ => 0 end.
Definition K e := exists n, limit (Phi e) e = Some n.
Theorem K_is_undecidable :
~ exists e,
total (Phi e)
/\ forall e', limit (Phi e) e' = Some 0 <-> ~K e'.
Proof.
intro.
destruct H as [e].
destruct H.
pose proof (H0 (Phi_inverse (fun s e' =>
match (Phi e s e') with
| Some n => Some (flip n)
| None => None end))).
(* to be continued *)
First, some clarification:
Functions that Coq thinks to be computable (i.e., definable functions of type nat -> nat)
Strictly speaking, Coq does not think that functions are computable. Coq's logic assert that there are certain functions can be defined, and that you can do certain things with them, but an arbitrary function is a black box as far as Coq is concerned. In particular, it is consistent to postulate the existence of a non-computable function.
Now, to the actual questions. Here's a solution that more or less follows Atsby's answer. We will represent a Turing machine function by a Coq function of type nat -> nat -> option bool. The idea is that the first argument is the input, and the second one is a maximum number of steps we'll run for. The output is None if we fail to produce an answer, and Some b if the computation terminates with producing b as an answer. I took the liberty of using Ssreflect to make the code a bit simpler:
Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool.
Require Import Ssreflect.ssrnat Ssreflect.choice.
Section Halting.
(* [code f c] holds if [f] is representable by some
Turing machine code [c]. Notice that we don't assume that
[code] is computable, nor do we assume that all functions
[nat -> nat -> option bool] can be represented by some code,
which means that we don't rule out the existence of
non-computable functions. *)
Variable code : (nat -> nat -> option bool) -> nat -> Prop.
(* We assume that we have a [decider] for the halting problem, with
its specification given by [deciderP]. Specifically, when running
on a number [m] that represents a pair [(c, n)], where [c] is the
code for some Turing machine [f] and [n] some input for [f], we
know that [decider m] will halt at some point, producing [true] iff
[f] halts on input [n].
This definition uses a few convenience features from Ssreflect to
make our lives simpler, namely, the [pickle] function, that
converts from [nat * nat] to [nat], and the implicit coercion from
[option] to [bool] ([Some] is mapped to [true], [None] to [false]) *)
Variable decider : nat -> nat -> option bool.
Hypothesis deciderP :
forall f c, code f c ->
forall (n : nat),
(forall s,
match decider (pickle (c, n)) s with
| Some true => exists s', f n s'
| Some false => forall s', negb (f n s')
| None => True
end) /\
exists s, decider (pickle (c, n)) s.
(* Finally, we define the usual diagonal function, and postulate that
it is representable by some code [f_code]. *)
Definition f (n : nat) s :=
match decider (pickle (n, n)) s with
| Some false => Some false
| _ => None
end.
Variable f_code : nat.
Hypothesis f_codeP : code f f_code.
(* The actual proof is straightforward (8 lines long).
I'm omitting it to avoid spoiling the fun. *)
Lemma pandora : False.
Proof. (* ... *) Qed.
End Halting.
In summary, it is perfectly reasonable to use Coq functions to talk about the Halting problem, and the result is quite simple. Notice that the above theorem doesn't force code to be related to Turing machines at all -- for instance, you could interpret the above theorem as saying that the halting problem for oracle Turing machines cannot be solved by an oracle Turing machine. In the end, what makes these results different from each other is the formalization of the underlying computation model, which is exactly what you wanted to avoid.
As for the template you were trying to start with, assuming that Phi exists and has an inverse already results in a contradiction. This is the usual diagonal argument:
Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool.
Require Import Ssreflect.ssrnat Ssreflect.choice.
Definition partial := nat -> nat -> option nat.
Axiom Phi : nat -> partial.
Axiom Phi_inverse : partial -> nat.
Axiom effective_enumeration :
forall (f : partial) (e : nat),
Phi e = f <-> Phi_inverse f = e.
Lemma pandora : False.
Proof.
pose f n (m : nat) :=
if Phi n n n is Some p then None
else Some 0.
pose f_code := Phi_inverse f.
move/effective_enumeration: (erefl f_code) => P.
move: (erefl (f f_code f_code)).
rewrite {1}/f P.
by case: (f _ _).
Qed.
The problem is that even though externally we know that Coq-definable functions are in bijection with nat, we cannot assert this fact internally. Asserting the existence of a non-effective code relation solves this issue.
As for oracles, having an oracle be a function of type nat -> bool does make sense, but you need to make sure that you are not violating other assumptions that you have in the proof by doing this. For instance, you can postulate that all nat -> nat functions are computable, by axiomatizing that you have a function like your Phi, but that would mean that your oracle would also be computable. Using a relation like code above allows you to have somewhat the best of both worlds.
Finally, as for relativization results, it depends a lot on what you want to prove. For instance, if you just want to show that certain functions over oracles can be written, you can write a parametric function and show that it has a certain property when the oracle has a certain behavior, without the need for dependent types. E.g.
Definition foo (oracle : nat -> bool) (n : nat) : bool :=
(* some definition ... *).
Definition oracle_spec (oracle : nat -> bool) : Prop :=
(* some definition ... *).
Lemma fooP oracle :
oracle_spec oracle ->
(* some property of [foo oracle]. *)
Finally, here's an interesting link discussing Church's thesis in dependent type theory, which you may find interesting: https://existentialtype.wordpress.com/2012/08/09/churchs-law/