# 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.