Theory AbsCFComp
section ‹The abstract semantics is computable›
theory AbsCFComp
imports AbsCF Computability FixTransform CPSUtils MapSets
begin
default_sort type
text ‹
The point of the abstract semantics is that it is computable. To show this, we exploit the special structure of ‹\<aF>› and ‹\<aC>›: Each call adds some elements to the result set and joins this with the results from a number of recursive calls. So we separate these two actions into separate functions. These take as arguments the direct sum of ‹\<afstate>› and ‹\<acstate>›, i.e.\ we treat the two mutually recursive functions now as one.
‹abs_g› gives the local result for the given argument.
›
fixrec abs_g :: "('c::contour \<afstate> + 'c \<acstate>) discr → 'c \<aans>"
where "abs_g⋅x = (case undiscr x of
(Inl (PC (Lambda lab vs c, β), as, ve, b)) ⇒ {}
| (Inl (PP (Plus c),[_,_,cnts],ve,b)) ⇒
let b' = \<anb> b c;
β = [c ↦ b]
in {((c, β), cont) | cont . cont ∈ cnts}
| (Inl (PP (prim.If ct cf),[_, cntts, cntfs],ve,b)) ⇒
(( let b' = \<anb> b ct;
β = [ct ↦ b]
in {((ct, β), cnt) | cnt . cnt ∈ cntts}
)∪(
let b' = \<anb> b cf;
β = [cf ↦ b]
in {((cf, β), cnt) | cnt . cnt ∈ cntfs}
))
| (Inl (AStop,[_],_,_)) ⇒ {}
| (Inl _) ⇒ ⊥
| (Inr (App lab f vs,β,ve,b)) ⇒
let fs = \<aA> f β ve;
as = map (λv. \<aA> v β ve) vs;
b' = \<anb> b lab
in {((lab, β),f') | f' . f'∈ fs}
| (Inr (Let lab ls c',β,ve,b)) ⇒ {}
)"
text ‹
‹abs_R› gives the set of arguments passed to the recursive calls.
›
fixrec abs_R :: "('c::contour \<afstate> + 'c \<acstate>) discr → ('c::contour \<afstate> + 'c \<acstate>) discr set"
where "abs_R⋅x = (case undiscr x of
(Inl (PC (Lambda lab vs c, β), as, ve, b)) ⇒
(if length vs = length as
then let β' = β (lab ↦ b);
ve' = ve ∪. (⋃. (map (λ(v,a). {(v,b) := a}.) (zip vs as)))
in {Discr (Inr (c,β',ve',b))}
else ⊥)
| (Inl (PP (Plus c),[_,_,cnts],ve,b)) ⇒
let b' = \<anb> b c;
β = [c ↦ b]
in (⋃cnt∈cnts. {Discr (Inl (cnt,[{}],ve,b'))})
| (Inl (PP (prim.If ct cf),[_, cntts, cntfs],ve,b)) ⇒
(( let b' = \<anb> b ct;
β = [ct ↦ b]
in (⋃cnt∈cntts . {Discr (Inl (cnt,[],ve,b'))})
)∪(
let b' = \<anb> b cf;
β = [cf ↦ b]
in (⋃cnt∈cntfs . {Discr (Inl (cnt,[],ve,b'))})
))
| (Inl (AStop,[_],_,_)) ⇒ {}
| (Inl _) ⇒ ⊥
| (Inr (App lab f vs,β,ve,b)) ⇒
let fs = \<aA> f β ve;
as = map (λv. \<aA> v β ve) vs;
b' = \<anb> b lab
in (⋃f' ∈ fs. {Discr (Inl (f',as,ve,b'))})
| (Inr (Let lab ls c',β,ve,b)) ⇒
let b' = \<anb> b lab;
β' = β (lab ↦ b');
ve' = ve ∪. (⋃. (map (λ(v,l). {(v,b') := (\<aA> (L l) β' ve)}.) ls))
in {Discr (Inr (c',β',ve',b'))}
)"
text ‹
The initial argument vector, as created by ‹\<aPR>›.
›
definition initial_r :: "prog ⇒ ('c::contour \<afstate> + 'c \<acstate>) discr"
where "initial_r prog = Discr (Inl
(the_elem (\<aA> (L prog) Map.empty {}.), [{AStop}], {}., \<abinit>))"
subsection ‹Towards finiteness›
text ‹
We need to show that the set of possible arguments for a given program ‹p› is finite. Therefore, we define the set of possible procedures, of possible arguments to ‹\<aF>›, or possible arguments to ‹\<aC>› and of possible arguments.
›
definition proc_poss :: "prog ⇒ 'c::contour proc set"
where "proc_poss p = PC ` (lambdas p × maps_over (labels p) UNIV) ∪ PP ` prims p ∪ {AStop}"
definition fstate_poss :: "prog ⇒ 'c::contour a_fstate set"
where "fstate_poss p = (proc_poss p × NList (Pow (proc_poss p)) (call_list_lengths p) × smaps_over (vars p × UNIV) (proc_poss p) × UNIV)"
definition cstate_poss :: "prog ⇒ 'c::contour a_cstate set"
where "cstate_poss p = (calls p × maps_over (labels p) UNIV × smaps_over (vars p × UNIV) (proc_poss p) × UNIV)"
definition arg_poss :: "prog ⇒ ('c::contour a_fstate + 'c a_cstate) discr set"
where "arg_poss p = Discr ` (fstate_poss p <+> cstate_poss p)"
text ‹
Using the auxiliary results from @{theory "Shivers-CFA.CPSUtils"}, we see that the argument space as defined here is finite.
›
lemma finite_arg_space: "finite (arg_poss p)"
unfolding arg_poss_def and cstate_poss_def and fstate_poss_def and proc_poss_def
by (auto intro!: finite_cartesian_product finite_imageI maps_over_finite smaps_over_finite finite_UNIV finite_Nlist)
text ‹
But is it closed? I.e.\ if we pass a member of ‹arg_poss› to ‹abs_R›, are the generated recursive call arguments also in ‹arg_poss›? This is shown in ‹arg_space_complete›, after proving an auxiliary result about the possible outcome of a call to ‹\<aA>› and an admissibility lemma.
›
lemma evalV_possible:
assumes f: "f ∈ \<aA> d β ve"
and d: "d ∈ vals p"
and ve: "ve ∈ smaps_over (vars p × UNIV) (proc_poss p)"
and β: "β ∈ maps_over (labels p) UNIV"
shows "f ∈ proc_poss p"
proof (cases "(d,β,ve)" rule: evalV_a.cases)
case (1 cl β' ve')
thus ?thesis using f by auto next
case (2 prim β' ve')
thus ?thesis using d f
by (auto dest: vals1 simp add:proc_poss_def)
next
case (3 l var β' ve')
thus ?thesis using f d smaps_over_im[OF _ ve]
by (auto split:option.split_asm dest: vals2)
next
case (4 l β ve)
thus ?thesis using f d β
by (auto dest!: vals3 simp add:proc_poss_def)
qed
lemma adm_subset: "cont (λx. f x) ⟹ adm (λx. f x ⊆ S)"
by (subst sqsubset_is_subset[THEN sym], intro adm_lemmas cont2cont)
lemma arg_space_complete:
"state ∈ arg_poss p ⟹ abs_R⋅state ⊆ arg_poss p"
proof(induct rule: abs_R.induct[case_names Admissibility Bot Step])
case Admissibility show ?case
by (intro adm_lemmas adm_subset cont2cont)
next
case Bot show ?case by simp next
case (Step abs_R)
note state = Step(2)
show ?case
proof (cases state)
case (Discr state') show ?thesis
proof (cases state')
case (Inl fstate) show ?thesis
using Inl Discr state
proof (cases fstate rule: a_fstate_case, auto)
txt ‹Case Lambda›
fix l vs c β as ve b
assume "Discr (Inl (PC (Lambda l vs c, β), as, ve, b)) ∈ arg_poss p"
hence lam: "Lambda l vs c ∈ lambdas p"
and beta: "β ∈ maps_over (labels p) UNIV "
and ve: "ve ∈ smaps_over (vars p × UNIV) (proc_poss p)"
and as: "as ∈ NList (Pow (proc_poss p)) (call_list_lengths p)"
unfolding arg_poss_def fstate_poss_def proc_poss_def by auto
from lam have "c ∈ calls p"
by (rule lambdas1)
moreover
from lam have "l ∈ labels p"
by (rule lambdas2)
with beta have "β(l ↦ b) ∈ maps_over (labels p) UNIV"
by (rule maps_over_upd, auto)
moreover
from lam have vs: "set vs ⊆ vars p" by (rule lambdas3)
from as have "∀ x ∈ set as. x ∈ Pow (proc_poss p)"
unfolding NList_def nList_def by auto
with vs have "ve ∪. ⋃.map (λ(v, y). { (v, b) := y}.) (zip vs as)
∈ smaps_over (vars p × UNIV) (proc_poss p)" (is "?ve' ∈ _")
by (auto intro!: smaps_over_un[OF ve] smaps_over_Union smaps_over_singleton)
(auto simp add:set_zip)
ultimately
have "(c, β(l ↦ b), ?ve', b) ∈ cstate_poss p" (is "?cstate ∈ _")
unfolding cstate_poss_def by simp
thus "Discr (Inr ?cstate) ∈ arg_poss p"
unfolding arg_poss_def by auto
next
txt ‹Case Plus›
fix ve b l v1 v2 cnts cnt
assume "Discr (Inl (PP (prim.Plus l), [v1, v2, cnts], ve, b)) ∈ arg_poss p"
and "cnt ∈ cnts"
hence "cnt ∈ proc_poss p"
and "ve ∈ smaps_over (vars p × UNIV) (proc_poss p)"
unfolding arg_poss_def fstate_poss_def NList_def nList_def
by auto
moreover
have "[{}] ∈ NList (Pow (proc_poss p)) (call_list_lengths p)"
unfolding call_list_lengths_def NList_def nList_def by auto
ultimately
have "(cnt, [{}], ve, \<anb> b l) ∈ fstate_poss p"
unfolding fstate_poss_def by auto
thus "Discr (Inl (cnt, [{}], ve, \<anb> b l)) ∈ arg_poss p"
unfolding arg_poss_def by auto
next
txt ‹Case If (true case)›
fix ve b l1 l2 v cntst cntsf cnt
assume "Discr (Inl (PP (prim.If l1 l2), [v, cntst, cntsf], ve, b)) ∈ arg_poss p"
and "cnt ∈ cntst"
hence "cnt ∈ proc_poss p"
and "ve ∈ smaps_over (vars p × UNIV) (proc_poss p)"
unfolding arg_poss_def fstate_poss_def NList_def nList_def
by auto
moreover
have "[] ∈ NList (Pow (proc_poss p)) (call_list_lengths p)"
unfolding call_list_lengths_def NList_def nList_def by auto
ultimately
have "(cnt, [], ve, \<anb> b l1) ∈ fstate_poss p"
unfolding fstate_poss_def by auto
thus "Discr (Inl (cnt, [], ve, \<anb> b l1)) ∈ arg_poss p"
unfolding arg_poss_def by auto
next
txt ‹Case If (false case)›
fix ve b l1 l2 v cntst cntsf cnt
assume "Discr (Inl (PP (prim.If l1 l2), [v, cntst, cntsf], ve, b)) ∈ arg_poss p"
and "cnt ∈ cntsf"
hence "cnt ∈ proc_poss p"
and "ve ∈ smaps_over (vars p × UNIV) (proc_poss p)"
unfolding arg_poss_def fstate_poss_def NList_def nList_def
by auto
moreover
have "[] ∈ NList (Pow (proc_poss p)) (call_list_lengths p)"
unfolding call_list_lengths_def NList_def nList_def by auto
ultimately
have "(cnt, [], ve, \<anb> b l2) ∈ fstate_poss p"
unfolding fstate_poss_def by auto
thus "Discr (Inl (cnt, [], ve, \<anb> b l2)) ∈ arg_poss p"
unfolding arg_poss_def by auto
qed
next
case (Inr cstate)
show ?thesis proof(cases cstate rule: prod_cases4)
case (fields c β ve b)
show ?thesis using Discr Inr fields state proof(cases c, auto simp add:HOL.Let_def simp del:evalV_a.simps)
txt ‹Case App›
fix l d ds f
assume arg: "Discr (Inr (App l d ds, β, ve, b)) ∈ arg_poss p"
and f: "f ∈ \<aA> d β ve"
hence c: "App l d ds ∈ calls p"
and d: "d ∈ vals p"
and ds: "set ds ⊆ vals p"
and beta: "β ∈ maps_over (labels p) UNIV"
and ve: "ve ∈ smaps_over (vars p × UNIV) (proc_poss p)"
by (auto simp add: arg_poss_def cstate_poss_def call_list_lengths_def dest: app1 app2)
have len: "length ds ∈ call_list_lengths p"
by (auto intro: rev_image_eqI[OF c] simp add: call_list_lengths_def)
have "f ∈ proc_poss p"
using f d ve beta by (rule evalV_possible)
moreover
have "map (λv. \<aA> v β ve) ds ∈ NList (Pow (proc_poss p)) (call_list_lengths p)"
using ds len
unfolding NList_def by (auto simp add:nList_def intro!: evalV_possible[OF _ _ ve beta])
ultimately
have "(f, map (λv. \<aA> v β ve) ds, ve, \<anb> b l) ∈ fstate_poss p" (is "?fstate ∈ _")
using ve
unfolding fstate_poss_def by simp
thus "Discr (Inl ?fstate) ∈ arg_poss p"
unfolding arg_poss_def by auto
next
txt ‹Case Let›
fix l binds c'
assume arg: "Discr (Inr (Let l binds c', β, ve, b)) ∈ arg_poss p"
hence l: "l ∈ labels p"
and c': "c' ∈ calls p"
and vars: "fst ` set binds ⊆ vars p"
and ls: "snd ` set binds ⊆ lambdas p"
and beta: "β ∈ maps_over (labels p) UNIV"
and ve: "ve ∈ smaps_over (vars p × UNIV) (proc_poss p)"
by (auto simp add: arg_poss_def cstate_poss_def call_list_lengths_def
dest:let1 let2 let3 let4)
have beta': "β(l ↦ \<anb> b l) ∈ maps_over (labels p) UNIV" (is "?β' ∈ _")
by (auto intro: maps_over_upd[OF beta l])
moreover
have "ve ∪. ⋃.map (λ(v, lam). { (v, \<anb> b l) := \<aA> (L lam) (β(l ↦ \<anb> b l)) ve }.)
binds
∈ smaps_over (vars p × UNIV) (proc_poss p)" (is "?ve' ∈ _")
using vars ls beta'
by (auto intro!: smaps_over_un[OF ve] smaps_over_Union)
(auto intro!:smaps_over_singleton simp add: proc_poss_def)
ultimately
have "(c', ?β', ?ve', \<anb> b l) ∈ cstate_poss p" (is "?cstate ∈ _")
using c' unfolding cstate_poss_def by simp
thus "Discr (Inr ?cstate) ∈ arg_poss p"
unfolding arg_poss_def by auto
qed
qed
qed
qed
qed
text ‹
This result is now lifted to the powerset of ‹abs_R›.
›
lemma arg_space_complete_ps: "states ⊆ arg_poss p ⟹ (\<^ps>abs_R)⋅states ⊆ arg_poss p"
using arg_space_complete unfolding powerset_lift_def by auto
text ‹
We are not so much interested in the finiteness of the set of possible arguments but rather of the the set of occurring arguments, when we start with the initial argument. But as this is of course a subset of the set of possible arguments, this is not hard to show.
›
lemma UN_iterate_less:
assumes start: "x ∈ S"
and step: "⋀y. y⊆S ⟹ (f⋅y) ⊆ S"
shows "(⋃i. iterate i⋅f⋅{x}) ⊆ S"
proof- {
fix i
have "iterate i⋅f⋅{x} ⊆ S"
proof(induct i)
case 0 show ?case using ‹x ∈ S› by simp next
case (Suc i) thus ?case using step[of "iterate i⋅f⋅{x}"] by simp
qed
} thus ?thesis by auto
qed
lemma args_finite: "finite (⋃i. iterate i⋅(\<^ps>abs_R)⋅{initial_r p})" (is "finite ?S")
proof (rule finite_subset[OF _finite_arg_space])
have [simp]:"p ∈ lambdas p" by (cases p, simp)
show "?S ⊆ arg_poss p"
unfolding initial_r_def
by (rule UN_iterate_less[OF _ arg_space_complete_ps])
(auto simp add:arg_poss_def fstate_poss_def proc_poss_def call_list_lengths_def NList_def nList_def
intro!: imageI)
qed
subsection ‹A decomposition›
text ‹
The functions ‹abs_g› and ‹abs_R› are derived from ‹\<aF>› and ‹\<aC>›. This connection has yet to expressed explicitly.
›
lemma Un_commute_helper:"(a ∪ b) ∪ (c ∪ d) = (a ∪ c) ∪ (b ∪ d)"
by auto
lemma a_evalF_decomp:
"\<aF> = fst (sum_to_tup⋅(fix⋅(Λ f x. (⋃y∈abs_R⋅x. f⋅y) ∪ abs_g⋅x)))"
apply (subst a_evalF_def)
apply (subst fix_transform_pair_sum)
apply (rule arg_cong [of _ _ "λx. fst (sum_to_tup⋅(fix⋅x))"])
apply (simp)
apply (simp only: discr_app undiscr_Discr)
apply (rule cfun_eqI, rule cfun_eqI, simp)
apply (case_tac xa, rename_tac a, case_tac a, simp)
apply (case_tac aa rule:a_fstate_case, simp_all add: Un_commute_helper)
apply (case_tac b rule:prod_cases4)
apply (case_tac aa)
apply (simp_all add:HOL.Let_def)
done
subsection ‹The iterative equation›
text ‹
Because of the special form of ‹\<aF>› (and thus ‹\<aPR>›) derived in the previous lemma, we can apply our generic results from @{theory "Shivers-CFA.Computability"} and express the abstract semantics as the image of a finite set under a computable function.
›
lemma a_evalF_iterative:
"\<aF>⋅(Discr x) = \<^ps>abs_g⋅(⋃i. iterate i⋅(\<^ps>abs_R)⋅{Discr (Inl x)})"
by (simp del:abs_R.simps abs_g.simps add: theorem12 Un_commute a_evalF_decomp)
lemma a_evalCPS_interative:
"\<aPR> prog = \<^ps>abs_g⋅(⋃i. iterate i⋅(\<^ps>abs_R)⋅{initial_r prog})"
unfolding evalCPS_a_def and initial_r_def
by(subst a_evalF_iterative, simp del:abs_R.simps abs_g.simps evalV_a.simps)
end