Email Gateway (Aug 22 2022 at 20:40): Email Gateway (Aug 22 2022 at 20:40):From: Lawrence Paulson <lp15@cam.ac.uk>
Dear Dominique,
It’s important to remember that Isabelle/HOL is based on higher-order logic and that most of its extensions, including recursive functions, types and predicates, are derived from first principles. So there is a bootstrapping process. A general well-founded recursion theorem is proved and the recursive data type definition package makes use of that to make primrec available on the types it introduces.
If you look at these session graph at https://isabelle.in.tum.de/dist/library/HOL/HOL/session_graph.pdf
it turns out that primrec is already available in theory Nat, where it provides primitive recursion on natural numbers, well before the function definition package in Fun_Def.
The specific advantages described by others on this list are possible because primrec maps straightforwardly to internal recursion combinators with no need to check termination or deal with pattern matching.
Larry Paulson
Email Gateway (Aug 22 2022 at 20:41):From: Dominique Unruh <unruh@ut.ee>
Thanks for your answers.
So, as an executive summary of the executive summary (including Manuel's
answer), we could say: There are cases where primrec works and fun
doesn't and vice versa. And if both work, use primrec because it's
faster and some things might be easier later.
Please correct me if that rule of thumb is wrong.
I think it might be useful to cover primrec in the function definition
tutorial.
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 20:43):From: Jasmin Blanchette via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
I'm not in charge of the "functions" tutorial, but a reference the other way does make sense. We already mentioned fun/function in the "datatypes" tutorial, but now I've just added (Isabelle/13d6b561b0ea) a paragraph capturing the essence of this thread.
Jasmin
Email Gateway (Aug 22 2022 at 20:45):From: Dominique Unruh <unruh@ut.ee>
Dear all,
Isabelle has different commands for introducing recursive functions:
fun, function, primrec.
The relationship between fun and function is clear to me: fun is just a
convenience command that invokes function with some useful defaults.
But I cannot figure out what primrec is meant for. From the
documentation (isar-ref), primrec does the same as fun, except that it
imposes additional limitations on the structure of the recursive
function. (And in contrast to the fun/function difference, it is not
easier/more compact to write.)
So my question is: Is there any difference between primrec and fun in
cases when both can be used? In that case: which command tends to be
preferable? Why does primrec exist?
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 20:46):From: Traytel Dmitriy <traytel@inf.ethz.ch>
Hi Dominique,
this is a recurring topic on this mailing list. See e.g.:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2017-July/msg00032.html
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-May/msg00037.html
The executive summary is: Reasons fo using the more low-level but also light-weight primrec include:
Dmitriy
Email Gateway (Aug 22 2022 at 20:47):From: Manuel Eberl <eberlm@in.tum.de>
There are also some things like parametricity and measurability that are
fairly easy to prove for primitive-recursive functions but can become
quite tedious for functions defined with ‘fun’.
Manuel
Last updated: Nov 21 2024 at 12:39 UTC