Library Rice

The self halting problem is not L-acceptable

Definition self_diverging (s : term) := ¬ pi s s.

Definition self_diverging_comb := conj self_diverging closed.

Lemma self_div : ¬ lacc self_diverging.

Lemma self_div_comb : ¬ lacc self_diverging_comb.

Rice's Theorem

Lemma Rice1 (M : term → Prop) : (M <=1 proc) →
                                 (∀ (s t : term), proc t → M 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 : term → Prop) : (M <=1 proc) →
                                 (∀ (s t : term), proc t → M 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 : term → Prop) : (M <=1 proc) →
                                 (∀ (s t : term), proc t → M 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 s ⇒ proc s ∧ ∀ t, pi s t).

Goal ¬ lacc (fun s ⇒ proc s ∧ ∃ t, ¬ pi s t).

Rice's Theorem, classical, on combinators

Theorem Rice_classical (M : term → Prop) : (M <=1 closed) →
                                 (∀ (s t : term), closed t → M s → (∀ u, pi s u ↔ pi t u) → M t) →
                                  (∃ p, closed p ∧ ¬ M p) → (∃ p, closed p ∧ M p) →
                                  ¬ ldec M.