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.


Lemma self_div_comb : ~ lacc self_diverging_comb.

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.