# Library Rice

Require Export Scott Acceptability.

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

Proof.

intros H.

destruct H as [u [[cls_u lam_u] H]].

unfold self_diverging in H.
specialize (H u). intuition.
Qed.

Proof.

intros [u [[cls_u lam_u] H]].

unfold self_diverging_comb in H.
unfold conj in H.
specialize (H u).
unfold self_diverging in H.
destruct H.
firstorder.
Qed.

# Rice's Theorem

Lemma Rice1 (M : term -> Prop) : (M <=1 proc) ->
(forall (s t : term), proc t -> M s -> (forall u, pi s u <-> pi t u) -> M t) ->
(exists p, proc p /\ ~ M p) -> (exists p, proc p /\ M p) ->
M (lam Omega) -> ~ lacc M.

Proof with eauto; try now intuition.

intros M_proc M_cl_equiv [t2 [cls_t2 nMt2]] [t1 [cls_t1 nMt1]] MLO [u [[cls_u lam_u] Hu]].

eapply (self_div_comb).

destruct (dec_lacc ldec_closed) as [c [[cls_c lam_c] Hc]].

pose (v := lam ( u (Lam (App (tenc (lam (t2 #1))) (App #0 (Q #0)))))).

pose (v' := acc_conj c v).

exists v'; split; value.

intros s.

pose (vs := lam ((lam (t2 #1)) (s (tenc s)))).

symmetry.

transitivity (pi v s /\ closed s).

{
unfold v'.
rewrite acc_conj_correct; value. firstorder intuition.
}

unfold self_diverging_comb, conj.

transitivity (pi u vs /\ closed s).

{
assert (H : u (Lam ((App (tenc (Î» t2 #1))) ((App (tenc s)) (Q (tenc s))))) == u (tenc vs))
by now rewrite Q_correct, !App_correct, !Lam_correct.

split; intros [pi_v_s cls_s]; intuition;
unfold pi; revert pi_v_s; eapply converges_proper; rewrite <- H; unfold v; [symmetry | ]; crush.

}

transitivity (M vs /\ closed s).

split; intros [? ?]; intuition; try (now rewrite Hu); firstorder.

{
split.

- intros [Mvs cls_s]; intuition.

intros [w Hw].

assert (forall t, pi vs t <-> pi t2 t). {

intros t.
eapply converges_proper; unfold vs; crush.
}
eapply nMt2.
eapply M_cl_equiv; eassumption.
- intros [npi_s_s cls_s]; intuition.

assert (forall t, pi (lam Omega) t <-> pi vs t). {

intros t; split; intros H.

- exfalso.
destruct H as [w Hw]. eapply Omega_diverges. rewrite <- Hw. symmetry. clear Hw. crush.
- exfalso.
eapply npi_s_s.
assert (A: converges ((Î» t2 (tenc t)) (s (tenc s)))).
revert H. eapply converges_proper. symmetry. unfold vs. crush.
eapply app_converges in A.
firstorder.
}
eapply M_cl_equiv; value; eassumption.

}
Qed.

Lemma Rice2 (M : term -> Prop) : (M <=1 proc) ->
(forall (s t : term), proc t -> M s -> (forall u, pi s u <-> pi t u) -> M t) ->
(exists p, proc p /\ ~ M p) -> (exists p, proc p /\ M p) ->
~ M (lam Omega) -> ~ lacc (complement M).

Proof.

intros M_cls M_cl_equiv [t2 [cls_t2 nMt2]] [t1 [cls_t1 nMt1]] nMLO decM.

destruct decM as [u [[cls_u lam_u] Hu]].
unfold complement in Hu.

eapply (self_div_comb).

destruct (dec_lacc ldec_closed) as [c [[cls_c lam_c] Hc]].

pose (v := lam ( u (Lam (App (tenc (lam (t1 #1))) (App #0 (Q #0)))))).

pose (v' := acc_conj c v).

exists v'; split; value.

intros s.

pose (vs := lam ((lam (t1 #1)) (s (tenc s)))).

symmetry.

transitivity (pi v s /\ closed s).

{
unfold v'.
rewrite acc_conj_correct; value. firstorder intuition.
}

unfold self_diverging_comb, conj.

transitivity (pi u vs /\ closed s).

{
assert (H : u (Lam ((App (tenc (Î» t1 #1))) ((App (tenc s)) (Q (tenc s))))) == u (tenc vs))
by now rewrite Q_correct, !App_correct, !Lam_correct.

split; intros [pi_v_s cls_s]; intuition;
unfold pi; revert pi_v_s; eapply converges_proper; rewrite <- H; unfold v; [symmetry | ]; crush.

}

transitivity (~ M vs /\ closed s).

{
split; intros [? ?]; try (rewrite Hu); intuition; firstorder.

}

{
split.

- intros [Mvs cls_s]; intuition.

intros [w Hw].

assert (forall t, pi t1 t <-> pi vs t). {

intros t.
symmetry. eapply converges_proper. unfold vs.
transitivity ((Î» t1 (tenc t)) (s (tenc s))).
crush. rewrite Hw. crush.
}
eapply Mvs.
eapply M_cl_equiv; value; eassumption.
- intros [npi_s_s cls_s]; intuition.

assert (forall t, pi (lam Omega) t <-> pi vs t). {

intros t; split; intros A.

- exfalso.
destruct A as [w Hw]. eapply Omega_diverges. rewrite <- Hw. symmetry. clear Hw. crush.
- exfalso.
eapply npi_s_s.
assert (B: converges ((Î» t1 (tenc t)) (s (tenc s)))).
revert A. eapply converges_proper. symmetry. unfold vs. crush.
eapply app_converges in B.
firstorder.
}
eapply nMLO.

eapply M_cl_equiv; try (symmetry); eauto.

}
Qed.

## Rice's Theorem, classical

Theorem Rice (M : term -> Prop) : (M <=1 proc) ->
(forall (s t : term), proc t -> M s -> (forall u, pi s u <-> pi t u) -> M t) ->
(exists p, proc p /\ ~ M p) -> (exists p, proc p /\ M p) ->
~ ldec M.

Proof.

intros.
intros A. assert (B : ldec M) by eassumption. destruct A as [u [proc_u Hu]].
destruct (Hu (lam Omega)).

- eapply Rice1; try eassumption.
tauto. eapply dec_lacc. exists u; tauto.
- eapply Rice2; try eassumption.
tauto. eapply dec_lacc. eapply ldec_complement. exists u; tauto.
Qed.

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

Proof.

intros A.
destruct A as [? H]. eapply Omega_diverges. symmetry in H; symmetry; crush.
Qed.

# Applications of Rice's Theorem

Goal ~ ldec (fun s => proc s /\ forall t, pi s t).

Proof.

eapply Rice.

- firstorder.

- firstorder.

- exists (lam Omega).
split; value. intros [_ A]. eapply lamOmega; eauto.
- exists (lam I).
repeat split; value. intros t; eexists; crush.
Grab Existential Variables.
repeat econstructor.
Qed.

Goal ~ lacc (fun s => proc s /\ exists t, ~ pi s t).

Proof.

eapply Rice1.

- firstorder.

- intros s t cls_t [cls_s [t0 H]] He.
split; eauto.
exists t0.
rewrite <- He. eassumption.
- exists (lam I).
split; value. intros [_ [? H]]. eapply H. eexists; crush.
- exists (lam Omega).
repeat split; value. exists I. eapply lamOmega.
- split; value.
exists I. eapply lamOmega.
Qed.

# Rice's Theorem, classical, on combinators

Theorem Rice_classical (M : term -> Prop) : (M <=1 closed) ->
(forall (s t : term), closed t -> M s -> (forall u, pi s u <-> pi t u) -> M t) ->
(exists p, closed p /\ ~ M p) -> (exists p, closed p /\ M p) ->
~ ldec M.

Proof.

intros.
eapply Scott.
- firstorder.

- intros.
eapply H0; try eassumption. intros. unfold pi. now rewrite H5.
- destruct H2; eauto.

- destruct H2; eauto.

Qed.