Email Gateway (Aug 18 2022 at 13:06): Email Gateway (Aug 18 2022 at 13:06):From: Brian Huffman <brianh@cs.pdx.edu>
Certainly, using the HOLCF continuous function type should allow you
to define datatypes with continuations, just like you would define
them in Haskell or ML. The domain package currently allows you to use
indirect recursion with the continuous function space; for example,
you can declare types like this:
domain 'a foo = Foo "(foo -> 'a) -> 'a" | Bar 'a
Currently, support for indirect recursion is rather limited (you can't
use indirect recursion with arbitrary type constructors, due to
soundness concerns), and the domain package doesn't give you a very
useful induction rule for such types. But I am working on some big
improvements; the support for indirect recursion should get much
better within the next few months.
Quoting Tobias Nipkow <nipkow@in.tum.de>:
Email Gateway (Aug 18 2022 at 13:06):From: Brian Huffman <brianh@cs.pdx.edu>
Unfortunately, code generation does not currently work for HOLCF definitions.
This is also on our to-do list. I plan to bring this up at the next
Isabelle developer's meeting this summer, if it hasn't been dealt with
before then. Implementing it will take some coordinated effort between
the HOLCF people (mainly me) and the code generation people (mainly
Florian Haftmann).
Of course, if users are clamoring for this new feature, it might
encourage us to implement it sooner...
Quoting Jeremy Siek <jeremy.siek@gmail.com>:
Email Gateway (Aug 18 2022 at 13:07):From: Jeremy Siek <jeremy.siek@gmail.com>
Good to hear.
Does the code generation support work for HOLCF fixrec
definitions?
Cheers,
Jeremy
Email Gateway (Aug 18 2022 at 13:07):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
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.
Email Gateway (Aug 18 2022 at 13:07):From: Jeremy Siek <jeremy.siek@gmail.com>
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
Email Gateway (Aug 18 2022 at 13:12):From: Jeremy Siek <jeremy.siek@gmail.com>
Lately I've been investigating writing interpreters in Isabelle/HOL and
ran into a problem when trying to support first-class continuations. The
typical approach when writing an interpreter in ML or Haskell is to
write the interpreter in continuation passing style (or monadic style)
and to embed the continuations as functions in the value (or expression)
datatype. Of course, in Isabelle/HOL this is not possible.
Using alternative approaches, such as SOS or abstract machines, this is not
a problem because continuations are represented explicitly as data.
At this point I'm thinking that one can't write an interpreter in Isabelle
that supports first-class continuations, but perhaps I'm overlooking something?
Cheers,
Jeremy
Email Gateway (Aug 18 2022 at 13:13):From: Tobias Nipkow <nipkow@in.tum.de>
Not in HOL (or other logics of total functions), but in the extension
HOLCF, which supports a separate type of continuous functions. I am not
sure if HOLCF has been used for this purpose before.
Tobias
Jeremy Siek schrieb:
Last updated: May 03 2024 at 08:18 UTC