Formalizing computability theory in Coq

Question

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 *)

Answer 1

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/

Answer 2

Here's how you would introduce a meaningful axiom (I'm still learning Coq myself so hopefully if I've done this wrong someone will correct me).

With Parameter we are stipulating the existence of a function called compute without giving a definition. With Axiom we are fixing some of its properties (hopefully without introducing a contradiction). Allegedly, Parameter and Axiom do the same thing internally.

Likewise to the declaration of compute, your Axiom Phi stipulates the existence of a function Phi from nat to partial, but you can't do anything with it in Coq yet because it has no known properties. Note that the existence of Phi doesn't imply anything like "there is an effective enumeration of the partial computable functions".

Here the axiom states that, when called with a greater number of allowed steps of computation, compute never changes an ACCEPT into a REJECT or vice versa or backs up to NOTYET. With these definitions, I've checked that it is possible to prove the trivial lemma test as a starter.

Obviously, I haven't carried this through to see if you can prove the undecidability of the halting problem but it should be possible by adding an axiom asserting the existence of a nat representing a program that computes equivalently to the construction required in proof of the halting problem. Of course, largely the entire point of the proof is lost by doing things this way but there'd still be a little bit left to prove.

Inductive result :=
| ACCEPT : result
| REJECT : result
| NOTYET : result.

Definition narrowing a b : Prop :=
(match a with
| ACCEPT => b = ACCEPT
| REJECT => b = REJECT
| NOTYET => True
end).

Parameter compute : nat (* program *) -> nat (* argument *) -> nat (* steps *) -> result.

Axiom compute_narrowing:
forall program input steps steps',
(steps' >= steps) ->
(narrowing (compute program input steps) (compute program input steps')).

Lemma test: ~ exists program input steps, (compute program input steps) = ACCEPT /\ (compute program input (steps + 1)) = NOTYET

EDIT: Here's a bit more. After thinking about the problem a bit, I realize I was definitely wrong that such a proof would necessarily have to axiomize the interesting constructions. One can plug in axioms that allow only simple low-level constructions and build higher-level ones on top of them. I'm assuming the goal is to follow Minsky's proof, as it seems simpler to formalize:

http://www.cs.odu.edu/~toida/nerzic/390teched/computability/unsolv-1.html

Here, additional axioms assert 1) the existence of a program that always accept 2) the existence of a program that always rejects and 3) for any three programs conditional when_accept when_reject, the existence of a program that first runs conditional and then based on that runs when_accept or when_reject (all the subprogram invocations are on the same input given to the composed program). With these axioms, it is possible to prove, for any program target the existence of a program that runs target and then outputs the opposite result (but also looping forever if target loops forever). This "negation" construction is just a simple example, and not one of the constructions used in Minsky's proof.

To follow Minsky's proof, one would need to add further axioms for the existence of a program that loops, and for the copier construction. Then add a definition for when a program is a decider, and prove that there is no decider for the halting problem. The codec axiom saves having to define functions encode_pair and decode_pair in Coq and prove codec as a Lemma. I think the properties of encode_pair and decode_pair will be needed for the copier construction and in the final proof (certainly the definition of a decider for the halting problem would need it as the machine input is a pair).

Require Import List.
Require Import Arith.
Require Import Omega.

Ltac mp_cancel :=
  repeat match goal with
  | [ H2 : ?P -> ?Q , H1 : ?P |- _ ] => specialize (H2 H1)
  end.

Ltac mp_cancel_reflexivity :=
  repeat match goal with
  | [ H1 : ?P = ?P -> ?Q |- _ ] => assert (H_mp_cancel_reflexivity : P = P) by reflexivity; specialize (H1 H_mp_cancel_reflexivity); clear H_mp_cancel_reflexivity
  end.

Inductive result :=
| ACCEPT : result
| REJECT : result
| NOTYET : result
.

Definition narrowing a b : Prop :=
  (match a with
  | ACCEPT => b = ACCEPT
  | REJECT => b = REJECT
  | NOTYET => True
  end)
.

Parameter encode_pair : (nat * nat) -> nat.
Parameter decode_pair : nat -> (nat * nat).

Axiom codec:
  forall a b,
  (decode_pair (encode_pair (a, b))) = (a, b).

Parameter compute : nat (* program *) -> nat (* input *) -> nat (* steps *) -> result.

Axiom compute_narrowing:
  forall program input steps steps',
  (steps' >= steps) -> (narrowing (compute program input steps) (compute program input steps')).

Axiom exists_always_accept:
  exists program_always_accept,
  forall input,
  exists steps,
  (compute program_always_accept input steps) = ACCEPT.

Axiom exists_always_reject:
  exists program_always_reject,
  forall input,
  exists steps,
  (compute program_always_reject input steps) = REJECT.

Definition result_compose_conditional (result_conditional : result) (result_when_accept : result) (result_when_reject : result) : result :=
  (match result_conditional with
  | ACCEPT => result_when_accept
  | REJECT => result_when_reject
  | NOTYET => NOTYET
  end).

Axiom exists_compose_conditional:
  forall program_conditional program_when_accept program_when_reject,
  exists program_composition,
  forall input steps_control steps_when result_conditional result_when_accept result_when_reject,
  (
    ((compute program_conditional input steps_control) = result_conditional) ->
    ((compute program_when_accept input steps_when) = result_when_accept) ->
    ((compute program_when_reject input steps_when) = result_when_reject) ->
    (exists steps_composition, (compute program_composition input steps_composition) = (result_compose_conditional result_conditional result_when_accept result_when_reject))
  ).

Definition result_negation (result_target : result) : result :=
  (match result_target with
  | ACCEPT => REJECT
  | REJECT => ACCEPT
  | NOTYET => NOTYET
  end).

Lemma exists_negation:
  forall program_target,
  exists program_negation,
  forall input steps_target result_target,
  (
    ((compute program_target input steps_target) = result_target) ->
    (exists steps_negation, (compute program_negation input steps_negation) = (result_negation result_target))
  ).
intros.
elim exists_always_accept; intros program_always_accept H_always_accept.
elim exists_always_reject; intros program_always_reject H_always_reject.
elim exists_compose_conditional with (program_conditional := program_target) (program_when_accept := program_always_reject) (program_when_reject := program_always_accept); intros program_negation H_program_negation.
exists program_negation.
intros.
specialize H_always_accept with input. elim H_always_accept; clear H_always_accept; intros steps_accept H_always_accept.
specialize H_always_reject with input. elim H_always_reject; clear H_always_reject; intros steps_reject H_always_reject.
pose (steps_when := (steps_accept + steps_reject)).
specialize H_program_negation with input steps_target steps_when result_target (compute program_always_reject input steps_when) (compute program_always_accept input steps_when).
mp_cancel.
mp_cancel_reflexivity.
elim H_program_negation; clear H_program_negation; intros steps_negation H_program_negation.
exists (steps_negation).
rewrite H_program_negation; clear H_program_negation.
replace (compute program_always_reject input steps_when) with REJECT; symmetry.
replace (compute program_always_accept input steps_when) with ACCEPT; symmetry.
unfold result_compose_conditional.
unfold result_negation.
reflexivity.
assert (T := (compute_narrowing program_always_accept input steps_accept steps_when)).
assert (steps_when >= steps_accept).
unfold steps_when.
omega.
mp_cancel.
unfold narrowing in T.
rewrite H_always_accept in T.
assumption.
assert (T := (compute_narrowing program_always_reject input steps_reject steps_when)).
assert (steps_when >= steps_reject).
unfold steps_when.
omega.
mp_cancel.
unfold narrowing in T.
rewrite H_always_reject in T.
assumption.
Qed.

EDIT#2: I had sort of understood that you wanted to be able to program the constructions in Coq but I hadn't figured out how that could be done at the time of my previous edit. In the following snippet it's done using the axiom exists_program_of_procedure, which asserts that there exists a nat representing a program that has the same behavior as any given procedure (at least for well-behaved procedures that are "narrowing" in their computation). Included is a straightforward formalization of Minsky's proof. Your approach has certainly cleaner axioms and will probably result in shorter proof due to the use of modulus to oracle-ify the steps to stabilization rather than dealing with narrowing. Most interesting to see is whether your approach can be carried out without the use of Classical. Update: It appears that your axioms introduce a contradiction since modulus isn't supposed to be computable (?).

Require Import List.
Require Import Arith.
Require Import Omega.

Ltac mp_cancel :=
  repeat match goal with
  | [ H2 : ?P -> ?Q , H1 : ?P |- _ ] => specialize (H2 H1)
  end.

Ltac mp_cancel_reflexivity :=
  repeat match goal with
  | [ H1 : ?P = ?P -> ?Q |- _ ] => assert (H_mp_cancel_reflexivity : P = P) by reflexivity; specialize (H1 H_mp_cancel_reflexivity); clear H_mp_cancel_reflexivity
  end.

Parameter encode_pair: (nat * nat) -> nat.
Parameter decode_pair: nat -> (nat * nat).

Axiom decode_encode: forall a b, (decode_pair (encode_pair (a, b))) = (a, b).

Inductive result :=
| ACCEPT : result
| REJECT : result
| NOTYET : result.

Definition result_narrowing (a : result) (b : result) : Prop :=
  (match a with
  | ACCEPT => b = ACCEPT
  | REJECT => b = REJECT
  | NOTYET => True
  end).

Lemma result_narrowing_trans: forall a b c, result_narrowing a b -> result_narrowing b c -> result_narrowing a c.
intros until 0.
destruct a; destruct b; destruct c;
  unfold result_narrowing;
  intros;
  try discriminate;
  reflexivity.
Qed.

Parameter compute: nat (* program *) -> nat (* input *) -> nat (* steps *) -> result.

Axiom compute_narrowing:
  forall program input steps steps',
  (steps' >= steps) -> (result_narrowing (compute program input steps) (compute program input steps')).

Require Import Classical.

Lemma compute_non_divergent:
  forall program input steps steps',
  (compute program input steps) = ACCEPT ->
  (compute program input steps') = REJECT ->
  False.
intros.
assert (T := (classic (steps' >= steps))).
destruct T.
assert (T := (compute_narrowing program input steps steps')).
mp_cancel.
rewrite H, H0 in T.
unfold result_narrowing in T.
discriminate T.
unfold not in H1.
assert (T := (classic (steps' = steps))).
destruct T.
rewrite H2 in H0.
rewrite H in H0.
discriminate.
assert (steps >= steps').
omega.
assert (T := (compute_narrowing program input steps' steps)).
mp_cancel.
rewrite H, H0 in T.
unfold result_narrowing in T.
discriminate.
Qed.

Definition procedure_type := nat (* input *) -> nat (* depth *) -> result.

Definition procedure_narrowing (procedure : procedure_type) : Prop :=
  forall input depth depth',
  (depth' >= depth) -> (result_narrowing (procedure input depth) (procedure input depth')).

Axiom exists_program_of_procedure:
  forall procedure : procedure_type,
  (procedure_narrowing procedure) ->
  exists program,
  forall input,
  (
    forall depth,
    exists steps,
    (result_narrowing (procedure input depth) (compute program input steps))
  ) /\
  (
    forall steps,
    exists depth,
    (result_narrowing (compute program input steps) (procedure input depth))
  ).

Definition program_halts_on_input (program : nat) (input : nat) : Prop :=
  (exists steps, (compute program input steps) <> NOTYET).

Definition program_is_decider (program : nat) : Prop :=
  forall input,
  exists steps,
  (compute program input steps) <> NOTYET.

Definition program_solves_halting_problem_partially (program : nat) : Prop :=
  forall input,
  forall steps,
  (
       ((compute program input steps) = ACCEPT)
    -> (match (decode_pair input) with | (target_program, target_input) => (  (program_halts_on_input target_program target_input)) end)
  ) /\
  (
       ((compute program input steps) = REJECT)
    -> (match (decode_pair input) with | (target_program, target_input) => (~ (program_halts_on_input target_program target_input)) end)
  ).

Lemma minsky: (~ (exists halts, (program_is_decider halts) /\ (program_solves_halting_problem_partially halts))).
unfold not.
intros H_ph.
elim H_ph; clear H_ph; intros invocation_halts [H_ph_d H_ph_b].
pose
  (procedure_modified := (fun (input : nat) (depth : nat) =>
    (match (compute invocation_halts input depth) with
    | ACCEPT => NOTYET
    | REJECT => REJECT
    | NOTYET => NOTYET
    end))).
pose
  (procedure_wrapper := (fun (input : nat) (depth : nat) =>
    (procedure_modified (encode_pair (input, input)) depth))).
unfold procedure_modified in procedure_wrapper.
clear procedure_modified.
assert (T1 := (exists_program_of_procedure procedure_wrapper)).
assert (T2 : (procedure_narrowing procedure_wrapper)).
{
  clear T1.
  unfold procedure_narrowing, procedure_wrapper.
  intros.
  unfold result_narrowing.
  case_eq (compute invocation_halts (encode_pair (input, input)) depth); try intuition.
  assert (T := (compute_narrowing invocation_halts (encode_pair (input, input)) depth depth')).
  mp_cancel.
  rewrite H0 in T.
  unfold result_narrowing in T.
  rewrite T.
  reflexivity.
}
mp_cancel.
clear T2.
elim T1; clear T1; intros program_wrapper H_pw.
unfold procedure_wrapper in H_pw.
clear procedure_wrapper.
specialize (H_pw program_wrapper).
destruct H_pw as [H_pw_fwd H_pw_rev].
unfold program_is_decider in H_ph_d.
specialize (H_ph_d (encode_pair (program_wrapper, program_wrapper))).
elim H_ph_d; clear H_ph_d; intros steps_inner H_ph_d.
unfold program_solves_halting_problem_partially in H_ph_b.
specialize (H_ph_b (encode_pair (program_wrapper, program_wrapper)) steps_inner).
destruct H_ph_b as [H_ph_b_1 H_ph_b_2].
case_eq (compute invocation_halts (encode_pair (program_wrapper, program_wrapper)) steps_inner).
{
  intros.
  rewrite H in *.
  mp_cancel_reflexivity.
  unfold program_halts_on_input in H_ph_b_1.
  rewrite decode_encode in H_ph_b_1.
  elim H_ph_b_1; clear H_ph_b_1; intros steps_outer H_ph_b_1.
  specialize (H_pw_rev steps_outer).
  case_eq (compute program_wrapper program_wrapper steps_outer).
  {
    intros.
    rewrite H0 in *.
    unfold result_narrowing in H_pw_rev.
    elim H_pw_rev; clear H_pw_rev; intros depth H_pw_rev.
    case_eq (compute invocation_halts (encode_pair (program_wrapper, program_wrapper)) depth); intros Hx; rewrite Hx in *; try discriminate.
  }
  {
    intros.
    rewrite H0 in *.
    unfold result_narrowing in H_pw_rev.
    elim H_pw_rev; clear H_pw_rev; intros depth H_pw_rev.
    case_eq (compute invocation_halts (encode_pair (program_wrapper, program_wrapper)) depth); intros Hx; rewrite Hx in *; try discriminate.
    assert (T := (compute_non_divergent invocation_halts (encode_pair (program_wrapper, program_wrapper)) steps_inner depth)).
    mp_cancel.
    assumption.
  }
  {
    intros.
    intuition.
  }
}
{
  intros.
  rewrite H in *.
  mp_cancel_reflexivity.
  unfold not, program_halts_on_input in H_ph_b_2.
  specialize (H_pw_fwd steps_inner).
  rewrite H in H_pw_fwd.
  unfold result_narrowing in H_pw_fwd.
  elim H_pw_fwd; intros.
  rewrite decode_encode in H_ph_b_2.
  contradict H_ph_b_2.
  exists x.
  unfold not.
  intros.
  rewrite H0 in H1.
  discriminate.
}
{
  intros.
  unfold not in H_ph_d.
  mp_cancel.
  assumption.
}
Qed.