Module halting_problem

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

This page has been generated by coqdoc