Email Gateway (Aug 22 2022 at 14:16): Email Gateway (Aug 22 2022 at 14:16):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Any ideas about the following?
theory Barf
imports Main
begin
datatype 't "term" =
Const 't
| U
| T "'t term * 't term"
| C "'t term * 't term"
| L "'t term"
| L' "'t term"
| R "'t term"
| R' "'t term"
| A "'t term * 't term * 't term"
| A' "'t term * 't term * 't term"
fun F :: "'a term ⇒ int"
where "F (T (T (U, b), c)) = 1 + F (T (U, T (b, c)))"
| "F (T (T (a, b), c)) = 1 + F a + F (T (b, c))"
| "F (T (U, b)) = 1 + F b"
| "F (T (a, U)) = 1 + F a"
| "F (T (a, b)) = (F a) + (F b)"
| "F a = undefined"
(* exception Chr raised (line 268 of "./basis/String.sml") *)
end
Barf.thy
Email Gateway (Aug 22 2022 at 14:16):From: Lars Hupel <hupel@in.tum.de>
Hi Eugene,
(* exception Chr raised (line 268 of "./basis/String.sml") *)
this is a fun problem!
By looking at the exception trace (to be enabled with "declare
[[ML_exception_trace]]" before "fun"), we can see the culprit:
Lexicographic_Order.no_order_msg
This function formats the message you see when the function package is
unable to find a termination order. In this specific case it fails
because it tries to come up with some alphabetic index:
val gc = map (fn i => chr (i + 96)) (1 upto length table)
Because there function definition explodes in size internally, the
argument passed to "chr" is simply out of range.
I'm pretty sure the author of the function package did not anticipate
such large functions ...
Cheers
Lars
Email Gateway (Aug 22 2022 at 14:17):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Eugene,
The problem seems to be with lexicographic_order (it probably tries to generate some error
or info message in which a conversion to characters fails). If you use size_change in the
termination proof, it works:
function (sequential) F :: "'a term ⇒ int"
where "F (T (T (U, b), c)) = 1 + F (T (U, T (b, c)))"
| "F (T (T (a, b), c)) = 1 + F a + F (T (b, c))"
| "F (T (U, b)) = 1 + F b"
| "F (T (a, U)) = 1 + F a"
| "F (T (a, b)) = (F a) + (F b)"
| "F a = undefined"
by pat_completeness auto
termination by size_change
Best,
Andreas
Last updated: Apr 24 2024 at 08:20 UTC