Y.v 3.35 KB
Newer Older
1
From iris.proofmode Require Import tactics.
2
From iris_logrel Require Export logrel examples.bot.
3

4
(* Semantic typeability of the Y combinator and the Landin's knot *)
5 6 7 8

Definition Y : val :=
  λ: "f", (λ: "x", "f" ("x" "x")) (λ: "x", "f" ("x" "x")).

9 10 11 12
Definition Knot : val := λ: "f",
  let: "z" := ref bot
  in "z" <- (λ: "x", "f" (!"z" #()));; !"z" #().

13 14 15
Definition F : val := rec: "f" "g" :=
  "g" ("f" "g").

16 17 18
Section contents.
  Context `{logrelG Σ}.
  Lemma Y_semtype Δ Γ A :
19
    {Δ;Γ}  Y log Y : TArrow (TArrow A A) A.
20 21
  Proof.
    unlock Y. simpl.
22
    iApply bin_log_related_arrow; eauto.
23 24 25 26
    iAlways. iIntros (f1 f2) "#Hff".
    rel_let_l. rel_let_r.
    iLöb as "IH".
    rel_let_l. rel_let_r.
27 28
    iApply (bin_log_related_app with "Hff").
    by iApply "IH".
29
  Qed.
30 31

  Lemma KNOT_Y Δ Γ A :
32
    {Δ;Γ}  Knot log Y : TArrow (TArrow A A) A.
33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48
  Proof.
    unlock Y Knot. simpl.
    iApply bin_log_related_arrow; eauto.
    iAlways. iIntros (f1 f2) "#Hff".
    rel_let_l. rel_let_r.
    rel_alloc_l as z "Hz". rel_let_l.
    rel_store_l.
    rel_let_l.
    iLöb as "IH".
    rel_let_r.
    rel_load_l. rel_let_l.
    iApply (bin_log_related_app with "Hff").
    by iApply "IH".
  Qed.

  Lemma Y_KNOT Δ Γ A :
49
    {Δ;Γ}  Y log Knot : TArrow (TArrow A A) A.
50 51 52 53 54 55 56 57 58 59 60 61 62 63
  Proof.
    unlock Y Knot. simpl.
    iApply bin_log_related_arrow; eauto.
    iAlways. iIntros (f1 f2) "#Hff".
    rel_let_l. rel_let_r.
    rel_alloc_r as z "Hz". rel_let_r.
    rel_store_r.
    rel_let_r.
    iLöb as "IH".
    rel_let_l.
    rel_load_r. rel_let_r.
    iApply (bin_log_related_app with "Hff").
    by iApply "IH".
  Qed.
64 65

  Lemma FIX_Y Δ Γ A :
66
    {Δ;Γ}  F log Y : TArrow (TArrow A A) A.
67 68 69 70 71 72 73 74 75 76 77 78
  Proof.
    unlock Y F. simpl.
    iApply bin_log_related_arrow; eauto.
    iAlways. iIntros (f1 f2) "#Hff".
    rel_let_r.
    iLöb as "IH".
    rel_let_l. rel_let_r.
    iApply (bin_log_related_app with "Hff").
    by iApply "IH".
  Qed.

  Lemma Y_FIX Δ Γ A :
79
    {Δ;Γ}  Y log F : TArrow (TArrow A A) A.
80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115
  Proof.
    unlock Y F. simpl.
    iApply bin_log_related_arrow; eauto.
    iAlways. iIntros (f1 f2) "#Hff".
    rel_let_l.
    iLöb as "IH".
    rel_let_l. rel_let_r.
    iApply (bin_log_related_app with "Hff").
    by iApply "IH".
  Qed.

  Lemma FIX_prefixpoint Δ Γ α β (v : val) :
     ({Δ;Γ}  v log v : ((α  β)  α  β)) -
    {Δ;Γ}  v (F v) log F v : (α  β).
  Proof.
    iIntros "#Hv".
    unlock F. simpl.
    rel_let_r.
    iApply (bin_log_related_app with "Hv").
    iApply (bin_log_related_app with "[] Hv").
    iApply binary_fundamental.
    solve_typed.
  Qed.

  Lemma FIX_postfixpoint Δ Γ α β (v : val) :
     ({Δ;Γ}  v log v : ((α  β)  α  β)) -
    {Δ;Γ}  F v log v (F v) : (α  β).
  Proof.
    iIntros "#Hv".
    unlock F. simpl.
    rel_let_l.
    iApply (bin_log_related_app with "Hv").
    iApply (bin_log_related_app with "[] Hv").
    iApply binary_fundamental.
    solve_typed.
  Qed.
116 117 118 119 120 121 122 123 124 125 126 127 128
End contents.

Theorem Y_typesafety f e' τ thp σ σ' :
   ⊢ₜ f : TArrow τ τ 
  rtc step ([Y f], σ) (thp, σ')  e'  thp 
  is_Some (to_val e')  reducible e' σ'.
Proof.
  intros Hf Hst He'.
  eapply (logrel_typesafety logrelΣ [] (Y f)); eauto.
  intros. iApply bin_log_related_app.
  - iApply Y_semtype.
  - iApply binary_fundamental; eauto.
Qed.