Commit 1bed793b by Dan Frumin

### Example: Landin's knot is equivalent to the Y combinator

parent fab4fb46
 ... @@ -27,6 +27,7 @@ theories/logrel/soundness_binary.v ... @@ -27,6 +27,7 @@ theories/logrel/soundness_binary.v theories/logrel.v theories/logrel.v theories/examples/lock.v theories/examples/lock.v theories/examples/ticket_lock.v theories/examples/ticket_lock.v theories/examples/bot.v theories/examples/counter.v theories/examples/counter.v theories/examples/lateearlychoice.v theories/examples/lateearlychoice.v theories/examples/par.v theories/examples/par.v ... ...
 From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics. From iris_logrel Require Export logrel. From iris_logrel Require Export logrel examples.bot. (* Semantic typeability of the Y combinator *) (* Semantic typeability of the Y combinator and the Landin's knot *) Definition Y : val := Definition Y : val := λ: "f", (λ: "x", "f" ("x" "x")) (λ: "x", "f" ("x" "x")). λ: "f", (λ: "x", "f" ("x" "x")) (λ: "x", "f" ("x" "x")). Definition Knot : val := λ: "f", let: "z" := ref bot in "z" <- (λ: "x", "f" (!"z" #()));; !"z" #(). Section contents. Section contents. Context `{logrelG Σ}. Context `{logrelG Σ}. Lemma Y_semtype Δ Γ A : Lemma Y_semtype Δ Γ A : ... @@ -20,6 +24,40 @@ Section contents. ... @@ -20,6 +24,40 @@ Section contents. iApply (bin_log_related_app with "Hff"). iApply (bin_log_related_app with "Hff"). by iApply "IH". by iApply "IH". Qed. Qed. Lemma KNOT_Y Δ Γ A : {⊤,⊤;Δ;Γ} ⊨ Knot ≤log≤ Y : TArrow (TArrow A A) A. 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 : {⊤,⊤;Δ;Γ} ⊨ Y ≤log≤ Knot : TArrow (TArrow A A) A. 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. End contents. End contents. Theorem Y_typesafety f e' τ thp σ σ' : Theorem Y_typesafety f e' τ thp σ σ' : ... ...
 From iris.proofmode Require Import tactics. From iris_logrel Require Export logrel. Definition bot : val := rec: "bot" <> := "bot" #(). Lemma bot_typed Γ τ : Γ ⊢ₜ bot : TArrow TUnit τ. Proof. solve_typed. Qed. Hint Resolve bot_typed : typeable. Section contents. Context `{logrelG Σ}. Lemma bot_l ϕ Δ Γ E K t τ : (ϕ -∗ {E;Δ;Γ} ⊨ fill K (bot #()) ≤log≤ t : τ) -∗ Maintainer Isn't this premise redundant? Isn't this premise redundant? Maintainer It most certainly is. I guess I had the lemma to be in this shape for the ease of some proof, but it is no longer needed. It most certainly is. I guess I had the lemma to be in this shape for the ease of some proof, but it is no longer needed. Maintainer I've fixed it in 7546cf67 I've fixed it in 7546cf67316c4749474372b29c4b5bfb18cae23a Please register or sign in to reply {E;Δ;Γ} ⊨ fill K (bot #()) ≤log≤ t : τ. Proof. iIntros "Hlog". iLöb as "IH". rel_rec_l. unlock bot; simpl_subst/=. iApply ("IH" with "Hlog"). Qed. End contents.
 ... @@ -15,7 +15,7 @@ ... @@ -15,7 +15,7 @@ where every v_i is well-typed Unit -> Unit where every v_i is well-typed Unit -> Unit *) *) From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics. From iris_logrel Require Export logrel examples.various (* for bot *). From iris_logrel Require Export logrel examples.bot. Definition or : val := λ: "e1" "e2", Definition or : val := λ: "e1" "e2", let: "x" := ref #0 in let: "x" := ref #0 in ... ...
 ... @@ -75,10 +75,6 @@ Definition nth : val := rec: "nth" "l" "n" := ... @@ -75,10 +75,6 @@ Definition nth : val := rec: "nth" "l" "n" := else "nth" (Snd "xs") ("n" - #1) else "nth" (Snd "xs") ("n" - #1) end. end. Lemma bot_typed Γ τ : Γ ⊢ₜ bot : TArrow TUnit τ. Proof. solve_typed. Qed. Hint Resolve bot_typed : typeable. Lemma nth_typed Γ τ : Lemma nth_typed Γ τ : Γ ⊢ₜ nth : TArrow (LIST τ) (TArrow TNat τ). Γ ⊢ₜ nth : TArrow (LIST τ) (TArrow TNat τ). Proof. Proof. ... ...
 ... @@ -4,7 +4,7 @@ ... @@ -4,7 +4,7 @@ *) *) From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics. From iris.algebra Require Import csum agree excl. From iris.algebra Require Import csum agree excl. From iris_logrel Require Import logrel examples.lock examples.counter. From iris_logrel Require Export logrel examples.lock examples.counter examples.bot. Section refinement. Section refinement. Context `{logrelG Σ}. Context `{logrelG Σ}. ... @@ -219,18 +219,6 @@ Section refinement. ... @@ -219,18 +219,6 @@ Section refinement. rel_vals; eauto. } rel_vals; eauto. } Qed. Qed. Definition bot : val := rec: "bot" <> := "bot" #(). Lemma bot_l ϕ Δ Γ E K t τ : (ϕ -∗ {E;Δ;Γ} ⊨ fill K (bot #()) ≤log≤ t : τ) -∗ {E;Δ;Γ} ⊨ fill K (bot #()) ≤log≤ t : τ. Proof. iIntros "Hlog". iLöb as "IH". rel_rec_l. unlock bot; simpl_subst/=. iApply ("IH" with "Hlog"). Qed. (* /Sort of/ a well-bracketedness example. (* /Sort of/ a well-bracketedness example. Without locking in the first expression, the callback can reenter Without locking in the first expression, the callback can reenter the body in a forked thread to change the value of x the body in a forked thread to change the value of x ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!