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
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 # ys) n"
I hope this example works in the latest Isabelle. Everything here is
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
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