Theory Continuations
section ‹Relating direct and continuation semantics›
theory Continuations
imports
PCF
begin
text‹
\label{sec:continuations}
This is a fairly literal version of
\<^citet>‹"DBLP:conf/icalp/Reynolds74"›, adapted to untyped PCF. A more
abstract account has been given by
\<^citet>‹"DBLP:journals/tcs/Filinski07"› in terms of a monadic meta
language, which is difficult to model in Isabelle (but see
\<^citet>‹"Huffman:MonadTransformers:2012"›).
We begin by giving PCF a continuation semantics following the modern
account of \<^citet>‹"wadler92:_essence_of_funct_progr"›. We use the
symmetric function space ‹('o ValK, 'o) K → ('o ValK, 'o) K›
as our language includes call-by-name.
›
type_synonym ('a, 'o) K = "('a → 'o) → 'o"
domain 'o ValK
= ValKF (lazy appKF :: "('o ValK, 'o) K → ('o ValK, 'o) K")
| ValKTT | ValKFF
| ValKN (lazy "nat")
type_synonym 'o ValKM = "('o ValK, 'o) K"
lemma ValK_case_ID [simp]:
"ValK_case⋅ValKF⋅ValKTT⋅ValKFF⋅ValKN = ID"
apply (rule cfun_eqI)
apply (case_tac x)
apply simp_all
done
lemma below_monic_ValKF [iff]:
"below_monic_cfun ValKF"
by (rule below_monicI) simp
lemma below_monic_ValKN [iff]:
"below_monic_cfun ValKN"
by (rule below_monicI) simp
text‹
We use the standard continuation monad to ease the semantic
definition.
›
definition unitK :: "'o ValK → 'o ValKM" where
"unitK ≡ Λ a. Λ c. c⋅a"
definition bindK :: "'o ValKM → ('o ValK → 'o ValKM) → 'o ValKM" where
"bindK ≡ Λ m k. Λ c. m⋅(Λ a. k⋅a⋅c)"
definition appKM :: "'o ValKM → 'o ValKM → 'o ValKM" where
"appKM ≡ Λ fK xK. bindK⋅fK⋅(Λ (ValKF⋅f). f⋅xK)"
lemma unitK_simps [simp]:
"unitK⋅v⋅c = c⋅v"
unfolding unitK_def by simp
lemma bindK_strict:
"bindK⋅⊥ = ⊥"
unfolding bindK_def by (simp add: eta_cfun)
lemma bindK_unitl:
"bindK⋅(unitK⋅e)⋅f = f⋅e"
unfolding bindK_def unitK_def by (simp add: eta_cfun)
lemma bindK_unitr:
"bindK⋅e⋅unitK = e"
unfolding bindK_def unitK_def by (simp add: eta_cfun)
lemma bindK_assoc:
"bindK⋅(bindK⋅f⋅g)⋅h = bindK⋅f⋅(Λ v. bindK⋅(g⋅v)⋅h)"
unfolding bindK_def unitK_def by simp
lemmas bindK_simps[simp] = bindK_strict bindK_unitl bindK_unitr bindK_assoc
text‹The interpretations of the constants.›
definition
condK :: "'o ValKM → 'o ValKM → 'o ValKM → 'o ValKM"
where
"condK ≡ Λ iK tK eK. bindK⋅iK⋅(Λ i. case i of
ValKF⋅f ⇒ ⊥ | ValKTT ⇒ tK | ValKFF ⇒ eK | ValKN⋅n ⇒ ⊥)"
definition succK :: "'o ValKM → 'o ValKM" where
"succK ≡ Λ nK. bindK⋅nK⋅(Λ (ValKN⋅n). unitK⋅(ValKN⋅(n + 1)))"
definition predK :: "'o ValKM → 'o ValKM" where
"predK ≡ Λ nK. bindK⋅nK⋅(Λ (ValKN⋅n). case n of 0 ⇒ ⊥ | Suc n ⇒ unitK⋅(ValKN⋅n))"
definition isZeroK :: "'o ValKM → 'o ValKM" where
"isZeroK ≡ Λ nK. bindK⋅nK⋅(Λ (ValKN⋅n). unitK⋅(if n = 0 then ValKTT else ValKFF))"
text ‹
A continuation semantics for PCF. If we had defined our direct
semantics using a monad then the correspondence would be more
syntactically obvious.
›
type_synonym 'o EnvK = "'o ValKM Env"
primrec
evalK :: "expr ⇒ 'o EnvK → 'o ValKM"
where
"evalK (Var v) = (Λ ρ. ρ⋅v)"
| "evalK (App f x) = (Λ ρ. appKM⋅(evalK f⋅ρ)⋅(evalK x⋅ρ))"
| "evalK (AbsN v e) = (Λ ρ. unitK⋅(ValKF⋅(Λ x. evalK e⋅(env_ext⋅v⋅x⋅ρ))))"
| "evalK (AbsV v e) = (Λ ρ. unitK⋅(ValKF⋅(Λ x c. x⋅(Λ x'. evalK e⋅(env_ext⋅v⋅(unitK⋅x')⋅ρ)⋅c))))"
| "evalK (Diverge) = (Λ ρ. ⊥)"
| "evalK (Fix v e) = (Λ ρ. μ x. evalK e⋅(env_ext⋅v⋅x⋅ρ))"
| "evalK (tt) = (Λ ρ. unitK⋅ValKTT)"
| "evalK (ff) = (Λ ρ. unitK⋅ValKFF)"
| "evalK (Cond i t e) = (Λ ρ. condK⋅(evalK i⋅ρ)⋅(evalK t⋅ρ)⋅(evalK e⋅ρ))"
| "evalK (Num n) = (Λ ρ. unitK⋅(ValKN⋅n))"
| "evalK (Succ e) = (Λ ρ. succK⋅(evalK e⋅ρ))"
| "evalK (Pred e) = (Λ ρ. predK⋅(evalK e⋅ρ))"
| "evalK (IsZero e) = (Λ ρ. isZeroK⋅(evalK e⋅ρ))"
text‹
To establish the chain completeness (admissibility) of our logical
relation, we need to show that @{term "unitK"} is an \emph{order
monic}, i.e., if @{term "unitK⋅x ⊑ unitK⋅y"} then @{term "x ⊑
y"}. This is an order-theoretic version of injectivity.
In order to define a continuation that witnesses this, we need to be
able to distinguish converging and diverging computations. We
therefore require our observation domain to contain at least two
elements:
›
locale at_least_two_elements =
fixes some_non_bottom_element :: "'o::domain"
assumes some_non_bottom_element: "some_non_bottom_element ≠ ⊥"
text‹
Following \<^citet>‹"DBLP:conf/icalp/Reynolds74"› and \<^citet>‹‹Remark
47› in "DBLP:journals/tcs/Filinski07"› we use the following continuation:
›
lemma cont_below [simp, cont2cont]:
"cont (λx::'a::pcpo. if x ⊑ d then ⊥ else c)"
proof(rule contI2)
show "monofun (λx. if x ⊑ d then ⊥ else c)"
apply (rule monofunI)
apply clarsimp
apply (cut_tac x=x and y=y and z=d in below_trans)
apply auto
done
next
fix Y :: "nat ⇒ 'a::pcpo"
assume Y: "chain Y"
assume "chain (λi. if Y i ⊑ d then ⊥ else c)"
show "(if (⨆ i. Y i) ⊑ d then ⊥ else c) ⊑ (⨆ i. if Y i ⊑ d then ⊥ else c)"
proof(cases "∀i. Y i ⊑ d")
case True hence "Lub Y ⊑ d"
using lub_below_iff[OF Y] by simp
thus ?thesis by simp
next
case False
let ?f = "λi. if Y i ⊑ d then ⊥ else c"
from False have LubY: "¬ Lub Y ⊑ d"
using lub_below_iff[OF Y] by simp
from False have F: "chain ?f"
apply -
apply (rule chainI)
apply clarsimp
apply (cut_tac i=i and j="Suc i" in chain_mono[OF Y])
apply clarsimp
apply (cut_tac x="Y i" and y="Y (Suc i)" and z=d in below_trans)
apply simp_all
done
from False obtain i where Yi: "¬ Y i ⊑ d" by blast
hence M: "max_in_chain i ?f"
apply -
apply (rule max_in_chainI)
apply clarsimp
apply (drule chain_mono[OF Y])
apply (cut_tac x="Y i" and y="Y j" and z=d in below_trans)
apply simp_all
done
from LubY Yi show ?thesis
using iffD1[OF maxinch_is_thelub, OF F M] by simp
qed
qed
text‹›
lemma (in at_least_two_elements) below_monic_unitK [intro, simp]:
"below_monic_cfun (unitK :: 'o ValK → 'o ValKM)"
proof(rule below_monicI)
fix v v' :: "'o ValK"
assume vv': "unitK⋅v ⊑ unitK⋅v'"
let ?k = "Λ x. if x ⊑ v' then ⊥ else some_non_bottom_element"
from vv' have "unitK⋅v⋅?k ⊑ unitK⋅v'⋅?k" by (rule monofun_cfun_fun)
hence "?k⋅v ⊑ ?k⋅v'" by (simp add: unitK_def)
with some_non_bottom_element show "v ⊑ v'" by (auto split: if_split_asm)
qed
subsection‹Logical relation›
text‹
We follow \<^citet>‹"DBLP:conf/icalp/Reynolds74"› by simultaneously
defining a pair of relations over values and functions. Both are
bottom-reflecting, in contrast to the situation for computational
adequacy in \S\ref{sec:compad}. \<^citet>‹"DBLP:journals/tcs/Filinski07"›
differs by assuming that values are always defined, and relates values
and monadic computations.
›
type_synonym 'o lfr = "(ValD, 'o ValKM, ValD → ValD, 'o ValKM → 'o ValKM) lf_pair_rep"
type_synonym 'o lflf = "(ValD, 'o ValKM, ValD → ValD, 'o ValKM → 'o ValKM) lf_pair"
context at_least_two_elements
begin
abbreviation lr_eta_rep_N where
"lr_eta_rep_N ≡ { (e, e') .
(e = ⊥ ∧ e' = ⊥)
∨ (e = ValTT ∧ e' = unitK⋅ValKTT)
∨ (e = ValFF ∧ e' = unitK⋅ValKFF)
∨ (∃n. e = ValN⋅n ∧ e' = unitK⋅(ValKN⋅n)) }"
abbreviation lr_eta_rep_F where
"lr_eta_rep_F ≡ λ(rm, rp). { (e, e') .
(e = ⊥ ∧ e' = ⊥)
∨ (∃f f'. e = ValF⋅f ∧ e' = unitK⋅(ValKF⋅f') ∧ (f, f') ∈ unlr (snd rp)) }"
definition lr_eta_rep where
"lr_eta_rep ≡ λr. lr_eta_rep_N ∪ lr_eta_rep_F r"
definition lr_theta_rep where
"lr_theta_rep ≡ λ(rm, rp). { (f, f') .
(∀(x, x') ∈ unlr (fst (undual rm)). (f⋅x, f'⋅x') ∈ unlr (fst rp)) }"
definition lr_rep :: "'o lfr" where
"lr_rep ≡ λr. (lr_eta_rep r, lr_theta_rep r)"
abbreviation lr :: "'o lflf" where
"lr ≡ λr. (mklr (fst (lr_rep r)), mklr (snd (lr_rep r)))"
text‹
Properties of the logical relation.
›
lemma admS_eta_rep [intro, simp]:
"fst (lr_rep r) ∈ admS"
unfolding lr_rep_def lr_eta_rep_def
apply simp
apply rule
apply (auto intro!: adm_disj simp: split_def)
using adm_below_monic_exists[OF _ below_monic_pair[OF below_monic_ValN below_monic_cfcomp2[OF below_monic_unitK below_monic_ValKN]], where P="λ_. True"]
apply (simp add: prod_eq_iff)
using adm_below_monic_exists[OF _ below_monic_pair_split[OF below_monic_ValF below_monic_cfcomp2[OF below_monic_unitK below_monic_ValKF]], where P="λx. x ∈ unlr (snd (snd r))"]
apply (simp add: prod_eq_iff)
done
lemma admS_theta_rep [intro, simp]:
"snd (lr_rep r) ∈ admS"
proof
show "⊥ ∈ snd (lr_rep r)"
unfolding lr_rep_def lr_theta_rep_def
by (cases r) simp
next
show "adm (λx. x ∈ snd (lr_rep r))"
apply (rule admI)
unfolding lr_rep_def lr_theta_rep_def
apply (clarsimp simp: split_def)
apply (rule admD)
apply (rule adm_subst)
apply force+
done
qed
lemma mono_lr:
shows "mono (lr :: 'o lflf)"
apply (rule monoI)
apply simp
apply (simp add: lr_rep_def)
apply (rule conjI)
apply (force simp: lr_eta_rep_def split_def dual_less_eq_iff unlr_leq[symmetric])
apply (auto simp: lr_theta_rep_def split_def dual_less_eq_iff unlr_leq[symmetric])
apply (drule_tac x="(ae, bc)" in bspec)
apply (case_tac a)
apply (case_tac ab)
apply (auto simp: unlr_leq[symmetric])
done
end
text‹
It takes some effort to set up the minimal invariant relating the two
pairs of domains. One might hope this would be easier using deflations
(which might compose) rather than ``copy'' functions (which certainly
don't).
We elide these as they are tedious.
›
primrec
ValD_copy_i :: "nat ⇒ ValD → ValD"
where
"ValD_copy_i 0 = ⊥"
| "ValD_copy_i (Suc n) = (Λ v. case v of ValF⋅f ⇒ ValF⋅(ValD_copy_i n oo f oo ValD_copy_i n) | ValTT ⇒ ValTT | ValFF ⇒ ValFF | ValN⋅m ⇒ ValN⋅m)"
abbreviation
"ValD_copy_lub ≡ (⨆i. ValD_copy_i i)"
lemma ValD_copy_chain [intro, simp]:
"chain ValD_copy_i"
proof(rule chainI)
fix i show "ValD_copy_i i ⊑ ValD_copy_i (Suc i)"
proof(induct i)
case (Suc i)
{ fix x
have "ValD_copy_i (Suc i)⋅x ⊑ ValD_copy_i (Suc (Suc i))⋅x"
proof(cases x)
case (ValF f) with Suc show ?thesis
by (clarsimp simp: cfcomp1 cfun_below_iff monofun_cfun)
qed simp_all }
thus ?case by (simp add: cfun_below_iff)
qed simp
qed
lemma ValD_copy_lub_ID:
"ValD_copy_lub = ID"
proof -
{ fix x :: ValD
fix i :: nat
have "ValD_take i⋅(ValD_copy_i i⋅(ValD_take i⋅x)) = ValD_take i⋅x"
proof (induct i arbitrary: x)
case (Suc n) thus ?case
by (cases x) (simp_all add: cfun_map_def)
qed simp }
hence "⋀x :: ValD. (⨆i. ValD_take i⋅(ValD_copy_i i⋅(ValD_take i⋅x))) = (⨆i. ValD_take i⋅x)"
by (blast intro: lub_eq)
thus ?thesis by (simp add: lub_distribs ValD.lub_take cfun_eq_iff)
qed
text‹
Continuations: we need to ensure the observation type is always the
same.
›
definition
KM_map :: "('o ValK → 'o ValK) → 'o ValKM → 'o ValKM"
where
"KM_map ≡ Λ f. cfun_map⋅(cfun_map⋅f⋅ID)⋅ID"
lemma KM_map_id [intro, simp]:
"KM_map⋅ID = ID"
unfolding KM_map_def by (simp add: cfun_map_ID)
lemma KM_map_strict [intro, simp]:
"KM_map⋅f⋅⊥ = ⊥"
unfolding KM_map_def by (simp add: cfun_map_def)
primrec
ValK_copy_i :: "nat ⇒ 'o ValK → 'o ValK"
where
"ValK_copy_i 0 = ⊥"
| "ValK_copy_i (Suc n) = (Λ v. case v of ValKF⋅f ⇒ ValKF⋅(cfun_map⋅(KM_map⋅(ValK_copy_i n))⋅(KM_map⋅(ValK_copy_i n))⋅f) | ValKTT ⇒ ValKTT | ValKFF ⇒ ValKFF | ValKN⋅m ⇒ ValKN⋅m)"
abbreviation
"ValK_copy ≡ (⨆i. ValK_copy_i i)"
lemma ValK_copy_chain [intro, simp]:
"chain (ValK_copy_i :: nat ⇒ 'o ValK → 'o ValK)"
proof(rule chainI)
fix i show "ValK_copy_i i ⊑ (ValK_copy_i (Suc i) :: 'o ValK → 'o ValK)"
proof(induct i)
case (Suc i)
{ fix x :: "'o ValK"
have "ValK_copy_i (Suc i)⋅x ⊑ ValK_copy_i (Suc (Suc i))⋅x"
proof(cases x)
case (ValKF f) with Suc show ?thesis by (clarsimp simp: monofun_cfun KM_map_def)
qed simp_all }
thus ?case by (simp add: cfun_below_iff)
qed simp
qed
lemma ValK_copy_fix:
"ValK_copy = (ID :: 'o ValK → 'o ValK)"
proof -
{ fix x :: "'o ValK"
fix i :: nat
have "ValK_take i⋅(ValK_copy_i i⋅(ValK_take i⋅x)) = ValK_take i⋅x"
proof (induct i arbitrary: x)
case (Suc n) thus ?case
by (cases x) (simp_all add: KM_map_def cfun_map_def)
qed simp }
hence "⋀x :: 'o ValK. (⨆i. ValK_take i⋅(ValK_copy_i i⋅(ValK_take i⋅x))) = (⨆i. ValK_take i⋅x)"
by (blast intro: lub_eq)
thus ?thesis by (simp add: lub_distribs ValK.lub_take cfun_eq_iff)
qed
lemma ValK_strict [intro, simp]:
"ValK_copy⋅⊥ = ⊥"
by (simp add: ValK_copy_fix)
text‹
We need to respect the purported domain structure, and positive and
negative occurrences.
›
fixrec
ValD_copy_rec :: "((ValD → ValD) × ((ValD → ValD) → (ValD → ValD)))
→ ((ValD → ValD) × ((ValD → ValD) → (ValD → ValD)))"
where
"ValD_copy_rec⋅r =
(Λ v. case v of ValF⋅f ⇒ ValF⋅(snd r⋅f) | ValTT ⇒ ValTT | ValFF ⇒ ValFF | ValN⋅n ⇒ ValN⋅n,
Λ f. cfun_map⋅(strictify⋅(fst r))⋅(strictify⋅(fst r))⋅f)"
abbreviation
ValD_copy_eta :: "nat ⇒ ValD → ValD"
where
"ValD_copy_eta i ≡ fst (iterate i⋅ValD_copy_rec⋅⊥)"
abbreviation
ValD_copy_theta :: "nat ⇒ (ValD → ValD) → (ValD → ValD)"
where
"ValD_copy_theta i ≡ snd (iterate i⋅ValD_copy_rec⋅⊥)"
lemma ValD_copy_eta_theta_strict [intro, simp]:
"ValD_copy_eta n⋅⊥ = ⊥"
"ValD_copy_theta n⋅⊥ = ⊥"
by (induct n) (simp_all add: cfun_map_def)
lemma ValD_copy_fix_strict [simp]:
"fst (fix⋅ValD_copy_rec)⋅⊥ = ⊥"
"snd (fix⋅ValD_copy_rec)⋅⊥ = ⊥"
by (subst fix_eq, simp add: cfun_map_def)+
lemma ValD_copy_rec_ValD_copy_lub:
"fix⋅ValD_copy_rec = (ValD_copy_lub, cfun_map⋅ValD_copy_lub⋅ValD_copy_lub)" (is "?lhs = ?rhs")
proof(rule below_antisym)
show "?lhs ⊑ ?rhs"
apply (rule fix_least)
apply (simp add: eta_cfun strictify_cancel ValD_copy_lub_ID cfun_map_def ID_def)
done
next
{ fix i have "ValD_copy_i i ⊑ fst (fix⋅ValD_copy_rec)"
proof(induct i)
case (Suc i) thus ?case
apply -
apply (subst fix_eq)
apply (subst fix_eq)
apply (simp add: eta_cfun strictify_cancel cfcomp1 cfun_map_def)
apply (intro monofun_cfun_fun monofun_cfun_arg)
apply (simp add: eta_cfun strictify_cancel monofun_cfun cfcomp1 cfun_map_def cfun_below_iff)
done
qed simp }
hence D: "ValD_copy_lub ⊑ fst (fix⋅ValD_copy_rec)" by (simp add: lub_below_iff)
moreover
from D
have "cfun_map⋅ValD_copy_lub⋅ValD_copy_lub ⊑ snd (fix⋅ValD_copy_rec)"
by (subst fix_eq) (simp add: eta_cfun strictify_cancel monofun_cfun)
ultimately show "?rhs ⊑ ?lhs" by (simp add: prod_belowI)
qed
lemma fix_ValD_copy_rec_ID:
"fix⋅ValD_copy_rec = (ID, ID)"
using ValD_copy_rec_ValD_copy_lub ValD_copy_lub_ID cfun_map_ID
by simp
fixrec
ValK_copy_rec :: "(('o ValKM → 'o ValKM) × (('o ValKM → 'o ValKM) → ('o ValKM → 'o ValKM)))
→ ('o ValKM → 'o ValKM) × (('o ValKM → 'o ValKM) → ('o ValKM → 'o ValKM))"
where
"ValK_copy_rec⋅r =
(Λ vm. KM_map⋅(Λ v. case v of ValKF⋅f ⇒ ValKF⋅(snd r⋅f) | ValKTT ⇒ ValKTT | ValKFF ⇒ ValKFF | ValKN⋅a ⇒ ValKN⋅a)⋅vm,
Λ f. cfun_map⋅(strictify⋅(fst r))⋅(strictify⋅(fst r))⋅f)"
abbreviation
ValK_copy_eta
where
"ValK_copy_eta i ≡ fst (iterate i⋅ValK_copy_rec⋅⊥)"
abbreviation
ValK_copy_theta
where
"ValK_copy_theta i ≡ snd (iterate i⋅ValK_copy_rec⋅⊥)"
lemma ValK_copy_strict [intro, simp]:
"ValK_copy_eta n⋅⊥ = (⊥ :: 'o ValKM)"
"ValK_copy_theta n⋅⊥ = (⊥ :: 'o ValKM → 'o ValKM)"
by (induct n) (simp_all add: cfun_map_def)
lemma ValK_copy_fix_strict [simp]:
"fst (fix⋅ValK_copy_rec)⋅⊥ = ⊥"
"snd (fix⋅ValK_copy_rec)⋅⊥ = ⊥"
by (subst fix_eq, simp add: cfun_map_def)+
lemma ValK_copy_rec_ValK_copy:
"fix⋅ValK_copy_rec
= (KM_map⋅(ValK_copy :: 'o ValK → 'o ValK),
cfun_map⋅(KM_map⋅ValK_copy)⋅(KM_map⋅ValK_copy))" (is "?lhs = ?rhs")
proof(rule below_antisym)
show "?lhs ⊑ ?rhs"
apply (rule fix_least)
apply (simp add: eta_cfun strictify_cancel cfun_map_def ID_def)
apply (intro cfun_eqI)
apply (simp add: KM_map_def cfun_map_def ValK_copy_fix eta_cfun)
done
next
{ fix i
have "KM_map⋅(ValK_copy_i i :: 'o ValK → 'o ValK) ⊑ fst (fix⋅ValK_copy_rec)"
and "(ValK_copy_i i :: 'o ValK → 'o ValK) ⊑ ValK_case⋅(Λ f. ValKF⋅(snd (fix⋅ValK_copy_rec)⋅f))⋅ValKTT⋅ValKFF⋅ValKN"
proof(induct i)
case 0
{ case 1 show ?case
apply (subst fix_eq)
apply (auto iff: cfun_below_iff intro!: monofun_cfun_arg simp: KM_map_def cfun_map_def eta_cfun)
done }
{ case 2 show ?case by simp }
next
case (Suc i)
{ case 1 from Suc show ?case
apply -
apply (subst fix_eq)
apply (subst fix_eq)
apply (simp add: eta_cfun strictify_cancel cfcomp1 cfun_map_def KM_map_def)
apply (intro cfun_belowI)
apply (simp add: eta_cfun strictify_cancel cfcomp1 cfun_map_def KM_map_def)
apply (intro monofun_cfun_arg)
apply (intro cfun_belowI)
apply (simp add: eta_cfun strictify_cancel cfcomp1 cfun_map_def KM_map_def)
apply (intro monofun_cfun_arg)
apply (simp add: eta_cfun strictify_cancel monofun_cfun cfcomp1 cfun_map_def)
apply (intro monofun_cfun)
apply simp_all
apply (intro cfun_belowI)
apply (simp add: eta_cfun strictify_cancel monofun_cfun cfcomp1 cfun_map_def)
apply (intro cfun_belowI)
apply (subst fix_eq)
apply (simp add: eta_cfun strictify_cancel monofun_cfun cfcomp1 KM_map_def cfun_map_def)
apply (intro monofun_cfun)
apply simp_all
apply (subst fix_eq)
apply (intro cfun_belowI)
apply (simp add: eta_cfun strictify_cancel monofun_cfun cfcomp1 KM_map_def cfun_map_def)
apply (intro monofun_cfun)
apply simp_all
apply (intro cfun_belowI)
apply simp
apply (intro monofun_cfun)
apply simp_all
apply (intro cfun_belowI)
apply simp
apply (intro monofun_cfun)
apply simp_all
done }
{ case 2 from Suc show ?case
apply -
apply (subst fix_eq)
apply (subst fix_eq)
apply (auto simp: eta_cfun strictify_cancel cfcomp1 cfun_map_def KM_map_def cfun_below_iff intro!: monofun_cfun)
done }
qed }
hence "(⨆i. KM_map⋅(ValK_copy_i i :: 'o ValK → 'o ValK)) ⊑ fst (fix⋅ValK_copy_rec)"
by (simp add: lub_below_iff)
hence D: "KM_map⋅(ValK_copy :: 'o ValK → 'o ValK) ⊑ fst (fix⋅ValK_copy_rec)"
by (simp add: contlub_cfun_arg[symmetric])
from D
have E: "cfun_map⋅(KM_map⋅(ValK_copy :: 'o ValK → 'o ValK))⋅(KM_map⋅ValK_copy) ⊑ snd (fix⋅ValK_copy_rec)"
apply (subst fix_eq)
apply (simp add: eta_cfun strictify_cancel KM_map_def)
apply (intro monofun_cfun)
apply simp_all
done
show "?rhs ⊑ ?lhs" by (simp add: prod_belowI D E)
qed
lemma fix_ValK_copy_rec_ID:
"fix⋅ValK_copy_rec = (ID, ID)"
by (simp add: ValK_copy_rec_ValK_copy ValK_copy_fix cfun_map_ID)
lemma (in at_least_two_elements) min_inv_lr:
assumes "fst ea⋅⊥ = ⊥"
assumes "fst eb⋅⊥ = ⊥"
assumes "eRSP ea eb R S"
shows "eRSP (ValD_copy_rec⋅ea) (ValK_copy_rec⋅eb) (dual ((lr :: 'o lflf) (dual S, undual R))) (lr (R, S))"
using assms some_non_bottom_element
apply (simp add: split_def)
apply (auto simp: split_def lr_rep_def lr_eta_rep_def lr_theta_rep_def KM_map_def cfun_map_def unitK_def)
apply (force simp: cfun_map_def strictify_cancel unitK_def)
done
sublocale at_least_two_elements < F: DomSolP lr ValD_copy_rec ValK_copy_rec
apply standard
apply (rule mono_lr)
apply (rule fix_ValD_copy_rec_ID)
apply (rule fix_ValK_copy_rec_ID)
apply (simp_all add: cfun_map_def)[4]
apply (erule (2) min_inv_lr)
done
subsection‹A retraction between the two definitions›
text‹
We can use the relation to establish a strong connection between the
direct and continuation semantics. All results depend on the
observation type being rich enough.
›
context at_least_two_elements
begin
abbreviation mrel (‹η: _ ↦ _› [50, 51] 50) where
"η: x ↦ x' ≡ (x, x') ∈ unlr (fst F.delta)"
abbreviation vrel (‹θ: _ ↦ _› [50, 51] 50) where
"θ: y ↦ y' ≡ (y, y') ∈ unlr (snd F.delta)"
lemma F_bottom_triv [intro, simp]:
"η: ⊥ ↦ ⊥"
"θ: ⊥ ↦ ⊥"
by simp_all
lemma etaI [intro, simp]:
"η: ValTT ↦ unitK⋅ValKTT"
"η: ValFF ↦ unitK⋅ValKFF"
"η: ValN⋅n ↦ unitK⋅(ValKN⋅n)"
by (subst F.delta_sol, simp, simp add: lr_rep_def lr_eta_rep_def)+
lemma eta_F:
"θ: f ↦ f' ⟹ η: ValF⋅f ↦ unitK⋅(ValKF⋅f')"
apply (subst F.delta_sol)
apply simp
apply (subst lr_rep_def)
apply (fastforce simp: lr_eta_rep_def split_def)
done
lemma theta_F:
"(⋀x x'. η: x ↦ x' ⟹ η: f⋅x ↦ f'⋅x') ⟹ θ: f ↦ f'"
apply (subst F.delta_sol)
apply simp
apply (subst lr_rep_def)
apply (simp add: lr_theta_rep_def split_def)
done
lemma eta_induct[case_names bottom N F, consumes 1]:
"⟦ η: x ↦ x';
⟦ x = ⊥; x' = ⊥ ⟧ ⟹ P x x';
⋀n. ⟦ x = ValTT; x' = unitK⋅ValKTT ⟧ ⟹ P x x';
⋀n. ⟦ x = ValFF; x' = unitK⋅ValKFF ⟧ ⟹ P x x';
⋀n. ⟦ x = ValN⋅n; x' = unitK⋅(ValKN⋅n) ⟧ ⟹ P x x';
⋀f f'. ⟦ x = ValF⋅f; x' = unitK⋅(ValKF⋅f'); θ: f ↦ f' ⟧ ⟹ P x x'
⟧ ⟹ P x x'"
apply (cases x)
apply (subst (asm) F.delta_sol, simp, simp add: lr_rep_def lr_eta_rep_def)
defer
apply (subst (asm) F.delta_sol, simp, simp add: lr_rep_def lr_eta_rep_def)
apply (subst (asm) F.delta_sol, simp, simp add: lr_rep_def lr_eta_rep_def)
apply (subst (asm) F.delta_sol, simp, simp add: lr_rep_def lr_eta_rep_def)
apply simp
apply (subst (asm) F.delta_sol)
apply simp
apply (subst (asm) lr_rep_def)
apply (subst (asm) lr_eta_rep_def)
apply clarsimp
done
lemma theta_induct[case_names F, consumes 1]:
"⟦ θ: f ↦ f';
(⋀x x'. η: x ↦ x' ⟹ η: f⋅x ↦ f'⋅x') ⟹ P f f'
⟧ ⟹ P f f'"
apply (subst (asm) F.delta_sol)
apply simp
apply (subst (asm) lr_rep_def)
apply (subst (asm) lr_theta_rep_def)
apply fastforce
done
text‹
Theorem 1 from \<^citet>‹"DBLP:conf/icalp/Reynolds74"›.
›
lemma AbsV_aux:
assumes "η: ValF⋅f ↦ unitK⋅(ValKF⋅f')"
shows "η: ValF⋅(strictify⋅f) ↦ unitK⋅(ValKF⋅(Λ x c. x⋅(Λ x'. f'⋅(unitK⋅x')⋅c)))"
apply (rule eta_F)
apply (rule theta_F)
using assms
apply (rule eta_induct)
apply simp_all
apply (drule injD[OF below_monic_inj[OF below_monic_unitK]])
apply clarsimp
apply (erule theta_induct)
apply (erule eta_induct)
apply (simp_all add: eta_cfun eta_F)
done
text‹›
theorem Theorem1:
assumes "∀v. η: ρ⋅v ↦ ρ'⋅v"
shows "η: evalD e⋅ρ ↦ evalK e⋅ρ'"
using assms
proof(induct e arbitrary: ρ ρ')
case App show ?case
apply simp
apply (simp add: appKM_def bindK_def)
using App.hyps(1)[OF App(3)]
apply (rule eta_induct)
apply simp_all
apply (simp add: eta_cfun)
apply (erule theta_induct)
using App.hyps(2)[OF App(3)]
apply simp
done
next
case AbsN show ?case
apply simp
apply (rule eta_F)
apply (rule theta_F)
apply simp
apply (rule AbsN.hyps)
using AbsN(2)
unfolding env_ext_def
apply simp
done
next
case (AbsV v e ρ ρ')
have "η: ValF⋅(Λ x. evalD e⋅(env_ext⋅v⋅x⋅ρ)) ↦ unitK⋅(ValKF⋅(Λ x. evalK e⋅(env_ext⋅v⋅x⋅ρ')))"
apply (rule eta_F)
apply (rule theta_F)
apply simp
apply (rule AbsV.hyps)
using AbsV(2)
unfolding env_ext_def
apply simp
done
thus ?case by (fastforce dest: AbsV_aux)
next
case Fix thus ?case
apply simp
apply (rule parallel_fix_ind)
apply (simp_all add: env_ext_def)
done
next
case Cond thus ?case
apply (simp add: cond_def condK_def eta_cfun)
using Cond(1)[OF Cond(4)]
apply (rule eta_induct)
apply simp_all
done
next
case Succ thus ?case
apply (simp add: succ_def succK_def eta_cfun)
using Succ(1)[OF Succ(2)]
apply (rule eta_induct)
apply simp_all
done
next
case Pred thus ?case
apply (simp add: pred_def predK_def eta_cfun)
using Pred(1)[OF Pred(2)]
apply (rule eta_induct)
apply (simp_all split: nat.split)
done
next
case IsZero thus ?case
apply (simp add: isZero_def isZeroK_def eta_cfun)
using IsZero(1)[OF IsZero(2)]
apply (rule eta_induct)
apply (simp_all split: nat.split)
done
qed simp_all
end
text‹
The retraction between the two value and monadic value spaces.
Note we need to work with an observation type that can represent the
``explicit values'', i.e. @{typ "'o ValK"}.
›
locale value_retraction =
fixes VtoO :: "'o ValK → 'o"
fixes OtoV :: "'o → 'o ValK"
assumes OV: "OtoV oo VtoO = ID"
sublocale value_retraction < at_least_two_elements "VtoO⋅(ValKN⋅0)"
using OV by - (standard, simp add: injection_defined cfcomp1 cfun_eq_iff)
context value_retraction
begin
fun
DtoKM_i :: "nat ⇒ ValD → 'o ValKM"
and
KMtoD_i :: "nat ⇒ 'o ValKM → ValD"
where
"DtoKM_i 0 = ⊥"
| "DtoKM_i (Suc n) = (Λ v. case v of
ValF⋅f ⇒ unitK⋅(ValKF⋅(cfun_map⋅(KMtoD_i n)⋅(DtoKM_i n)⋅f))
| ValTT ⇒ unitK⋅ValKTT
| ValFF ⇒ unitK⋅ValKFF
| ValN⋅m ⇒ unitK⋅(ValKN⋅m))"
| "KMtoD_i 0 = ⊥"
| "KMtoD_i (Suc n) = (Λ v. case OtoV⋅(v⋅VtoO) of
ValKF⋅f ⇒ ValF⋅(cfun_map⋅(DtoKM_i n)⋅(KMtoD_i n)⋅f)
| ValKTT ⇒ ValTT
| ValKFF ⇒ ValFF
| ValKN⋅m ⇒ ValN⋅m)"
abbreviation "DtoKM ≡ (⨆i. DtoKM_i i)"
abbreviation "KMtoD ≡ (⨆i. KMtoD_i i)"
lemma DtoKM_KMtoD_chain [intro, simp]:
"chain DtoKM_i"
"chain KMtoD_i"
proof -
let ?C = "λi. (DtoKM_i i, KMtoD_i i)"
have "chain ?C"
proof(rule chainI)
fix i show "?C i ⊑ ?C (Suc i)"
proof(induct i)
case (Suc i) show ?case
proof(rule monofun_pair)
show "DtoKM_i (Suc i) ⊑ DtoKM_i (Suc (Suc i))"
proof(rule cfun_belowI)
fix x from Suc show "DtoKM_i (Suc i)⋅x ⊑ DtoKM_i (Suc (Suc i))⋅x"
by (cases x) (auto intro!: monofun_cfun simp: cfun_map_def cfun_below_iff)
qed
show "KMtoD_i (Suc i) ⊑ KMtoD_i (Suc (Suc i))"
proof(rule cfun_belowI)
fix x from Suc show "KMtoD_i (Suc i)⋅x ⊑ KMtoD_i (Suc (Suc i))⋅x"
apply (simp add: eta_cfun)
apply (intro monofun_cfun_fun monofun_cfun_arg)
apply (intro cfun_belowI)
apply (auto intro: monofun_cfun)
done
qed
qed
qed simp
qed
then show "chain DtoKM_i" "chain KMtoD_i"
by (auto dest: ch2ch_fst ch2ch_snd)
qed
text‹
Lemma 1 from \<^citet>‹"DBLP:conf/icalp/Reynolds74"›.
›
lemma Lemma1:
"η: x ↦ DtoKM⋅x"
"η: x ↦ x' ⟹ x = KMtoD⋅x'"
proof -
have K: "η: ValD_copy_i i⋅x ↦ DtoKM_i i⋅x"
and L: "η: x ↦ x' ⟹ ValD_copy_i i⋅x = KMtoD_i i⋅x'" for x x' i
proof(induct i arbitrary: x x')
case (Suc i)
{ case 1 show ?case
apply (cases x)
apply simp_all
apply (rule eta_F)
apply (rule theta_F)
using Suc
apply simp
done }
{ case 2 thus ?case
apply (induct rule: eta_induct)
using OV
apply (simp_all add: cfun_eq_iff retraction_strict)
apply (clarsimp simp: cfun_eq_iff)
apply (erule theta_induct)
using Suc
apply simp
done }
qed simp_all
let ?C1 = "λi. (ValD_copy_i i, DtoKM_i i)"
let ?P1 = "λf. η: (fst f)⋅x ↦ (snd f)⋅x"
have "adm ?P1" by (rule adm_subst) simp_all
with K
have "?P1 (⨆i. ValD_copy_i i, ⨆i. DtoKM_i i)"
using admD[where P="?P1" and Y="?C1"] lub_prod[where S="?C1"] by simp
moreover
{ fix x :: ValD
fix x' :: "'o ValKM"
let ?C2 = "λi. (ValD_copy_i i, KMtoD_i i)"
let ?P2 = "λf. (fst f)⋅x = (snd f)⋅x'"
have "adm (λf. ?P2 f)" by simp
with L have "η: x ↦ x' ⟹ ?P2 (⨆i. ValD_copy_i i, ⨆i. KMtoD_i i)"
using admD[where P="?P2" and Y="?C2"] lub_prod[where S="?C2"]
by simp }
ultimately show
"η: x ↦ DtoKM⋅x"
"η: x ↦ x' ⟹ x = KMtoD⋅x'"
by (simp_all add: ValD_copy_lub_ID)
qed
text‹
Theorem 2 from \<^citet>‹"DBLP:conf/icalp/Reynolds74"›.
›
theorem Theorem2: "evalD e⋅ρ = KMtoD⋅(evalK e⋅(DtoKM oo ρ))"
using Lemma1(2)[OF Theorem1] Lemma1(1) by (simp add: cfcomp1)
end
text‹
\<^citet>‹‹Remark~48› in "DBLP:journals/tcs/Filinski07"› observes that there
will not be a retraction between direct and continuation semantics for
languages with richer notions of effects.
It should be routine to extend the above approach to the higher-order
backtracking language of \<^citet>‹"DBLP:conf/icfp/WandV04"›.
I wonder if it is possible to construct continuation semantics from
direct semantics as proposed by
\<^citet>‹"DBLP:journals/jacm/SethiT80"›. Roughly we might hope to lift a
retraction between two value domains to a retraction at higher types
by synthesising a suitable logical relation.
›
end