Re: [isabelle] interpreters and continuations



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.