[isabelle] primrec of datatype containing fset · Archive Mirror: Isabelle Users Mailing List

Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] primrec of datatype containing fset

Email Gateway (Aug 22 2022 at 15:42):

From: "Siek, Jeremy" <jsiek@indiana.edu>
I’d like to write recursive functions over the following datatype:

datatype val = VNat nat | VRel "(val × val) fset"

As a simple example,

primrec count :: "val ⇒ nat" where
"count (VNat n) = 1" |
"count (VRel t) = (ffold (λ (v1,v2). λ r. count v1 + count v2 + r) 0 t)"

But this get’s rejected with the “Invalid map function” error.

What’s the correct way to do this?

Cheers,
Jeremy

Jeremy G. Siek <jsiek@indiana.edu<mailto:jsiek@indiana.edu>>
Associate Professor
School of Informatics and Computing
Indiana University Bloomington
http://homes.soic.indiana.edu/jsiek/

Email Gateway (Aug 22 2022 at 15:42):

From: Lars Hupel <hupel@in.tum.de>
Dear Jeremy,

I’d like to write recursive functions over the following datatype:

datatype val = VNat nat | VRel "(val × val) fset"

As a simple example,

primrec count :: "val ⇒ nat" where
"count (VNat n) = 1" |
"count (VRel t) = (ffold (λ (v1,v2). λ r. count v1 + count v2 + r) 0
t)"

But this get’s rejected with the “Invalid map function” error.

this is a restriction of "primrec". What you're writing is not in fact a
primitive recursive specification. There are two ways around that:

1) Rewrite it as primitive recursive
2) Use the "fun"/"function" command

Here is option 1:

primrec count :: "val ⇒ nat" where
"count (VNat n) = 1" |
"count (VRel t) = (ffold (λ (v1,v2). λ r. v1 + v2 + r) 0 (map_prod count
count |`| t))"

Observe that the recursive calls of "count" must only occur within
suitable "map functions" of the involved type constructors. In your case,
the recursion of "val" is nested through a pair and an "fset". Hence, the
use of "|`|" (map for "fset") and "map_prod" (map for "prod").

Option 2:

fun count :: "val ⇒ nat" where
"count (VNat n) = 1" |
"count (VRel t) = (ffold (λ (v1,v2). λ r. count v1 + count v2 + r) 0 t)"

The problem here is showing termination. The function package tries to
automatically derive a termination relation, which fails here.

It can be specified manually as follows:

function (sequential) count :: "val ⇒ nat" where
"count (VNat n) = 1" |
"count (VRel t) = (ffold (λ (v1,v2). λ r. count v1 + count v2 + r) 0 t)"
by pat_completeness auto

termination
apply (relation "measure size")
<proof>

But as far as I can tell, the resulting goal is not actually provable. The
reason is that the function package has no idea how recursive calls nested
in "ffold" work. There are ways to explain to the function package how this
works, but I'm not sure if it's possible in this concrete case. One would
need a lemma like this:

lemma ffold_cong[fundef_cong]:
assumes "⋀x y. x |∈| S ⟹ f x y = g x y" "x = y" "S = T"
shows "ffold f x S = ffold g y T"
sorry

Using this lemma, we can successfully prove termination, but I'm not sure
whether it actually holds.

In summary, I think you're left with either rewriting your function to be
primitive recursive, or avoid "non-deterministic" functions like "ffold".

Cheers
Lars

Email Gateway (Aug 22 2022 at 15:42):

From: "Siek, Jeremy" <jsiek@indiana.edu>
Dear Lars,

Thank you for your very thorough answer! It looks like option 1 will suite my needs.

Thank you!
Jeremy

Email Gateway (Aug 22 2022 at 15:42):

From: Lars Hupel <hupel@in.tum.de>

Thank you for your very thorough answer! It looks like option 1 will
suite
my needs.

On second thought, I realised that your use of "ffold" is merely to
compute the sum of some things in a set. Luckily, we can make "function"
cope with that. See attachment for a possible solution (also a version with
"primrec" that doesn't use "ffold").

Cheers
Lars
Scratch.thy

Email Gateway (Aug 22 2022 at 15:43):

From: Lawrence Paulson <lp15@cam.ac.uk>
These days, users should regard "primrec" as an internal feature necessary for bootstrapping the system but for implementers only.

Larry Paulson

Email Gateway (Aug 22 2022 at 15:43):

From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Hi Jeremy and Lars,

Special care is needed when recursing through permutative structures like sets and multisets. For example, the primrec version discussed here is _not_ equal to the 'fun' version of 'count', since it recursively collapses the numbers coming from subtrees that happen to have the same count. The 'fun' version is the correct one.

All the best,

Andrei

From: cl-isabelle-users-bounces@lists.cam.ac.uk <cl-isabelle-users-bounces@lists.cam.ac.uk> on behalf of Lars Hupel <hupel@in.tum.de>
Sent: 09 July 2017 11:28
To: Siek, Jeremy
Cc: cl-isabelle-users@lists.cam.ac.uk
Subject: Re: [isabelle] primrec of datatype containing fset

Thank you for your very thorough answer! It looks like option 1 will
suite
my needs.

Cheers
Lars

Email Gateway (Aug 22 2022 at 15:43):

From: Lars Hupel <hupel@in.tum.de>
Hi Andrei,

Special care is needed when recursing through permutative structures like sets and multisets. For example, the primrec version discussed here is _not_ equal to the 'fun' version of 'count', since it recursively collapses the numbers coming from subtrees that happen to have the same count. The 'fun' version is the correct one.

ah of course, you're right. Sorry for the mistake, Jeremy!

Cheers
Lars

Email Gateway (Aug 22 2022 at 15:43):

From: Manuel Eberl <eberlm@in.tum.de>
I don't fully agree.

There are some cases, like infinitely-branching datatypes, where
"primrec" works without problems, but "function" requires considerable
additional work (because there is no usable "size" function).

Also, for datatypes with many constructors, I think "function" can be
quite slow due to the huge number of things it does and theorems that it
proves. "primrec" is a good light-weight alternative then.

Personally, I tend to use primrec rather than fun whenever it is
possible to do so without significant effort.

Manuel

Email Gateway (Aug 22 2022 at 15:43):

From: "Siek, Jeremy" <jsiek@indiana.edu>
Hi Andrei,

Good catch!

But now I’m a bit unsatisfied… the function version of count required a fair bit of work and
looks like it’s rather specific, so I may have to repeat this amount of work for every
other recursive function on datatype val.

I wonder if the termination argument involving fsum could be adapted to ffold?

Cheers,
Jeremy

On Jul 9, 2017, at 7:19 AM, Andrei Popescu <A.Popescu@mdx.ac.uk<mailto:A.Popescu@mdx.ac.uk>> wrote:

Hi Jeremy and Lars,

All the best,

Andrei

From: cl-isabelle-users-bounces@lists.cam.ac.uk<mailto:cl-isabelle-users-bounces@lists.cam.ac.uk> <cl-isabelle-users-bounces@lists.cam.ac.uk<mailto:cl-isabelle-users-bounces@lists.cam.ac.uk>> on behalf of Lars Hupel <hupel@in.tum.de<mailto:hupel@in.tum.de>>
Sent: 09 July 2017 11:28
To: Siek, Jeremy
Cc: cl-isabelle-users@lists.cam.ac.uk<mailto:cl-isabelle-users@lists.cam.ac.uk>
Subject: Re: [isabelle] primrec of datatype containing fset

Thank you for your very thorough answer! It looks like option 1 will
suite
my needs.

Cheers
Lars

Jeremy G. Siek <jsiek@indiana.edu<mailto:jsiek@indiana.edu>>
Associate Professor
School of Informatics and Computing
Indiana University Bloomington
http://homes.soic.indiana.edu/jsiek/

Email Gateway (Aug 22 2022 at 15:43):

From: Manuel Eberl <eberlm@in.tum.de>
Personally, I would suggest something like this:

lemma single_le_sumI:
assumes "∃b∈A. a ≤ (f b :: nat)" "finite A"
shows "a ≤ (∑b∈A. f b)"
proof -
from assms obtain b where "b ∈ A" "a ≤ f b" by blast
note this(2)
also from ‹b ∈ A› and ‹finite A›
have "f b ≤ (∑b∈A. f b)" by (intro member_le_sum) auto
finally show ?thesis .
qed

function count :: "val ⇒ nat" where
"count (VNat n) = 1" |
"count (VRel A) = (∑(x,y)∈fset A. count x + count y)"
by pat_completeness auto
termination by (relation "measure size") (force simp: less_Suc_eq_le
intro: single_le_sumI)+

This reuses the summation function for sets, and I think that will be
much nicer to work with than a fold. The termination proof is still a
bit messy, unfortunately, and I don't know what can be done about it in
general, but at least similar cases should also work with this "one-liner".

Manuel

Email Gateway (Aug 22 2022 at 15:43):

From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Dear Larry,

These days, users should regard "primrec" as an internal feature necessary for bootstrapping the system but for implementers only.

While this is true in most cases, in complex situations involving nested recursion "primrec" can provide the most elegant solution. For example, compare the "function"-based definition with the following correct primrec definition:

primrec count' :: "val ⇒ nat" where
"count' (VNat n) = 1" |
"count' (VRel t) = fsum (λ((_,v), (_,u)). v + u) (fimage (map_prod (λ v. (v,count' v)) (λ v. (v,count' v))) t)"

(This is now correct since all subtrees are counted as separate entities, taking advantage of full primitive recursion as opposed to mere iteration.)

With a proper setting for congruences and such, this can be handled by "function" as well, but this is tricky and quite laborious -- as the current thread shows.

Best,

Andrei

Larry Paulson

On 9 Jul 2017, at 11:15, Lars Hupel <hupel@in.tum.de> wrote:

this is a restriction of "primrec". What you're writing is not in fact a
primitive recursive specification. There are two ways around that:

1) Rewrite it as primitive recursive
2) Use the "fun"/"function" command

Email Gateway (Aug 22 2022 at 15:43):

From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Hi Jeremy,

Hi Andrei,
Good catch!
But now I’m a bit unsatisfied… the function version of count required a fair bit of work and
looks like it’s rather specific, so I may have to repeat this amount of work for every
other recursive function on datatype val.
I wonder if the termination argument involving fsum could be adapted to ffold?

It can, with some tricks.

But for this particular function, primrec works:

primrec count :: "val ⇒ nat" where
"count (VNat n) = 1" |
"count (VRel t) = fsum (λ((_,n), (_,m)). n + m) (fimage (map_prod (λ v. (v,count v)) (λ v. (v,count v))) t)"

If you have a genuinely primitive recursion function and primrec seems to cause you trouble, you can always use the primtive recursive combinator

rec_val :: (nat ⇒ 'a) ⇒ (((val × 'a) × val × 'a) fset ⇒ 'a) ⇒ val ⇒ 'a

explicitly, and then infer the high-level equations, e.g.:

definition count where "count = rec_val (λn. 1) (fsum (λ((_,n), (_,m)). n + m))"
lemma count_simps[simp]:
"count (VNat n) = 1"
and
"count (VRel t) = fsum (λ((_,n), (_,m)). n + m) (fimage (map_prod (λ v. (v,count v)) (λ v. (v,count v))) t)"
unfolding count_def by auto

This is essentially what the primrec package does for you automatically, but sometimes, esp. for nested recursion, the combinator version is easier to get right.

I would be curious to know what other functions you would like to define on val. These examples would help us devise the right support for ffold and friends in the finite set library.

Best,

Andrei

On Jul 9, 2017, at 7:19 AM, Andrei Popescu <A.Popescu@mdx.ac.uk<mailto:A.Popescu@mdx.ac.uk>> wrote:

Hi Jeremy and Lars,

All the best,

Andrei

Thank you for your very thorough answer! It looks like option 1 will
suite
my needs.

Cheers
Lars

Jeremy G. Siek <jsiek@indiana.edu<mailto:jsiek@indiana.edu>>
Associate Professor
School of Informatics and Computing
Indiana University Bloomington
http://homes.soic.indiana.edu/jsiek/

Email Gateway (Aug 22 2022 at 15:44):

From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Hi Manuel,

Sorry, I had missed your message. I fully agree with your disagreement. :-)

Best,

Andrei

Email Gateway (Aug 22 2022 at 15:44):

From: "Siek, Jeremy" <jsiek@indiana.edu>
Thanks Andrei!

Cheers,
Jeremy

On Jul 9, 2017, at 8:16 AM, Andrei Popescu <A.Popescu@mdx.ac.uk<mailto:A.Popescu@mdx.ac.uk>> wrote:

Dear Larry,

These days, users should regard "primrec" as an internal feature necessary for bootstrapping the system but for implementers only.

primrec count' :: "val ⇒ nat" where
"count' (VNat n) = 1" |
"count' (VRel t) = fsum (λ((_,v), (_,u)). v + u) (fimage (map_prod (λ v. (v,count' v)) (λ v. (v,count' v))) t)"

(This is now correct since all subtrees are counted as separate entities, taking advantage of full primitive recursion as opposed to mere iteration.)

With a proper setting for congruences and such, this can be handled by "function" as well, but this is tricky and quite laborious -- as the current thread shows.

Best,

Andrei

Larry Paulson

On 9 Jul 2017, at 11:15, Lars Hupel <hupel@in.tum.de<mailto:hupel@in.tum.de>> wrote:

this is a restriction of "primrec". What you're writing is not in fact a
primitive recursive specification. There are two ways around that:

1) Rewrite it as primitive recursive
2) Use the "fun"/"function" command

Jeremy G. Siek <jsiek@indiana.edu<mailto:jsiek@indiana.edu>>
Associate Professor
School of Informatics and Computing
Indiana University Bloomington
http://homes.soic.indiana.edu/jsiek/

Email Gateway (Aug 22 2022 at 15:44):

From: Dmitriy Traytel <traytel@inf.ethz.ch>
And I agree with Andrei’s agreement to Manuel’s disagreement. :)

The question of using primrec or fun shows up every now and then on this mailing list, e.g., here https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-May/msg00037.html <https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-May/msg00037.html>.

Next to the reasons brought up by Manuel before, I also particularly agree with Florian’s advice to use the least powerful command as a means of documentation: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-May/msg00044.html <https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-May/msg00044.html>

Dmitriy

Last updated: Nov 21 2024 at 12:39 UTC