Theory Backtracking

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

theory Backtracking
imports
  HOLCF
  Nats
  WorkerWrapperNew
begin

(*>*)
section‹Backtracking using lazy lists and continuations›

text‹
\label{sec:ww-backtracking}

To illustrate the utility of worker/wrapper fusion to programming
language semantics, we consider here the first-order part of a
higher-order backtracking language by \<^citet>‹"DBLP:conf/icfp/WandV04"›;
see also \<^citet>‹"DBLP:journals/ngc/DanvyGR01"›. We refer the reader to
these papers for a broader motivation for these languages.

As syntax is typically considered to be inductively generated, with
each syntactic object taken to be finite and completely defined, we
define the syntax for our language using a HOL datatype:

›

datatype expr = const nat | add expr expr | disj expr expr | fail
(*<*)

lemma case_expr_cont[cont2cont]:
  assumes f1: "⋀y. cont (λx. f1 x y)"
  assumes f2: "⋀y z. cont (λx. f2 x y z)"
  assumes f3: "⋀y z. cont (λx. f3 x y z)"
  assumes f4: "cont (λx. f4 x)"
  shows "cont (λx. case_expr (f1 x) (f2 x) (f3 x) (f4 x) expr)"
  using assms by (cases expr) simp_all

(* Presumably obsolete in the HG version, not so in Isabelle2011. *)

fun
  expr_encode :: "expr ⇒ nat"
where
  "expr_encode (const n) = prod_encode (0, n)"
| "expr_encode (add e1 e2) = prod_encode (1, (prod_encode (expr_encode e1, expr_encode e2)))"
| "expr_encode (disj e1 e2) = prod_encode (2, (prod_encode (expr_encode e1, expr_encode e2)))"
| "expr_encode fail = prod_encode (3, 0)"

lemma expr_encode_inj:
  "expr_encode x = expr_encode y ⟹ x = y"
  by (induct x arbitrary: y) ((case_tac y, auto dest!: inj_onD[OF inj_prod_encode, where A=UNIV])[1])+

instance expr :: countable
  by (rule countable_classI[OF expr_encode_inj])

(*>*)
text‹

The language consists of constants, an addition function, a
disjunctive choice between expressions, and failure. We give it a
direct semantics using the monad of lazy lists of natural numbers,
with the goal of deriving an an extensionally-equivalent evaluator
that uses double-barrelled continuations.

Our theory of lazy lists is entirely standard.

›

default_sort predomain

domain 'a llist =
    lnil
  | lcons (lazy "'a") (lazy "'a llist")

text‹

By relaxing the default sort of type variables to ‹predomain›,
our polymorphic definitions can be used at concrete types that do not
contain @{term "⊥"}. These include those constructed from HOL types
using the discrete ordering type constructor @{typ "'a discr"}, and in
particular our interpretation @{typ "nat discr"} of the natural
numbers.

The following standard list functions underpin the monadic
infrastructure:

›

fixrec lappend :: "'a llist → 'a llist → 'a llist" where
  "lappend⋅lnil⋅ys = ys"
| "lappend⋅(lcons⋅x⋅xs)⋅ys = lcons⋅x⋅(lappend⋅xs⋅ys)"

fixrec lconcat :: "'a llist llist → 'a llist" where
  "lconcat⋅lnil = lnil"
| "lconcat⋅(lcons⋅x⋅xs) = lappend⋅x⋅(lconcat⋅xs)"

fixrec lmap :: "('a → 'b) → 'a llist → 'b llist" where
  "lmap⋅f⋅lnil = lnil"
| "lmap⋅f⋅(lcons⋅x⋅xs) = lcons⋅(f⋅x)⋅(lmap⋅f⋅xs)"
(*<*)

lemma lappend_strict'[simp]: "lappend⋅⊥ = (Λ a. ⊥)"
  by fixrec_simp

lemma lconcat_strict[simp]: "lconcat⋅⊥ = ⊥"
  by fixrec_simp

lemma lmap_strict[simp]: "lmap⋅f⋅⊥ = ⊥"
  by fixrec_simp

(*>*)
text‹

We define the lazy list monad ‹S› in the traditional fashion:

›

type_synonym S = "nat discr llist"

definition returnS :: "nat discr → S" where
  "returnS = (Λ x. lcons⋅x⋅lnil)"

definition bindS :: "S → (nat discr → S) → S" where
  "bindS = (Λ x g. lconcat⋅(lmap⋅g⋅x))"

text‹

Unfortunately the lack of higher-order polymorphism in HOL prevents us
from providing the general typing one would expect a monad to have in
Haskell.

The evaluator uses the following extra constants:

›

definition addS :: "S → S → S" where
  "addS ≡ (Λ x y. bindS⋅x⋅(Λ xv. bindS⋅y⋅(Λ yv. returnS⋅(xv + yv))))"

definition disjS :: "S → S → S" where
  "disjS ≡ lappend"

definition failS :: "S" where
  "failS ≡ lnil"

text‹

We interpret our language using these combinators in the obvious
way. The only complication is that, even though our evaluator is
primitive recursive, we must explicitly use the fixed point operator
as the worker/wrapper technique requires us to talk about the body of
the recursive definition.

›

definition
  evalS_body :: "(expr discr → nat discr llist)
              → (expr discr → nat discr llist)"
where
  "evalS_body ≡ Λ r e. case undiscr e of
     const n ⇒ returnS⋅(Discr n)
   | add e1 e2 ⇒ addS⋅(r⋅(Discr e1))⋅(r⋅(Discr e2))
   | disj e1 e2 ⇒ disjS⋅(r⋅(Discr e1))⋅(r⋅(Discr e2))
   | fail ⇒ failS"

abbreviation evalS :: "expr discr → nat discr llist" where
  "evalS ≡ fix⋅evalS_body"

text‹

We aim to transform this evaluator into one using double-barrelled
continuations; one will serve as a "success" context, taking a natural
number into "the rest of the computation", and the other outright
failure.

In general we could work with an arbitrary observation type ala
\<^citet>‹"DBLP:conf/icalp/Reynolds74"›, but for convenience we use the
clearly adequate concrete type @{typ "nat discr llist"}.

›

type_synonym Obs = "nat discr llist"
type_synonym Failure = "Obs"
type_synonym Success = "nat discr → Failure → Obs"
type_synonym K = "Success → Failure → Obs"

text‹

To ease our development we adopt what
\<^citet>‹‹\S5› in "DBLP:conf/icfp/WandV04"› call a "failure computation"
instead of a failure continuation, which would have the type @{typ
"unit → Obs"}.

The monad over the continuation type @{typ "K"} is as follows:

›

definition returnK :: "nat discr → K" where
  "returnK ≡ (Λ x. Λ s f. s⋅x⋅f)"

definition bindK :: "K → (nat discr → K) → K" where
  "bindK ≡ Λ x g. Λ s f. x⋅(Λ xv f'. g⋅xv⋅s⋅f')⋅f"

text‹

Our extra constants are defined as follows:

›

definition addK :: "K → K → K" where
  "addK ≡ (Λ x y. bindK⋅x⋅(Λ xv. bindK⋅y⋅(Λ yv. returnK⋅(xv + yv))))"

definition disjK :: "K → K → K" where
  "disjK ≡ (Λ g h. Λ s f. g⋅s⋅(h⋅s⋅f))"

definition failK :: "K" where
  "failK ≡ Λ s f. f"

text‹

The continuation semantics is again straightforward:

›

definition
  evalK_body :: "(expr discr → K) → (expr discr → K)"
where
  "evalK_body ≡ Λ r e. case undiscr e of
     const n ⇒ returnK⋅(Discr n)
   | add e1 e2 ⇒ addK⋅(r⋅(Discr e1))⋅(r⋅(Discr e2))
   | disj e1 e2 ⇒ disjK⋅(r⋅(Discr e1))⋅(r⋅(Discr e2))
   | fail ⇒ failK"

abbreviation evalK :: "expr discr → K" where
  "evalK ≡ fix⋅evalK_body"

text‹

We now set up a worker/wrapper relation between these two semantics.

The kernel of @{term "unwrap"} is the following function that converts
a lazy list into an equivalent continuation representation.

›

fixrec SK :: "S → K" where
  "SK⋅lnil = failK"
| "SK⋅(lcons⋅x⋅xs) = (Λ s f. s⋅x⋅(SK⋅xs⋅s⋅f))"

definition
  unwrap :: "(expr discr → nat discr llist) → (expr discr → K)"
where
  "unwrap ≡ Λ r e. SK⋅(r⋅e)"
(*<*)

lemma SK_strict[simp]: "SK⋅⊥ = ⊥"
  by fixrec_simp

lemma unwrap_strict[simp]: "unwrap⋅⊥ = ⊥"
  unfolding unwrap_def by simp

(*>*)
text‹

Symmetrically @{term "wrap"} converts an evaluator using continuations
into one generating lazy lists by passing it the right continuations.

›

definition KS :: "K → S" where
  "KS ≡ (Λ k. k⋅lcons⋅lnil)"

definition wrap :: "(expr discr → K) → (expr discr → nat discr llist)" where
  "wrap ≡ Λ r e. KS⋅(r⋅e)"
(*<*)

lemma KS_strict[simp]: "KS⋅⊥ = ⊥"
  unfolding KS_def by simp

lemma wrap_strict[simp]: "wrap⋅⊥ = ⊥"
  unfolding wrap_def by simp

(*>*)
text‹

The worker/wrapper condition follows directly from these definitions.

›

lemma KS_SK_id:
  "KS⋅(SK⋅xs) = xs"
  by (induct xs) (simp_all add: KS_def failK_def)

lemma wrap_unwrap_id:
  "wrap oo unwrap = ID"
  unfolding wrap_def unwrap_def
  by (simp add: KS_SK_id cfun_eq_iff)

text‹

The worker/wrapper transformation is only non-trivial if @{term
"wrap"} and @{term "unwrap"} do not witness an isomorphism. In this
case we can show that we do not even have a Galois connection.

›

lemma cfun_not_below:
  "f⋅x \<notsqsubseteq> g⋅x ⟹ f \<notsqsubseteq> g"
  by (auto simp: cfun_below_iff)

lemma unwrap_wrap_not_under_id:
  "unwrap oo wrap \<notsqsubseteq> ID"
proof -
  let ?witness = "Λ e. (Λ s f. lnil :: K)"
  have "(unwrap oo wrap)⋅?witness⋅(Discr fail)⋅⊥⋅(lcons⋅0⋅lnil)
       \<notsqsubseteq> ?witness⋅(Discr fail)⋅⊥⋅(lcons⋅0⋅lnil)"
    by (simp add: failK_def wrap_def unwrap_def KS_def)
  hence "(unwrap oo wrap)⋅?witness \<notsqsubseteq> ?witness"
    by (fastforce intro!: cfun_not_below)
  thus ?thesis by (simp add: cfun_not_below)
qed

text‹

We now apply \texttt{worker\_wrapper\_id}:

›

definition eval_work :: "expr discr → K" where
  "eval_work ≡ fix⋅(unwrap oo evalS_body oo wrap)"

definition eval_ww :: "expr discr → nat discr llist" where
  "eval_ww ≡ wrap⋅eval_work"

lemma "evalS = eval_ww"
  unfolding eval_ww_def eval_work_def
  using worker_wrapper_id[OF wrap_unwrap_id]
  by simp

text‹

We now show how the monadic operations correspond by showing that
@{term "SK"} witnesses a \emph{monad morphism}
\<^citep>‹‹\S6› in "wadler92:_comprehending_monads"›. As required by
\<^citet>‹‹Definition~2.1› in "DBLP:journals/ngc/DanvyGR01"›, the mapping needs
to hold for our specific operations in addition to the common monadic
scaffolding.

›

lemma SK_returnS_returnK:
  "SK⋅(returnS⋅x) = returnK⋅x"
  by (simp add: returnS_def returnK_def failK_def)

lemma SK_lappend_distrib:
 "SK⋅(lappend⋅xs⋅ys)⋅s⋅f = SK⋅xs⋅s⋅(SK⋅ys⋅s⋅f)"
  by (induct xs) (simp_all add: failK_def)

lemma SK_bindS_bindK:
  "SK⋅(bindS⋅x⋅g) = bindK⋅(SK⋅x)⋅(SK oo g)"
  by (induct x)
     (simp_all add: cfun_eq_iff
                    bindS_def bindK_def failK_def
                    SK_lappend_distrib)

lemma SK_addS_distrib:
  "SK⋅(addS⋅x⋅y) = addK⋅(SK⋅x)⋅(SK⋅y)"
  by (clarsimp simp: cfcomp1
                     addS_def addK_def failK_def
                     SK_bindS_bindK SK_returnS_returnK)

lemma SK_disjS_disjK:
 "SK⋅(disjS⋅xs⋅ys) = disjK⋅(SK⋅xs)⋅(SK⋅ys)"
  by (simp add: cfun_eq_iff disjS_def disjK_def SK_lappend_distrib)

lemma SK_failS_failK:
  "SK⋅failS = failK"
  unfolding failS_def by simp

text‹

These lemmas directly establish the precondition for our all-in-one
worker/wrapper and fusion rule:

›

lemma evalS_body_evalK_body:
  "unwrap oo evalS_body oo wrap = evalK_body oo unwrap oo wrap"
proof(intro cfun_eqI)
  fix r e' s f
  obtain e :: "expr"
    where ee': "e' = Discr e" by (cases e')
  have "(unwrap oo evalS_body oo wrap)⋅r⋅(Discr e)⋅s⋅f
      = (evalK_body oo unwrap oo wrap)⋅r⋅(Discr e)⋅s⋅f"
    by (cases e)
       (simp_all add: evalS_body_def evalK_body_def unwrap_def
                      SK_returnS_returnK SK_addS_distrib
                      SK_disjS_disjK SK_failS_failK)
  with ee' show "(unwrap oo evalS_body oo wrap)⋅r⋅e'⋅s⋅f
                = (evalK_body oo unwrap oo wrap)⋅r⋅e'⋅s⋅f"
    by simp
qed

theorem evalS_evalK:
  "evalS = wrap⋅evalK"
  using worker_wrapper_fusion_new[OF wrap_unwrap_id unwrap_strict]
        evalS_body_evalK_body
  by simp

text‹

This proof can be considered an instance of the approach of
\<^citet>‹"DBLP:journals/jfp/HuttonJG10"›, which uses the worker/wrapper
machinery to relate two algebras.

This result could be obtained by a structural induction over the
syntax of the language. However our goal here is to show how such a
transformation can be achieved by purely equational means; this has
the advantange that our proof can be locally extended, e.g. to the
full language of \<^citet>‹"DBLP:journals/ngc/DanvyGR01"› simply by proving
extra equations. In contrast the higher-order language of
\<^citet>‹"DBLP:conf/icfp/WandV04"› is beyond the reach of this approach.

›
(*<*)

end
(*>*)