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

``` ```

Index