Email Gateway (Aug 18 2022 at 20:12): Email Gateway (Aug 18 2022 at 20:12):From: Christian Sternagel <c-sterna@jaist.ac.jp>
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:
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
Email Gateway (Aug 18 2022 at 20:12):From: Christian Sternagel <c-sterna@jaist.ac.jp>
On 06/25/2012 01:21 PM, Peter Gammie wrote:
Christian,
(We could have this conversation on the list if you like - just post any followup there.)
On 25/06/2012, at 2:10 PM, Christian Sternagel wrote:
thanks for the pointer to HOLCF. Assuming code generation works (almost) as usual for HOLCF, this is indeed what I was looking for.
AFAIK the code generator does not work at all for HOLCF.
If that is the case, it would be interesting to know whether this is an
inherent restriction or would "just" require more work (I know by
painful experience that such "just"s can get quite huge ;)).
I would love to be able to formalize functions as is done in lazy
functional programming papers and get generated code "for free".
PS: I wanted to download your paper on the worker/wrapper transformation from your website, but the file seems to be damaged (at least that's what two of my pdf reader applications are claiming).
Oops, thanks for that.
I'd recommend you scrape the theory out of the AFP - it subsumes the JFP paper.
Good to know, thanks.BTW this transformation should apply to other inductively-defined things, e.g. inductive definitions in HOL.
However I have not investigated how you'd connect an inductive thing (e.g. a function nat => 'a) to it's coinductive counterpart (e.g. an 'a llist) using it. (It works in a domain theoretic setting as recursive domain equations have unique fixed points.)
I guess this is the same problem as relating "'a list" to "'a llist"?There's some work on this by Thorsten Altenkirch et al that is heavy on the category theory (TLCA 2001?) - I think the keyword is "containers". See the original worker/wrapper paper by Hutton and Gill for the reference.
cheers
chris
Email Gateway (Aug 18 2022 at 20:12):From: Peter Gammie <peteg42@gmail.com>
Christian,
Probably. Roughly I think Altenkirch et al show that if you have a function from an inductively-defined domain then there is an equivalent coinductive definition of that function.
You can think of it as a generalisation of using lazy lists to memoise functions from the natural numbers, as Hutton and Gill did in their worker/wrapper paper. In their setting, for (partial) f :: nat -> 'a, f x is memoised by the x'th element of the lazy list. (In a total setting you'd want to use streams, not lazy lists.)
In general you need to index into a more complex coinductive type (whose structure depends on the type of the function's domain). There's probably a link to differentiating datatypes, zippers and so forth too.
Their framework probably handles the issue in the paper I mentioned earlier.
BTW I think it is great you are contemplating putting Bird et al's work through a proof assistant. Parts of Bird's theory of lists (from circa 1987) are still visible in List.thy. One might hope the newer work is similarly useful.
I'll leave the questions about code generation to Brian and Florian.
cheers
peter
Email Gateway (Aug 18 2022 at 20:12):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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
Transfer_List.thy
Email Gateway (Aug 18 2022 at 20:12):From: Lawrence Paulson <lp15@cam.ac.uk>
Absolutely and definitely true. HOLCF is explicitly a theory of computation; Coinductive is merely a theory of infinite objects. Such a pity if it doesn't yet support code generation.
Larry
Email Gateway (Aug 18 2022 at 20:13):From: Brian Huffman <huffman@in.tum.de>
On Mon, Jun 25, 2012 at 8:43 AM, Andreas Lochbihler
<andreas.lochbihler@kit.edu> wrote:
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.
That's right: The automation provided by the setup_lifting command is
designed for transferring theorems from supertype to subtype, not the
other way around. But you can always define your own transfer relation
manually, in whichever direction you want. The attached theory file
defines a relation for transferring from list to llist (it is the
converse of the relation that would be generated by setup_lifting),
and shows how it can be used.
Using the "transfer" proof method (which acts like the "descending"
method from the Quotient package) is rather cumbersome for these kinds
of examples; once we get around to implementing counterparts to the
"lifting" method and "lifted" attribute, transferring theorems from
list to llist should be a lot easier.
So, here is a wish-list:
- in contexts where we have "lfinite", reuse facts on "'a list" functions
Using the planned but yet-to-be-implemented "transferred" attribute,
this kind of transfer should be completely automatic. You should be
able to write
map_append [transferred tr_llist]
and get the theorem
"lfinite xs ==> lfinite ys ==> lmap f (lappend xs ys) = lappend (lmap
f xs) (lmap f ys)"
(assuming that the transfer rules are set up as in the attached theory file).
This feature will definitely be available before the next Isabelle release.
Last updated: Apr 24 2024 at 04:17 UTC