|
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).
Intros.
Unfold constInp.
Case (pCompose (const c) p inp out).
Intros.
Split.
Intro.
Case (H0 H1).
Clear H0.
Clear H1.
Intros.
Case H0.
Clear H0.
Intros.
Assert (eg x c).
Apply pComputes with (const c) inp.
Trivial.
Apply pConst.
Apply (substEgVal x c [y: Val] (computes p y out)).
Trivial.
Trivial.
Clear H0.
Intro.
Apply H.
Clear H.
Exists c.
Split.
Apply pConst.
Trivial.
Qed.
| 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).
Unfold eqComp.
Intros.
Pose (H out).
Assert (A, B: Prop) (A <-> B) -> (B <-> A).
Tauto.
Apply H0.
Assumption.
Qed.
Theorem pDiagPair: (p: Prog)(n,r: Val)
(results_in ((compose diagonalize p), n) r) <->
(results_in (p, (pairCode n n)) r).
Intros.
Unfold results_in.
Unfold fst snd.
Split.
Intro.
Case (pCompose diagonalize p n r).
Intros.
Clear H0.
Elim (H1 H).
Clear H1.
Clear H.
Intros.
Elim H.
Clear H.
Intros.
Assert (eg x (pairCode n n)).
Apply pComputes with diagonalize n.
Trivial.
Exact (pDiagonalize n).
Clear H.
Apply (substEgVal x (pairCode n n) [y: Val] (computes p y r)).
Trivial.
Trivial.
Intro.
Case (pCompose diagonalize p n r).
Intros.
Clear H1.
Apply H0.
Clear H0.
Apply ex_intro with (pairCode n n).
Split.
Apply pDiagonalize.
Trivial.
Qed.
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).
Assert ssi_proj1: (A, B: Prop) (A <-> B) -> A -> B.
Tauto.
Assert ssi_proj2: (A, B: Prop) (A <-> B) -> B -> A.
Tauto.
Intros.
Unfold not.
Intro.
Unfold decidable in H2.
Case H2.
Clear H2.
Intros.
Pose liar :=
(SI (compose diagonalize x)
(constInp (fst ?? nex) (snd ?? nex))
(constInp (fst ?? ex) (snd ?? ex))
).
| Beginning pLiar1. |
Assert pLiar1: (inp: Val)
(computes x (pairCode inp inp) Vrai) ->
~(pred (liar, inp)).
Intros.
Assert (eqComp nex (liar, inp)).
Unfold eqComp.
Intro.
Unfold results_in.
Split.
Intro.
Unfold fst.
Unfold snd.
Unfold liar.
Pose (pSI (compose diagonalize x)
(constInp (fst Prog Val nex) (snd Prog Val nex))
(constInp (fst Prog Val ex) (snd Prog Val ex)) inp out).
ClearBody i.
Case i.
Clear i.
Intros.
Clear H5.
Apply H6.
Clear H6.
Left.
Split.
Pose i:= (pDiagPair x inp Vrai).
ClearBody i.
Unfold results_in in i.
Unfold fst in i.
Unfold snd in i.
Apply (ssi_proj2 (computes (compose diagonalize x) inp Vrai) (computes x (pairCode inp inp) Vrai) i).
Trivial.
Apply (ssi_proj2
(computes (constInp (fst Prog Val nex) (snd Prog Val nex)) inp out)
(computes (fst Prog Val nex) (snd Prog Val nex) out)
(pConstInp (fst Prog Val nex) (snd Prog Val nex) inp out)).
Trivial.
| End step 1 |
Intro.
Unfold fst in H4.
Unfold snd in H4.
Unfold liar in H4.
Pose (pSI (compose diagonalize x)
(constInp (fst Prog Val nex) (snd Prog Val nex))
(constInp (fst Prog Val ex) (snd Prog Val ex)) inp out).
ClearBody i.
Case i.
Clear i.
Intros.
Clear H6.
Elim (H5 H4).
Clear H5.
Clear H4.
Intro.
Case H4.
Clear H4.
Intros.
Apply (ssi_proj1
(computes (constInp (fst Prog Val nex) (snd Prog Val nex)) inp out)
(computes (fst Prog Val nex) (snd Prog Val nex) out)
(pConstInp (fst Prog Val nex) (snd Prog Val nex) inp out)).
Trivial.
| End step 2. |
Cut ~((computes (compose diagonalize x) inp Faux)).
Tauto.
Clear H4.
Clear H5.
Unfold not.
Intro.
Apply pTrueIsNotFalse.
Assert (computes x (pairCode inp inp) Faux).
Pose i := (pDiagPair x inp Faux).
ClearBody i.
Unfold results_in in i.
Unfold fst in i.
Unfold snd in i.
Case i.
Clear i.
Intros.
Clear H6.
Apply (H5 H4).
Apply pComputes with x (pairCode inp inp).
Assumption.
Assumption.
| End step 3. |
Unfold isSubst in H.
Unfold not.
Intro.
Unfold not in H1.
Apply H1.
Apply H with (liar,inp).
Apply eqComp_sym.
Assumption.
Assumption.
| End of pLiar1 proof. |
| Beginning pLiar2: almost the same as pLiar1 |
Assert pLiar2: (inp: Val)
(computes x (pairCode inp inp) Faux) ->
(pred (liar, inp)).
Clear pLiar1.
Intros.
Assert (eqComp ex (liar, inp)).
Unfold eqComp.
Intro.
Unfold results_in.
Split.
Intro.
Unfold fst.
Unfold snd.
Unfold liar.
Pose (pSI (compose diagonalize x)
(constInp (fst Prog Val nex) (snd Prog Val nex))
(constInp (fst Prog Val ex) (snd Prog Val ex)) inp out).
ClearBody i.
Case i.
Clear i.
Intros.
Clear H5.
Apply H6.
Clear H6.
Right.
Split.
Pose i:= (pDiagPair x inp Faux).
ClearBody i.
Unfold results_in in i.
Unfold fst in i.
Unfold snd in i.
Apply (ssi_proj2 (computes (compose diagonalize x) inp Faux) (computes x (pairCode inp inp) Faux) i).
Trivial.
Apply (ssi_proj2
(computes (constInp (fst Prog Val ex) (snd Prog Val ex)) inp out)
(computes (fst Prog Val ex) (snd Prog Val ex) out)
(pConstInp (fst Prog Val ex) (snd Prog Val ex) inp out)).
Trivial.
| End step 1 |
Intro.
Unfold fst in H4.
Unfold snd in H4.
Unfold liar in H4.
Pose (pSI (compose diagonalize x)
(constInp (fst Prog Val nex) (snd Prog Val nex))
(constInp (fst Prog Val ex) (snd Prog Val ex)) inp out).
ClearBody i.
Case i.
Clear i.
Intros.
Clear H6.
Elim (H5 H4).
Clear H5.
Clear H4.
Intro.
Case H4.
Clear H4.
Intros.
Apply (ssi_proj1
(computes (constInp (fst Prog Val ex) (snd Prog Val ex)) inp out)
(computes (fst Prog Val ex) (snd Prog Val ex) out)
(pConstInp (fst Prog Val ex) (snd Prog Val ex) inp out)).
Trivial.
| End step 2. |
Cut ~((computes (compose diagonalize x) inp Vrai)).
Tauto.
Clear H4.
Clear H5.
Unfold not.
Intro.
Apply pTrueIsNotFalse.
Assert (computes x (pairCode inp inp) Vrai).
Pose i := (pDiagPair x inp Vrai).
ClearBody i.
Unfold results_in in i.
Unfold fst in i.
Unfold snd in i.
Case i.
Clear i.
Intros.
Clear H6.
Apply (H5 H4).
Apply pComputes with x (pairCode inp inp).
Assumption.
Assumption.
| End step 3. |
Intro.
Case H6.
Clear H6.
Clear H4.
Clear H5.
Intros.
Clear H4.
Case (pConstInp (fst Prog Val ex) (snd Prog Val ex) inp out).
Intros.
Tauto.
| End step 4. |
Unfold isSubst in H.
Apply H with ex.
Assumption.
Assumption.
| End of pLiar2 proof. |
Pose liarliar := (liar, encode liar).
Case (H2 liarliar).
Clear H2.
Intros.
Case H2.
Intro.
Assert (pred liarliar) /\ ~(pred liarliar).
Split.
Clear H2.
Clear pLiar1.
Clear pLiar2.
Tauto.
Clear H2.
Clear H3.
Intro.
Apply pLiar1 with (encode liar).
Trivial.
Trivial.
Tauto.
| End step 1. |
Intro.
Clear H2.
Clear pLiar1.
Assert ~(pred liarliar) /\ (pred liarliar).
Split.
Clear pLiar2.
Tauto.
Clear H3.
Unfold liarliar.
Apply pLiar2.
Exact H4.
Tauto.
| End step 2. |
Qed.
Proof of the halting problem. |
Definition c_terminates: computation := ((const Vrai), Vrai).
Definition c_not_terminates: computation := (loop, Vrai).
Lemma isSubst_terminates: (isSubst terminates).
Unfold isSubst.
Intros.
Unfold terminates.
Unfold terminates in H0.
Unfold eqComp in H.
Case H0.
Intros.
Apply ex_intro with x.
Cut (results_in c1 x)<->(results_in c2 x).
Tauto.
Apply H.
Qed.
Lemma terminates_constant: (terminates c_terminates).
Unfold terminates.
Apply ex_intro with Vrai.
Unfold c_terminates.
Unfold results_in.
Unfold fst.
Apply pConst.
Qed.
Lemma not_terminates_loop: ~(terminates c_not_terminates).
Unfold c_not_terminates.
Unfold terminates.
Unfold results_in.
Unfold fst.
Apply pLoop.
Qed.
Theorem halting_problem: ~(decidable terminates).
Apply abstractHaltp with c_terminates c_not_terminates.
Exact isSubst_terminates.
Exact terminates_constant.
Exact not_terminates_loop.
Qed.