[isabelle] Lazy Lists



Dear all,

just for fun, I recently wanted to formalize the first "pearl" from the book "Pearls of Functional Algorithm Design" (by Richard Bird) inside Isabelle/HOL. The solutions in the book are implemented in Haskell and sometimes rely on lazy evaluation.

I stumbled across the following points. In proofs the case of infinite lists is (as far as I read) never considered (i.e., plain structural induction on finite lists is used). However, the implementations sometimes contain infinite lists like [0..]. Since this "omissions" are only done in contexts where the lists that are used for induction are really finite, this seems to be fine.

My question is now, how closely can such a kind of proof be imitated inside Isabelle/HOL?

Lets consider we use "'a llist" (from AFP/Coinductive) for lazy lists and "'a list" for finite lists.

If I'm correct, the new transfer package should be able (after appropriate setup) to transfer facts from "'a list" to "'a llist" with additional "lfinite ..." assumptions (and also the other way round?). But how this setup is actually done, I did not find out. The current documentation of the transfer package is rather inaccessible (in fact I only know of the example theories that are mentioned in the NEWS file).

Another issue is that Haskell functions (on lazy lists) are defined using notation like "fun" of Isabelle/HOL despite not being based on well-founded recursion, whereas for function definitions on "'a llist" in Isabelle/HOL this does not work (at least I don't know how). That is, there is a gap between what is used in Haskell programming and how this can be "simulated" in Isabelle/HOL.

So, here is a wish-list:
- in contexts where we have "lfinite", reuse facts on "'a list" functions
- provide a command that allows to define functions on "'a llist" using the same notation as "fun" (is this already possible?) - for Haskell code generation Nil and LNil as well as Cons and LCons should be unified and mapped to [] and (:) of Haskell - moreover, would it be possible to unify "equivalent" (modulo infiniteness) functions like "map" and "lmap", "filter" and "lfilter" ..., for code generation?

My main questions are:
1) how would the above mentioned transfer setup work?
2) how realistic is the above wish-list and what do you think about it?

cheers

chris





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.