*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] interpreters and continuations*From*: Jeremy Siek <jeremy.siek at gmail.com>*Date*: Thu, 5 Mar 2009 12:23:18 -0700*In-reply-to*: <49AF7271.4060401@nicta.com.au>*References*: <49AF7271.4060401@nicta.com.au>

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

| Const c \<Rightarrow> \<delta> c v\<^isub>2 | _ \<Rightarrow> Wrong)"

an inductively defined relation. However, the above functional variation

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! *)

the edges.

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_orderI hope this example works in the latest Isabelle. Everything hereis perfectlywell-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-passinginterpreter for a significant language, but I think it ought to bepossible.You should also be able to develop a (partial) big-step semanticsonce you'veused this kind of approach to define something. I don't know how this compares to just using HOLCF. Yours, Thomas.

**References**:**Re: [isabelle] interpreters and continuations***From:*Thomas Sewell

- Previous by Date: [isabelle] SFM-09:WS -- school on formal methods for web services (last call)
- Next by Date: [isabelle] 2nd CFP: LSFA2009
- Previous by Thread: Re: [isabelle] interpreters and continuations
- Next by Thread: [isabelle] Deadline Extension for TPHOLs 2009
- Cl-isabelle-users March 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list