Theory Accumulator
theory Accumulator
imports
HOLCF
LList
WorkerWrapperNew
begin
section‹Naive reverse becomes accumulator-reverse.›
text‹\label{sec:accum}›
subsection‹Hughes lists, naive reverse, worker-wrapper optimisation.›
text‹The ``Hughes'' list type.›
type_synonym 'a H = "'a llist → 'a llist"
definition
list2H :: "'a llist → 'a H" where
"list2H ≡ lappend"
lemma acc_c2a_strict[simp]: "list2H⋅⊥ = ⊥"
by (rule cfun_eqI, simp add: list2H_def)
definition
H2list :: "'a H → 'a llist" where
"H2list ≡ Λ f . f⋅lnil"
text‹The paper only claims the homomorphism holds for finite lists,
but in fact it holds for all lazy lists in HOLCF. They are trying to
dodge an explicit appeal to the equation @{thm "inst_cfun_pcpo"},
which does not hold in Haskell.›
lemma H_llist_hom_append: "list2H⋅(xs :++ ys) = list2H⋅xs oo list2H⋅ys" (is "?lhs = ?rhs")
proof(rule cfun_eqI)
fix zs
have "?lhs⋅zs = (xs :++ ys) :++ zs" by (simp add: list2H_def)
also have "… = xs :++ (ys :++ zs)" by (rule lappend_assoc)
also have "… = list2H⋅xs⋅(ys :++ zs)" by (simp add: list2H_def)
also have "… = list2H⋅xs⋅(list2H⋅ys⋅zs)" by (simp add: list2H_def)
also have "… = (list2H⋅xs oo list2H⋅ys)⋅zs" by simp
finally show "?lhs⋅zs = (list2H⋅xs oo list2H⋅ys)⋅zs" .
qed
lemma H_llist_hom_id: "list2H⋅lnil = ID" by (simp add: list2H_def)
lemma H2list_list2H_inv: "H2list oo list2H = ID"
by (rule cfun_eqI, simp add: H2list_def list2H_def)
text‹\<^citet>‹‹\S4.2› in "GillHutton:2009"› define the naive reverse
function as follows.›
fixrec lrev :: "'a llist → 'a llist"
where
"lrev⋅lnil = lnil"
| "lrev⋅(x :@ xs) = lrev⋅xs :++ (x :@ lnil)"
text‹Note ``body'' is the generator of @{term "lrev_def"}.›
lemma lrev_strict[simp]: "lrev⋅⊥ = ⊥"
by fixrec_simp
fixrec lrev_body :: "('a llist → 'a llist) → 'a llist → 'a llist"
where
"lrev_body⋅r⋅lnil = lnil"
| "lrev_body⋅r⋅(x :@ xs) = r⋅xs :++ (x :@ lnil)"
lemma lrev_body_strict[simp]: "lrev_body⋅r⋅⊥ = ⊥"
by fixrec_simp
text‹This is trivial but syntactically a bit touchy. Would be nicer
to define @{term "lrev_body"} as the generator of the fixpoint
definition of @{term "lrev"} directly.›
lemma lrev_lrev_body_eq: "lrev = fix⋅lrev_body"
by (rule cfun_eqI, subst lrev_def, subst lrev_body.unfold, simp)
text‹Wrap / unwrap functions.›
definition
unwrapH :: "('a llist → 'a llist) → 'a llist → 'a H" where
"unwrapH ≡ Λ f xs . list2H⋅(f⋅xs)"
lemma unwrapH_strict[simp]: "unwrapH⋅⊥ = ⊥"
unfolding unwrapH_def by (rule cfun_eqI, simp)
definition
wrapH :: "('a llist → 'a H) → 'a llist → 'a llist" where
"wrapH ≡ Λ f xs . H2list⋅(f⋅xs)"
lemma wrapH_unwrapH_id: "wrapH oo unwrapH = ID" (is "?lhs = ?rhs")
proof(rule cfun_eqI)+
fix f xs
have "?lhs⋅f⋅xs = H2list⋅(list2H⋅(f⋅xs))" by (simp add: wrapH_def unwrapH_def)
also have "… = (H2list oo list2H)⋅(f⋅xs)" by simp
also have "… = ID⋅(f⋅xs)" by (simp only: H2list_list2H_inv)
also have "… = ?rhs⋅f⋅xs" by simp
finally show "?lhs⋅f⋅xs = ?rhs⋅f⋅xs" .
qed
subsection‹Gill/Hutton-style worker/wrapper.›
definition
lrev_work :: "'a llist → 'a H" where
"lrev_work ≡ fix⋅(unwrapH oo lrev_body oo wrapH)"
definition
lrev_wrap :: "'a llist → 'a llist" where
"lrev_wrap ≡ wrapH⋅lrev_work"
lemma lrev_lrev_ww_eq: "lrev = lrev_wrap"
using worker_wrapper_id[OF wrapH_unwrapH_id lrev_lrev_body_eq]
by (simp add: lrev_wrap_def lrev_work_def)
subsection‹Optimise worker/wrapper.›
text‹Intermediate worker.›
fixrec lrev_body1 :: "('a llist → 'a H) → 'a llist → 'a H"
where
"lrev_body1⋅r⋅lnil = list2H⋅lnil"
| "lrev_body1⋅r⋅(x :@ xs) = list2H⋅(wrapH⋅r⋅xs :++ (x :@ lnil))"
definition
lrev_work1 :: "'a llist → 'a H" where
"lrev_work1 ≡ fix⋅lrev_body1"
lemma lrev_body_lrev_body1_eq: "lrev_body1 = unwrapH oo lrev_body oo wrapH"
apply (rule cfun_eqI)+
apply (subst lrev_body.unfold)
apply (subst lrev_body1.unfold)
apply (case_tac xa)
apply (simp_all add: list2H_def wrapH_def unwrapH_def)
done
lemma lrev_work1_lrev_work_eq: "lrev_work1 = lrev_work"
by (unfold lrev_work_def lrev_work1_def,
rule cfun_arg_cong[OF lrev_body_lrev_body1_eq])
text‹Now use the homomorphism.›
fixrec lrev_body2 :: "('a llist → 'a H) → 'a llist → 'a H"
where
"lrev_body2⋅r⋅lnil = ID"
| "lrev_body2⋅r⋅(x :@ xs) = list2H⋅(wrapH⋅r⋅xs) oo list2H⋅(x :@ lnil)"
lemma lrev_body2_strict[simp]: "lrev_body2⋅r⋅⊥ = ⊥"
by fixrec_simp
definition
lrev_work2 :: "'a llist → 'a H" where
"lrev_work2 ≡ fix⋅lrev_body2"
lemma lrev_work2_strict[simp]: "lrev_work2⋅⊥ = ⊥"
unfolding lrev_work2_def
by (subst fix_eq) simp
lemma lrev_body2_lrev_body1_eq: "lrev_body2 = lrev_body1"
by ((rule cfun_eqI)+
, (subst lrev_body1.unfold, subst lrev_body2.unfold)
, (simp add: H_llist_hom_append[symmetric] H_llist_hom_id))
lemma lrev_work2_lrev_work1_eq: "lrev_work2 = lrev_work1"
by (unfold lrev_work2_def lrev_work1_def
, rule cfun_arg_cong[OF lrev_body2_lrev_body1_eq])
text ‹Simplify.›
fixrec lrev_body3 :: "('a llist → 'a H) → 'a llist → 'a H"
where
"lrev_body3⋅r⋅lnil = ID"
| "lrev_body3⋅r⋅(x :@ xs) = r⋅xs oo list2H⋅(x :@ lnil)"
lemma lrev_body3_strict[simp]: "lrev_body3⋅r⋅⊥ = ⊥"
by fixrec_simp
definition
lrev_work3 :: "'a llist → 'a H" where
"lrev_work3 ≡ fix⋅lrev_body3"
lemma lrev_wwfusion: "list2H⋅((wrapH⋅lrev_work2)⋅xs) = lrev_work2⋅xs"
proof -
{
have "list2H oo wrapH⋅lrev_work2 = unwrapH⋅(wrapH⋅lrev_work2)"
by (rule cfun_eqI, simp add: unwrapH_def)
also have "… = (unwrapH oo wrapH)⋅lrev_work2" by simp
also have "… = lrev_work2"
apply -
apply (rule worker_wrapper_fusion[OF wrapH_unwrapH_id, where body="lrev_body"])
apply (auto iff: lrev_body2_lrev_body1_eq lrev_body_lrev_body1_eq lrev_work2_def lrev_work1_def)
done
finally have "list2H oo wrapH⋅lrev_work2 = lrev_work2" .
}
thus ?thesis using cfun_eq_iff[where f="list2H oo wrapH⋅lrev_work2" and g="lrev_work2"] by auto
qed
text‹If we use this result directly, we only get a partially-correct
program transformation, see \<^citet>‹"Tullsen:PhDThesis"› for details.›
lemma "lrev_work3 ⊑ lrev_work2"
unfolding lrev_work3_def
proof(rule fix_least)
{
fix xs have "lrev_body3⋅lrev_work2⋅xs = lrev_work2⋅xs"
proof(cases xs)
case bottom thus ?thesis by simp
next
case lnil thus ?thesis
unfolding lrev_work2_def
by (subst fix_eq[where F="lrev_body2"], simp)
next
case (lcons y ys)
hence "lrev_body3⋅lrev_work2⋅xs = lrev_work2⋅ys oo list2H⋅(y :@ lnil)" by simp
also have "… = list2H⋅((wrapH⋅lrev_work2)⋅ys) oo list2H⋅(y :@ lnil)"
using lrev_wwfusion[where xs=ys] by simp
also from lcons have "… = lrev_body2⋅lrev_work2⋅xs" by simp
also have "… = lrev_work2⋅xs"
unfolding lrev_work2_def by (simp only: fix_eq[symmetric])
finally show ?thesis by simp
qed
}
thus "lrev_body3⋅lrev_work2 = lrev_work2" by (rule cfun_eqI)
qed
text‹We can't show the reverse inclusion in the same way as the
fusion law doesn't hold for the optimised definition. (Intuitively we
haven't established that it is equal to the original @{term "lrev"}
definition.) We could show termination of the optimised definition
though, as it operates on finite lists. Alternatively we can use
induction (over the list argument) to show total equivalence.
The following lemma shows that the fusion Gill/Hutton want to do is
completely sound in this context, by appealing to the lazy list
induction principle.›
lemma lrev_work3_lrev_work2_eq: "lrev_work3 = lrev_work2" (is "?lhs = ?rhs")
proof(rule cfun_eqI)
fix x
show "?lhs⋅x = ?rhs⋅x"
proof(induct x)
show "lrev_work3⋅⊥ = lrev_work2⋅⊥"
apply (unfold lrev_work3_def lrev_work2_def)
apply (subst fix_eq[where F="lrev_body2"])
apply (subst fix_eq[where F="lrev_body3"])
by (simp add: lrev_body3.unfold lrev_body2.unfold)
next
show "lrev_work3⋅lnil = lrev_work2⋅lnil"
apply (unfold lrev_work3_def lrev_work2_def)
apply (subst fix_eq[where F="lrev_body2"])
apply (subst fix_eq[where F="lrev_body3"])
by (simp add: lrev_body3.unfold lrev_body2.unfold)
next
fix a l assume "lrev_work3⋅l = lrev_work2⋅l"
thus "lrev_work3⋅(a :@ l) = lrev_work2⋅(a :@ l)"
apply (unfold lrev_work3_def lrev_work2_def)
apply (subst fix_eq[where F="lrev_body2"])
apply (subst fix_eq[where F="lrev_body3"])
apply (fold lrev_work3_def lrev_work2_def)
apply (simp add: lrev_body3.unfold lrev_body2.unfold lrev_wwfusion)
done
qed simp_all
qed
text‹Use the combined worker/wrapper-fusion rule. Note we get a weaker lemma.›
lemma lrev3_2_syntactic: "lrev_body3 oo (unwrapH oo wrapH) = lrev_body2"
apply (subst lrev_body2.unfold, subst lrev_body3.unfold)
apply (rule cfun_eqI)+
apply (case_tac xa)
apply (simp_all add: unwrapH_def)
done
lemma lrev_work3_lrev_work2_eq': "lrev = wrapH⋅lrev_work3"
proof -
from lrev_lrev_body_eq
have "lrev = fix⋅lrev_body" .
also from wrapH_unwrapH_id unwrapH_strict
have "… = wrapH⋅(fix⋅lrev_body3)"
by (rule worker_wrapper_fusion_new
, simp add: lrev3_2_syntactic lrev_body2_lrev_body1_eq lrev_body_lrev_body1_eq)
finally show ?thesis unfolding lrev_work3_def by simp
qed
text‹Final syntactic tidy-up.›
fixrec lrev_body_final :: "('a llist → 'a H) → 'a llist → 'a H"
where
"lrev_body_final⋅r⋅lnil⋅ys = ys"
| "lrev_body_final⋅r⋅(x :@ xs)⋅ys = r⋅xs⋅(x :@ ys)"
definition
lrev_work_final :: "'a llist → 'a H" where
"lrev_work_final ≡ fix⋅lrev_body_final"
definition
lrev_final :: "'a llist → 'a llist" where
"lrev_final ≡ Λ xs. lrev_work_final⋅xs⋅lnil"
lemma lrev_body_final_lrev_body3_eq': "lrev_body_final⋅r⋅xs = lrev_body3⋅r⋅xs"
apply (subst lrev_body_final.unfold)
apply (subst lrev_body3.unfold)
apply (cases xs)
apply (simp_all add: list2H_def ID_def cfun_eqI)
done
lemma lrev_body_final_lrev_body3_eq: "lrev_body_final = lrev_body3"
by (simp only: lrev_body_final_lrev_body3_eq' cfun_eqI)
lemma lrev_final_lrev_eq: "lrev = lrev_final" (is "?lhs = ?rhs")
proof -
have "?lhs = lrev_wrap" by (rule lrev_lrev_ww_eq)
also have "… = wrapH⋅lrev_work" by (simp only: lrev_wrap_def)
also have "… = wrapH⋅lrev_work1" by (simp only: lrev_work1_lrev_work_eq)
also have "… = wrapH⋅lrev_work2" by (simp only: lrev_work2_lrev_work1_eq)
also have "… = wrapH⋅lrev_work3" by (simp only: lrev_work3_lrev_work2_eq)
also have "… = wrapH⋅lrev_work_final" by (simp only: lrev_work3_def lrev_work_final_def lrev_body_final_lrev_body3_eq)
also have "… = lrev_final" by (simp add: lrev_final_def cfun_eqI H2list_def wrapH_def)
finally show ?thesis .
qed
end