Email Gateway (Aug 22 2022 at 13:20): Email Gateway (Aug 22 2022 at 13:20):From: Rustom Mody <rustompmody@gmail.com>
In
http://stackoverflow.com/questions/30419419/what-is-the-difference-between-primrec-and-fun-in-isabelle-hol
the general advice seems to be:
However when I see examples anywhere I see mostly primrec and not fun
Also I remember seeing somewhere that primrec is preferable since functions
in Isabelle must be terminating and with fun that proof obligation needs
to be separately dealt with
Thanks
Rusi
Email Gateway (Aug 22 2022 at 13:20):From: Joachim Breitner <breitner@kit.edu>
Dear Rusi,
Am Mittwoch, den 11.05.2016, 16:18 +0530 schrieb Rustom Mody:
In
http://stackoverflow.com/questions/30419419/what-is-the-difference-between-primrec-and-fun-in-isabelle-hol
the general advice seems to be:*From a practitioner’s point of view, primrec is a lower-level tool that
you usually do not need to worry about, and simply always use fun.*
However when I see examples anywhere I see mostly primrec and not fun
I’m not sure about the history of primrec and fun, but some of the
examples might be from times when fun was not around, or not as good as
it is now. Also, some tutorials/classes/courses might deliberately use
primrec to force the student to be aware of the differences between
primitive recursion and general recursion.
Also I remember seeing somewhere that primrec is preferable since functions
in Isabelle must be terminating and with fun that proof obligation needs
to be separately dealt with
"fun" always proves termination (or gives up). If it cannot, you have
to use "function" and prove termination yourself.
There are only a few (obscure?) cases where fun cannot do what primrec
can, as Andreas writes on SO: When a data type does not have a size
function.
Greetings,
Joachim
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner
signature.asc
Email Gateway (Aug 22 2022 at 13:20):From: Rustom Mody <rustompmody@gmail.com>
Ok if you say so :-)
However http://isabelle.in.tum.de/doc/tutorial.pdf is from 2016 and still
heavily uses primrec?
[Sorry for being obtuse -- just finding it hard to find my way around]
Email Gateway (Aug 22 2022 at 13:20):From: Gergely Buday <gbuday@karolyrobert.hu>
Hi,
the tutorial is originally from 2001 so might use idioms not up to date now.
Email Gateway (Aug 22 2022 at 13:20):From: Tobias Nipkow <nipkow@in.tum.de>
This tutorial was written in 2000, before fun. It doesn't reflect Isabelle 2016
at all anymore, it was merely kept alive because it contains interesting
examples. It will not be distributed as part of the Isabelle documentation in
the future.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 13:21):From: Manuel Eberl <eberlm@in.tum.de>
One of the advantages of primrec is that fun generates a number of
auxiliary definitions and facts that you may not need for simple
recursion patterns like the ones supported by primrec, so primrec is
more ‘light-weight’ and may be faster.
I therefore tend to use primrec whenever it is possible and I don't need
the facts generated by fun.
Manuel
Email Gateway (Aug 22 2022 at 13:21):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
That difference is indeed significant for more than theoretical reasons.
Your ultimate aim is not to specify something but to actually prove
properties about it. Specifications mechanisms indicate what proof
principle is likely most suitable to derive fundamental properties:
definition -> unfolding
inductive -> induction using specific induct rule
function -> induction using specific induct rule
primrec -> structural induction over a datatype
Hence primrec can be seen as a codified comment in that respect.
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 13:21):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Joachim wrote:
There's also the case of mutual recursion on mutually defined datatypes, where I've seen some "fun" failures.
"primrec" is more lightweight, so if you develop large theories it might help make Isabelle take fewer resources. Might because I'm not aware of any actual measurements.
Jasmin
Last updated: May 06 2024 at 16:21 UTC