Re: [isabelle] fun termination, mutual-recursive datatype



On Thu, May 17, 2012 at 4:46 PM, John Wickerson <jpw48 at cam.ac.uk> wrote:
> Dear Isabelle,
>
> I am using a groovy mutually-recursive datatype a bit like the following one:
>
>> datatype jack = A "int" | B "jill"
>> and jill = C "int => jack" "int list"
>
> I would like to write a (mutually-recursive) function over my datatype, something like this:
>
>> datatype jack = A "int" | B "jill"
>> and jill = C "int => jack" "int list"
>>
>> fun
>>   foo_jack :: "jack => int" and
>>   foo_jill :: "jill => int"
>> where
>>   "foo_jack (A n) = n"
>> | "foo_jack (B j) = foo_jill j"
>> | "foo_jill (C f ns) = listsum (map (foo_jack \<circ> f) ns)"
>
> But the <fun> command says: "Could not find lexicographic termination order." Does anybody know how one might prove that such a function terminates?

If you unfold the function composition operator \<circ>, then the
definition works with primrec:

primrec
  foo_jack :: "jack => int" and
  foo_jill :: "jill => int"
where
  "foo_jack (A n) = n"
| "foo_jack (B j) = foo_jill j"
| "foo_jill (C f ns) = listsum (map (\<lambda>n. foo_jack (f n)) ns)"

Infinitely-branching datatypes are one area where primrec still holds
a lead over the function package.

- Brian





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