Re: [isabelle] Lazy Lists



Dear Christian,

if you want to formalise functional programming, I recommend HOLCF over Coinductive, because domain theory is the semantics behind Haskell, not coinductive datatypes. HOLCF lists, for example, can distinguish between "definitely terminating", "definitely infinite", and "evaluated up to a certain point with unknown rest". Coinductive lists ('a llist) cannot express the last case. You can then also do induction over HOLCF lists, known as Scott induction.
However, using standard HOL types and functions within HOLCF may need some work.

Lets consider we use "'a llist" (from AFP/Coinductive) for lazy lists and "'a
list" for finite lists.
The predicate "lfinite" is defined inductively, so you could do induction on that. But obviously, your induction then has to thread through this predicate.

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.
I tried to set it up in the attached theory, but it only seems to works in the wrong direction: You can prove theorems on 'a list by transferring them to 'a llist with the lfinite predicate. Since neither 'a llist nor 'a list are defined in terms of each other, you need to do the setup manually, i.e., prove all those transfer rules that relate functions on 'a llist with those on 'a list. Maybe the transfer package experts can improve my attempt.

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.
Unfortunately, there is currently no support for corecursive definitions.

So, here is a wish-list:
- in contexts where we have "lfinite", reuse facts on "'a list" functions
That would be great, but you have to ensure that the functions on 'a llist behave exactly like on 'a list. This is non-trivial for underspecified functions like hd and nth when applied with inappropriate parameters (such as []). I tried hard to make these functions coindice (see, e.g., the "undefined (Suc n)" in the definition of lnth), but I do not remember whether this was always possible.

- provide a command that allows to define functions on "'a llist" using the same
notation as "fun" (is this already possible?)
I hope that the new package for codatatypes provides at least "coprimrec". I doubt that there will be a powerful tool for arbitrary corecursive definitions, because the internal constructions and proofs required differ considerably from well-founded recursions.

- 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?
The last two should be easy to accomplish. Even you yourself could do that, one only has to adapt the section on code_type and code_const in List.thy for Coinductive_List_Lib.

Hope this helps,
Andreas

--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft
theory Transfer_List 
imports
  Quotient_Coinductive_List 
begin

lemma transfer_list_llist: "type_definition llist_of list_of {xs. lfinite xs}"
by unfold_locales simp_all

setup_lifting transfer_list_llist

lemma [transfer_rule]: "cr_list LNil []" 
by(simp add: cr_list_def)

lemma [transfer_rule]: "(op = ===> cr_list ===> cr_list) LCons op #"
by(rule fun_relI)+(simp add: cr_list_def)

lemma [transfer_rule]: "(cr_list ===> cr_list ===> cr_list) lappend op @"
by(rule fun_relI)+(simp add: cr_list_def)

lemma "xs @ [] = xs"
by transfer simp

lemma "lfinite xs \<Longrightarrow> lappend xs LNil = xs"
oops

end


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