Re: [isabelle] interpreters and continuations
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
an inductively defined relation. However, the above functional variation
is nicer because one can use monads to avoid the explicit treatment
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
I'm realizing that it has a significant learning curve and is quite
Of course, this problem goes away with a small-step semantics or
machine because the continuation can be concretely represented by its
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
interpLang :: "lang list => nat => step"
"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 #
I hope this example works in the latest Isabelle. Everything here
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-
interpreter for a significant language, but I think it ought to be
You should also be able to develop a (partial) big-step semantics
used this kind of approach to define something.
I don't know how this compares to just using HOLCF.
This archive was generated by a fusion of
Pipermail (Mailman edition) and