Library Rice


The self halting problem is not L-acceptable

Rice's Theorem


Lemma Rice1 (M : termProp) : (M <=1 proc) →
                                 ( (s t : term), proc tM s → ( u, pi s u pi t u) → M t) →
                                 ( p, proc p ¬ M p) → ( p, proc p M p) →
                                 M (lam Omega) → ¬ lacc M.
Lemma Rice2 (M : termProp) : (M <=1 proc) →
                                 ( (s t : term), proc tM s → ( u, pi s u pi t u) → M t) →
                                 ( p, proc p ¬ M p) → ( p, proc p M p) →
                                 ¬ M (lam Omega) → ¬ lacc (complement M).

Rice's Theorem, classical

Theorem Rice (M : termProp) : (M <=1 proc) →
                                 ( (s t : term), proc tM s → ( u, pi s u pi t u) → M t) →
                                  ( p, proc p ¬ M p) → ( p, proc p M p) →
                                  ¬ ldec M.

Lemma lamOmega s : ¬ pi (lam Omega) s.

Applications of Rice's Theorem


Goal ¬ ldec (fun sproc s t, pi s t).

Goal ¬ lacc (fun sproc s t, ¬ pi s t).

Rice's Theorem, classical, on combinators


Theorem Rice_classical (M : termProp) : (M <=1 closed) →
                                 ( (s t : term), closed tM s → ( u, pi s u pi t u) → M t) →
                                  ( p, closed p ¬ M p) → ( p, closed p M p) →
                                  ¬ ldec M.