Email Gateway (Aug 18 2022 at 17:59): Email Gateway (Aug 18 2022 at 17:59):From: Mathieu Giorgino <mathieu.giorgino@IRIT.FR>
Hi all,
I just noticed a problem with "let" bindings on left-nested tuples in function
definitions.
For example, these 2 functions -- each written with "function" and "fun" --
are exactly the same, excepted for the nesting of tuples.
theory Scratch imports Main
begin
function (sequential) f1 :: "(nat * nat * nat) \<Rightarrow> unit"
where
"f1 (_, _, 0) = ()"
| "f1 n = (let (a1, a2, a3) = n in f1 (a2+2, a1+1, a3 - 1))"
by pat_completeness auto
termination
apply (relation "measure (snd o snd)")
apply (auto simp del:in_measure)
by auto
fun f1' :: "(nat * nat * nat) \<Rightarrow> unit"
where
"f1' (_, _, 0) = ()"
| "f1' n = (let (a1, a2, a3) = n in f1' (a2+2, a1+1, a3 - 1))"
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
termination
apply (relation "measure snd")
apply (auto simp del:in_measures)
oops
fun f2' :: "((nat * nat) * nat) \<Rightarrow> unit"
where
"f2' ((_, _), 0) = ()"
| "f2' n = (let ((a1, a2), a3) = n in f2' ((a2+2, a1+1), a3 - 1))"
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.
In these examples, the let could be replaced by the function pattern matching
but this problem also prevents those let-bindings in more complicated
functions.
An idea on what is going wrong ?
Thanks,
Mathieu
Email Gateway (Aug 18 2022 at 17:59):From: Brian Huffman <brianh@cs.pdx.edu>
Hi Mathieu,
I'm pretty sure that this is a bug in the function package.
If I do a theorem search for "f2_dom" during the termination proof, I
see the following rule, which is apparently derived from f2.pinduct:
local.termination:
⟦wf ?R;
⋀v vb x xa y xb ya xc.
⟦x = (v, Suc vb); (xa, y) = x; (xb, ya) = xa⟧
⟹ (((ya + 2, xb + 1), xc - 1), v, Suc vb) ∈ ?R⟧
⟹ All f2_dom
This rule is completely useless, because it does not let you assume
anything about the variable xc. The correct form of this rule should
have "xc" replaced with "y".
Compare this with the similar rule we get for the termination proof of f1:
local.termination:
⟦wf ?R;
⋀v vb vd x xa y xb ya.
⟦x = (v, vb, Suc vd); (xa, y) = x; (xb, ya) = y⟧
⟹ ((xb + 2, xa + 1, ya - 1), v, vb, Suc vd) ∈ ?R⟧
⟹ All f1_dom
Here, the local assumptions imply that (v, vb, Suc vd) = (xa, xb, ya),
making the rule possible to use in practice.
Unfortunately I can't think of a good workaround for this problem,
unless you want to manually prove a corrected form of f2.pinduct and
the termination rule, based on unfolding the definition of f2_dom. You
will probably just have to wait for a bug fix from the developers.
Email Gateway (Aug 18 2022 at 17:59):From: Alexander Krauss <krauss@in.tum.de>
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
Last updated: May 01 2024 at 20:18 UTC