Email Gateway (Aug 18 2022 at 19:44): Email Gateway (Aug 18 2022 at 19:44):From: John Wickerson <jpw48@cam.ac.uk>
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?
Thanks very much!
John
ps. I wondered whether the problem was the (infinite) "int => jack" in the C-constructor. I replaced it with a (finite) association list "(int * jack) list", and changed foo_jill so
"foo_jill (C f ns) = listsum (map (foo_jack \<circ> (lookup f)) ns)"
where
"lookup A x == (map snd A) ! (THE i. (map fst A) ! i = x)"
but it didn't help.
Email Gateway (Aug 18 2022 at 19:44):From: Brian Huffman <huffman@in.tum.de>
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.
Email Gateway (Aug 18 2022 at 19:44):From: John Wickerson <jpw48@cam.ac.uk>
Awesome. Many thanks Brian :)
Email Gateway (Aug 18 2022 at 19:45):From: John Wickerson <jpw48@cam.ac.uk>
Why must the definition of \<circ> be unfolded? I mean, why does primrec throw an "Unknown variable foo_jack" otherwise? (I'm finding this problem with several of my other primrec definitions.)
Thanks,
john
Last updated: Apr 26 2024 at 16:20 UTC