Re: [isabelle] primrec of datatype containing fset



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.