Email Gateway (Aug 18 2022 at 18:14): Email Gateway (Aug 18 2022 at 18:14):From: René Neumann <lists@necoro.eu>
Hi all,
I had to define a function that needed its own proof of termination.
Thereby I noticed an issue, I'd like to show by example:
Let succs :: "('a × 'a) set ⇒ 'a ⇒ 'a set"
and then define some example function "foo":
function foo :: "('a × 'a) set ⇒ 'a ⇒ nat ⇒ nat" where
"foo E v n = (if n > 0 then
fold (λv'.λn. if n = 0 then 0
else foo E v' n) (n - 1) (succs E v)
else 0)"
This function might f.ex. being seen as walking depth-first through a
graph, doing at most n steps.
The problem now arises when showing termination: A 'termination proof'
wants me to show the following goal (the concrete measurement ?R should
be unimportant to my issue, but should probably rely on n):
⋀E v n x xa. ⟦0 < n; xa ≠ 0⟧ ⟹ ((E, x, xa), E, v, n) ∈ ?R
As you might notice there is no relation between xa and n, though it
should be something like "xa = n - 1".
Is it possible somehow to put the relation in again without doing some
heavy rewriting of the function? (As this might work for one case but
not for another)
Thanks,
René
Email Gateway (Aug 18 2022 at 18:14):From: Konrad Slind <konrad.slind@gmail.com>
Hi Rene,
Since there is an occurrence of fold, you need to have
a congruence rule for fold installed so the termination
extraction machinery will do the right thing. I imagine
the documentation discusses this.
Cheers,
Konrad.
Last updated: Apr 26 2024 at 04:17 UTC