Re: [isabelle] interpreters and continuations



Hi Thomas,

I started out very much along the lines you suggest, using
a counter to force the interpreter to terminate. This works
quite well in dealing with the partiality of the interpreter.

fun eval :: "nat \<Rightarrow> expr \<Rightarrow> expr result" where
  "eval 0 e = TimeOut"
| "eval (Suc n) (Const c) = Result (Const c)"
| "eval (Suc n) (Y T1 T2) = Result (Y T1 T2)"
| "eval (Suc n) (Lam x T e) = Result (Lam x T e)"
| "eval (Suc n) (App e\<^isub>1 e\<^isub>2) =
    (v\<^isub>1 := eval n e\<^isub>1; v\<^isub>2 := eval n e\<^isub>2;
     case v\<^isub>1 of
       Lam x T e \<Rightarrow> eval n ([x\<rightarrow>v\<^isub>2]e)
     | Y T\<^isub>1 T\<^isub>2 \<Rightarrow>
        (let x = Suc (max_list (FV_list v\<^isub>2)) in
eval n (App v\<^isub>2 (\<lambda> x:T\<^isub>1. App (App (Y T\<^isub>1 T\<^isub>2) v\<^isub>2) (Var x))))
     | Const c \<Rightarrow> \<delta> c v\<^isub>2
     | _ \<Rightarrow> Wrong)"

This counter trick can also be applied to a big-step semantics expressed as
an inductively defined relation. However, the above functional variation
is nicer because one can use monads to avoid the explicit treatment of errors
and timeouts.

However, when I got to the point of adding first-class continuations
to the language being interpreted, I ran into a different problem.
I needed to add a new constructor "Cont" to the expr datatype
that stores a HOL function, but this isn't allowed in HOL.

datatype expr =  Var name | Const const
  | Lam name ty expr | App expr expr | Y ty ty
  | Cont "expr => expr result"  (* problem! *)

This is allowed in HOLCF, though after spending a couple hours with HOLCF I'm realizing that it has a significant learning curve and is quite rough around
the edges.

Of course, this problem goes away with a small-step semantics or abstract
machine because the continuation can be concretely represented by its
own datatype.

Cheers,
Jeremy


On Mar 4, 2009, at 11:34 PM, Thomas Sewell wrote:

Let me point out that you don't necessarily need to move
to a partial logic like HOLCF to deal with a partial function.
You just need to introduce partiality explicitly.

For instance, consider a simple recursive interpreter
which may fail to terminate if the program it is interpreting
fails to terminate. Specifying the big-step semantics is a
problem in Isabelle/HOL because there may not be any. But
specifying a small-step semantics is easy. We model the outcome
as a trace (nat => step) of steps taken.

datatype lang = Emit string | Loop "lang list"

datatype step = Emitted string | Looped | Terminated

function
 interpLang :: "lang list => nat => step"
where
 "interpLang [] n = Terminated"
| "interpLang (Emit string # xs) 0 = Emitted string"
| "interpLang (Loop xs # ys) 0 = Looped"
| "interpLang (Emit string # xs) (Suc n) = interpLang xs n"
| "interpLang (Loop xs # ys) (Suc n) = interpLang (xs @ Loop xs # ys) n"
 apply simp_all
 apply pat_completeness
 done

termination interpLang
 by lexicographic_order

I hope this example works in the latest Isabelle. Everything here is perfectly
well-defined. We can look at the trace the interpreter generates with:

value "map (interpLang [Loop [Emit ''foo'']]) [0 ..< 10]"

Of course, we're a long way from an elegantly stated continuation- passing interpreter for a significant language, but I think it ought to be possible. You should also be able to develop a (partial) big-step semantics once you've
used this kind of approach to define something.

I don't know how this compares to just using HOLCF.

Yours,
   Thomas.






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.