Re: [isabelle] Termination of function with let-binding on left-nested tuples



Hi Matthieu,

function (sequential) f2 :: "((nat * nat) * nat) \<Rightarrow>  unit"
   where
   "f2 ((_, _), 0) = ()"
| "f2 n = (let ((a1, a2), a3) = n in f2 ((a2+2,a1+1), a3 - 1))"
   by pat_completeness auto
[...]
Then it seems impossible to prove the termination of f2 (and "fun f2'" fails).
In the termination proof, we can see there is no equality relation for the
second component of the outermost pair.

It seems to be related to congruence rules in some way but I couldn't figure
out the exact problem.

Thanks for reporting this issue. The root of the problem lies in the way the function package extracts recursive calls from the definition. This information is then used in the construction of pretty much everything: the function itself, the graph, the domain, the rules etc.

The extraction process, guided by congruence rules, is necessarily heuristic in nature and known to be imprecise in some cases, which can then lead to unprovable termination conditions. This is also the case here (the code behaves exactly as specified), but the example is especially disturbing, since the problem is so easy and completely first-order.

Here is a different instance of the same problem, which is a bit clearer:

function f3 :: "bool => nat => nat"
where
  "f3 _ 0 = 0"
| "f3 b (Suc n) = (case b of True => f3 True | False => id) n"

Note that he branches of the case are functions, and one is a recursive call. But the argument to the call sits at the other end of the term. A similar thing happens in your example.

It seems that, unlike in most other situations, this cannot be solved (in general) by adding some cong rules. Since I'd like the process to be complete for situations like this one, I am considering adding special treatment for tuple patterns, but this is not trivial...

Alex





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