Theory WorkerWrapperNew

(*<*)
(*
 * The worker/wrapper transformation, following Gill and Hutton.
 * (C)opyright 2009-2011, Peter Gammie, peteg42 at gmail.com.
 * License: BSD
 *)

theory WorkerWrapperNew
imports
  HOLCF
  FixedPointTheorems
  WorkerWrapper
begin

(*>*)
section‹A totally-correct fusion rule›

text‹
\label{sec:ww-fixed}

We now show that a termination-preserving worker/wrapper fusion rule
can be obtained by requiring @{term "unwrap"} to be strict. (As we
observed earlier, @{term "wrap"} must always be strict due to the
assumption that ‹wrap oo unwrap = ID›.)

Our first result shows that a combined worker/wrapper transformation
and fusion rule is sound, using the assumptions of ‹worker_wrapper_id› and the ubiquitous ‹lfp_fusion› rule.

›

lemma worker_wrapper_fusion_new:
  fixes wrap :: "'b::pcpo → 'a::pcpo"
  fixes unwrap :: "'a → 'b"
  fixes body' :: "'b → 'b"
  assumes wrap_unwrap: "wrap oo unwrap = (ID :: 'a → 'a)"
  assumes unwrap_strict: "unwrap⋅⊥ = ⊥"
  assumes body_body': "unwrap oo body oo wrap = body' oo (unwrap oo wrap)"
  shows "fix⋅body = wrap⋅(fix⋅body')"
proof -
  from body_body'
  have "unwrap oo body oo (wrap oo unwrap) = (body' oo unwrap oo (wrap oo unwrap))"
    by (simp add: assoc_oo)
  with wrap_unwrap have "unwrap oo body = body' oo unwrap"
    by simp
  with unwrap_strict have "unwrap⋅(fix⋅body) = fix⋅body'"
    by (rule lfp_fusion)
  hence "(wrap oo unwrap)⋅(fix⋅body) = wrap⋅(fix⋅body')"
    by simp
  with wrap_unwrap show ?thesis by simp
qed

text‹

We can also show a more general result which allows fusion to be
optionally performed on a per-recursive-call basis using
\texttt{parallel\_fix\_ind}:

›

lemma worker_wrapper_fusion_new_general:
  fixes wrap :: "'b::pcpo → 'a::pcpo"
  fixes unwrap :: "'a → 'b"
  assumes wrap_unwrap: "wrap oo unwrap = (ID :: 'a → 'a)"
  assumes unwrap_strict: "unwrap⋅⊥ = ⊥"
  assumes body_body': "⋀r. (unwrap oo wrap)⋅r = r
                        ⟹ (unwrap oo body oo wrap)⋅r = body'⋅r"
  shows "fix⋅body = wrap⋅(fix⋅body')"
proof -
  let ?P = "λ(x, y). x = y ∧ unwrap⋅(wrap⋅x) = x"
  have "?P (fix⋅(unwrap oo body oo wrap), (fix⋅body'))"
  proof(induct rule: parallel_fix_ind)
    case 2 with retraction_strict unwrap_strict wrap_unwrap show "?P (⊥, ⊥)"
      by (bestsimp simp add: cfun_eq_iff)
    case (3 x y)
    hence xy: "x = y" and unwrap_wrap: "unwrap⋅(wrap⋅x) = x" by auto
    from body_body' xy unwrap_wrap
    have "(unwrap oo body oo wrap)⋅x = body'⋅y"
      by simp
    moreover
    from wrap_unwrap
    have "unwrap⋅(wrap⋅((unwrap oo body oo wrap)⋅x)) = (unwrap oo body oo wrap)⋅x"
      by (simp add: cfun_eq_iff)
    ultimately show ?case by simp
  qed simp
  thus ?thesis
    using worker_wrapper_id[OF wrap_unwrap refl] by simp
qed

text‹

This justifies the syntactically-oriented rules shown in
Figure~\ref{fig:wwc2}; note the scoping of the fusion rule.

Those familiar with the ``bananas'' work of \citet*{barbed-wire:1991}
will not be surprised that adding a strictness assumption justifies an
equational fusion rule.

\begin{figure}[tb]
 \begin{center}
  \fbox{\parbox{0.96\textwidth}{For a recursive definition @{haskell "comp =
      body"} of type @{haskell "A"} and a pair of functions @{haskell "wrap :: B \\to A"}
      and @{haskell "unwrap :: A \\to B"} where @{haskell "wrap \\circ unwrap = id_A"} and
      @{haskell "unwrap\\ \\bot = \\bot"}, define:

      \parbox{0.35\textwidth}{\begin{haskell}
        comp & = wrap\ work\\
        work & = unwrap\ (body[wrap\ work / comp])
      \end{haskell}}\hfill \textsf{(the worker/wrapper transformation)}

    In the scope of @{haskell "work"}, the following rewrite is admissable:

    \parbox{0.35\textwidth}{\begin{haskell}
        unwrap\ (wrap\ work) \Longrightarrow work
      \end{haskell}}\hfill \textsf{(worker/wrapper fusion)}}}%
 \end{center}%
\caption{The syntactic worker/wrapper transformation and fusion rule.}\label{fig:wwc2}
\end{figure}

›

(*<*)
end
(*>*)