Email Gateway (Aug 18 2022 at 11:35): Email Gateway (Aug 18 2022 at 11:35):From: Sven Schneider <svens@cs.tu-berlin.de>
Hello mailinglist
I have a problem defining a mutually recursive primrec. My problem is of
course more complex than the examples below. They are reduced versions.
_section_ 1
In this example it becomes obvious that primrec has a problem with case
and option.
_section_ 2
In this example the same code as before is used but the fun (instead of
the primrec) is capable to proof the termination.
_section_ 3
In this example the problem is more close to my problem and the primrec
does not get the calls right. f1 and f2 indeed have calls to each other,
therefore they should be at least mutually recursive... The message is a
bit confusion in my opinion. At least if the real problem is that the
primrec again cannot 'proof' termination.
_section_ 4
This example shows that f1 and f2 (defined as in section 3) depend on
each other... This seems to be a contradiction to me.
It seems that 'mutually recursive iff circular dependent' is incorrect
(of course more than mutually recursion is necessary to be able to
define a terminating function)?
_section_ 5
Using functions instead does not solve the problem. A termination
argument is not found automaticly. Attempts to do it manually didn't
resolve the problem.
_Questions_
If you haven't yet extracted any questions ;-) here they are:
1) What is the problem of the primrec exactly that the fun can resolve
(section 1+2)?
2) How to prove termination and finish the definition in section 3-5?
Bye,
Sven
_CODE_
theory test
imports Main begin
datatype phi2 =
Fin
| Con "phi2 option"
section {* 1: f0 should be primrec but isn't. *}
(*
consts
f0:: "phi2 \<Rightarrow> phi2"
primrec
"f0 Fin = Fin"
"f0 (Con x) = (case x of None \<Rightarrow> Fin | (Some y)
\<Rightarrow> Con (Some(f0 y)))"
*)
(*
*** Entity to be defined occurs on rhs
*** The error(s) above occurred in definition "f0_phi2_def":
*** "f0 \<equiv> phi2_rec_1 Fin (\<lambda>x xa. case x of None
\<Rightarrow> Fin | Some y \<Rightarrow> Con (Some (f0 y))) undefined
undefined"
*** At command "primrec".
*)
section {* 2: f3 (which is 'equal' to f0) is a function though. *}
fun f3:: "phi2 \<Rightarrow> phi2"
where
"f3 Fin = Fin"
| "f3 (Con x) = (case x of None \<Rightarrow> Fin | (Some y)
\<Rightarrow> Con (Some(f3 y)))"
section {* 3: f1,f2 call each other but they are not mutually recursive
(primrecs).*}
(*
consts
f1 :: "phi2 \<Rightarrow> phi2"
f2 :: "phi2 option \<Rightarrow> phi2 option"
primrec
"f1 Fin = Fin"
"f1 (Con f) = Con (case f of None \<Rightarrow> None | Some x
\<Rightarrow> f2 (Some x))"
"f2 None = None"
"f2 (Some a) = Some (f1 a)"
*)
(*
*** Primrec definition error:
*** functions "test.f1", "test.f2"
*** are not mutually recursive
*** At command "primrec".
*)
section {* 4: f1,f2 call each other, they are not mutually recursive but
there is a circular dependency between them.*}
(*
consts
f1 :: "phi2 \<Rightarrow> phi2"
f2 :: "phi2 option \<Rightarrow> phi2 option"
primrec
"f1 Fin = Fin"
"f1 (Con f) = Con (case f of None \<Rightarrow> None | Some x
\<Rightarrow> f2 (Some x))"
primrec
"f2 None = None"
"f2 (Some a) = Some (f1 a)"
*)
(*
*** Circular dependency of constant test.f1 -> test.f1
*** The error(s) above occurred in definition "f2_option_def":
*** "f2 \<equiv> option_rec None (\<lambda>a. Some (f1 a))"
*** At command "primrec".
*)
section {* 5: f1,f2 call each other but no termination argument is found.*}
(*
fun
f1 :: "phi2 \<Rightarrow> phi2"
and f2 :: "phi2 option \<Rightarrow> phi2 option"
where
"f1 Fin = Fin"
| "f1 (Con f) = Con (case f of None \<Rightarrow> None | Some x
\<Rightarrow> f2 (Some x))"
| "f2 None = None"
| "f2 (Some a) = Some (f1 a)"
*)
(*
*** Unfinished subgoals: (..)
*)
end
Email Gateway (Aug 18 2022 at 11:35):From: Alexander Krauss <krauss@in.tum.de>
Sven,
datatype phi2 =
Fin
| Con "phi2 option"
Your datatype has nested recursion: The recursive occurrence occurs
under the "option" type. Isabelle internally expresses this with a
mutual recursion and requires you to express your primrecs with mutual
recursion of a certain fixed form. The funny error messages you are
getting are because you are not following that schema.
Section 3.4.2 in the Tutorial describes nested recursion of datatypes,
and primrecs about such types.
The "fun" command is much more liberal about the form of the
definitions, but proving termination can be an issue.
section {* 3: f1,f2 call each other but they are not mutually recursive
(primrecs).*}
(*
consts
f1 :: "phi2 \<Rightarrow> phi2"
f2 :: "phi2 option \<Rightarrow> phi2 option"
primrec
"f1 Fin = Fin"
"f1 (Con f) = Con (case f of None \<Rightarrow> None | Some x
\<Rightarrow> f2 (Some x))"
"f2 None = None"
"f2 (Some a) = Some (f1 a)"
Obviously they are mutually recursive, but primrec is confused because
you are not following the schema: "f1 (Con f)" should call "f2 f".
section {* 4: f1,f2 call each other, they are not mutually recursive but
there is a circular dependency between them.*}
The same, but the confusion is slightly different, so you get a
different error (from a different component of the system).
section {* 5: f1,f2 call each other but no termination argument is found.*}
(*
fun
f1 :: "phi2 \<Rightarrow> phi2"
and f2 :: "phi2 option \<Rightarrow> phi2 option"
where
"f1 Fin = Fin"
| "f1 (Con f) = Con (case f of None \<Rightarrow> None | Some x
\<Rightarrow> f2 (Some x))"
| "f2 None = None"
| "f2 (Some a) = Some (f1 a)"
*)
The automatic termination prover does not deal very well with nested
datatypes yet. Section 4 of the (separate) tutorial on functions
explains how to do termination proofs manually. You should also read
Section 5 about mutual recursive functions.
Hope this helps
Alex
Last updated: May 03 2024 at 04:19 UTC