Email Gateway (Aug 18 2022 at 12:59): Email Gateway (Aug 18 2022 at 12:59):From: Peter Chapman <pc@cs.st-and.ac.uk>
Hi
I have a polymorphic datatype as follows
datatype 'a form:
ff
| Cpd 'a ('a form list)
I also have a function which, given a list of naturals, returns the
largest, called max_list. I want to define a function on my datatype
as follows:
primrec depth :: 'a form => nat
depth ff = 0
depth Cpd f fs = max_list (map depth fs) + 1
Isabelle doesn't like it, giving me the error message
*** Entity to be defined occurs on rhs
*** The error(s) above occurred in definition "depth_form_def":
*** "depth =_ form_rec_1 (\ i. 0) (\ f fs fsa. max_list (map depth
fs) + 1) 0 undefined undefined"
*** At command "primrec".
(where =_ is the identity symbol, and \ is a lambda). Is this not a
proper recursive call? I think it should be. For instance, if it is
written as
depth Cpd f [p,...q] = max_list [depth p,..., depth q]
then I think it is a recursive call. Can anyone point out how to fix
this, or why I am wrong in my belief?
Cheers
Peter
Email Gateway (Aug 18 2022 at 12:59):From: Stefan Berghofer <berghofe@in.tum.de>
Peter Chapman wrote:
Hi Peter,
unfortunately, the primrec command is rather restrictive as far as the recursion
scheme of the function is concerned. More precisely, it requires that the recursion
scheme of the function exactly matches the recursion scheme of the datatype. Since
the datatype "'a form" involves nested recursion through the list type constructor,
the type of lists is "unfolded" when constructing the datatype, as can be seen
from the induction rule
[| P1 ff; !!list. P2 list ==> P1 (Cpd a list); P2 [];
!!form list. [| P1 form; P2 list |] ==> P2 (form # list) |] ==>
P1 form & P2 list
which involves two predicates P1 and P2. Consequently, primrec also expects you
to define your depth function as two mutually recursive functions, where one of
the functions is on "'a form", while the other one is on "'a form list":
primrec depth :: "'a form => nat" and depth_list :: "'a form list => nat list" where
"depth ff = 0"
| "depth (Cpd f fs) = max_list (depth_list fs) + 1"
| "depth_list [] = []"
| "depth_list (f # fs) = depth f # depth_list fs"
Alternatively, you can also use the more general "fun" command for defining
functions by well-founded recursion, which accepts your definition right away:
fun depth :: "'a form => nat" where
"depth ff = 0"
| "depth (Cpd f fs) = max_list (map depth fs) + 1"
Greetings,
Stefan
Email Gateway (Aug 18 2022 at 12:59):From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
Hi Peter,
datatype 'a form:
ff
| Cpd 'a ('a form list)
the problem is that Cpd does not take a parameter of type "'a form", but
the "'a form" is nested inside the list type constructor. Internally,
such nested datatypes are converted into mutually recursive datatypes,
which becomes visible when you try to use primrec.
If you want to use primrec, you must define mutually recursive
functions, i.e. the following should work:
primrec depth :: 'a form => nat and depths :: 'a form list => nat list
where
depth ff = 0
| depth Cpd f fs = max_list (depths fs) + 1
| depths [] = []
| depths (x # xs) = (depth x) # (depths xs)
Then, you can later on prove a lemma saying
"depth Cpd f fs = max_list (map depth fs)"
by induction on fs.
Alternatively, you can use the function package instead of primrec,
which allows arbitrary pattern matchings and recursion. Since Isabelle
2008, the termination prover usually handles such primitive recursion
for nested datatypes.
Andreas
Last updated: May 03 2024 at 08:18 UTC