|
This work is a proof of the undecidability of the halting problem for Turing complete computation models. It is just a translation to Coq of the proof presented in Kristofer Johannisson's paper called Formalizing the Halting
Problem in a Constructive Type Theory.
(Vincent Cremet - mars 2003) |
The abstract computation model |
| The set of programs. |
Variable Prog: Set.
| The set of input and output values for programs with an associated equivalence relation. |
Variable Val: Set.
Variable eg: Val -> Val -> Prop.
Hypothesis eg_refl: (x: Val) (eg x x).
Hypothesis eg_sym: (x, y: Val) (eg x y) -> (eg y x).
Hypothesis eg_trans: (x, y, z: Val) (eg x y) -> (eg y z) -> (eg x z).
| Substitutivity of the equivalence relation. |
Definition isSubstitutive [A: Set; eg: A -> A -> Prop]: Prop :=
(a, b: A)(P: A -> Prop) (eg a b) -> (P a) -> (P b).
Hypothesis substEgVal: (isSubstitutive Val eg).
| A partial function which maps a program and a input value to an output value. |
Hypothesis computes: Prog -> Val -> Val -> Prop.
Hypothesis pComputes: (p: Prog) (inp: Val) (out1: Val) (out2: Val)
(computes p inp out1) -> (computes p inp out2) -> (eg out1 out2).
| Encoding of programs and pairs of values into values. |
Variable encode: Prog -> Val.
Variable pairCode: Val -> Val -> Val.
| Diagonalization program. |
Variable diagonalize: Prog.
Hypothesis pDiagonalize: (n: Val) (computes diagonalize n (pairCode n n)).
| Composition of programs. |
Variable compose: Prog -> Prog -> Prog.
Hypothesis pCompose: (p1, p2: Prog) (inp, out: Val)
(EX interm: Val | (computes p1 inp interm) /\ (computes p2 interm out))
<->
(computes (compose p1 p2) inp out).
| Boolean Litterals. |
Variable Vrai: Val.
Variable Faux: Val.
Hypothesis pTrueIsNotFalse: ~(eg Vrai Faux).
| Loop program. |
Variable loop: Prog.
Hypothesis pLoop: (inp: Val) ~(EX out: Val | (computes loop inp out)).
| Constant programs. |
Variable const: Val -> Prog.
Hypothesis pConst: (c: Val) (inp: Val) (computes (const c) inp c).
Definition constInp [p: Prog; c: Val]: Prog := (compose (const c) p).
Theorem pConstInp: (p: Prog)(c, inp, out: Val)
(computes (constInp p c) inp out) <-> (computes p c out).
| Conditional program (if). |
Variable SI: Prog -> Prog -> Prog -> Prog.
Hypothesis pSI: (si, alors, sinon: Prog)(inp, out: Val)
((computes (SI si alors sinon) inp out) <->
(((computes si inp Vrai) /\ (computes alors inp out)) \/
((computes si inp Faux) /\ (computes sinon inp out)))).
Termination of a computation. |
Definition computation: Set := Prog * Val.
Definition results_in [c: computation; out: Val]: Prop :=
(computes (fst ? ? c) (snd ? ? c) out).
Definition terminates [c: computation]: Prop :=
(ex Val [out: Val] (results_in c out)).
Definition eqComp [c1, c2: computation]: Prop :=
(out: Val) (results_in c1 out) <-> (results_in c2 out).
Lemma eqComp_sym: (c1, c2: computation) (eqComp c1 c2) -> (eqComp c2 c1).
Theorem pDiagPair: (p: Prog)(n,r: Val)
(results_in ((compose diagonalize p), n) r) <->
(results_in (p, (pairCode n n)) r).
Definition of decidability. |
Definition decides [pred: computation -> Prop; prog: Prog]: Prop :=
(c: computation)
((computes prog (pairCode (encode (fst ?? c)) (snd ?? c)) Vrai) \/
(computes prog (pairCode (encode (fst ?? c)) (snd ?? c)) Faux)) /\
((computes prog (pairCode (encode (fst ?? c)) (snd ?? c)) Vrai) <-> (pred c)) /\
((computes prog (pairCode (encode (fst ?? c)) (snd ?? c)) Faux) <-> ~(pred c)).
Definition decidable [pred: computation -> Prop]: Prop :=
(EX prog: Prog | (decides pred prog)).
Non trivial and substitutive predicates are undecidable. |
Definition isSubst [pred: computation -> Prop]: Prop :=
(c1, c2: computation) (eqComp c1 c2) -> (pred c1) -> (pred c2).
Theorem abstractHaltp:
(pred: computation -> Prop)
(isSubst pred) ->
(ex, nex: computation)
(pred ex) -> ~(pred nex) ->
~(decidable pred).
Proof of the halting problem. |
Definition c_terminates: computation := ((const Vrai), Vrai).
Definition c_not_terminates: computation := (loop, Vrai).
Lemma isSubst_terminates: (isSubst terminates).
Lemma terminates_constant: (terminates c_terminates).
Lemma not_terminates_loop: ~(terminates c_not_terminates).
Theorem halting_problem: ~(decidable terminates).