Email Gateway (Aug 18 2022 at 16:33): Email Gateway (Aug 18 2022 at 16:33):From: Jason Dagit <dagitj@gmail.com>
Hello,
I was trying to prove termination for the following definition:
\begin{code}
theory Termination
imports Nat Multiset Divides Datatype
begin
inductive_set even :: "nat set" where
zero[intro!]: "0 ∈ even" |
step[intro!]: "n ∈ even ⟹ (Suc (Suc n)) ∈ even"
function (sequential) foo :: "nat ⇒ nat list" where
"foo 0 = [0]" |
"foo (Suc 0) = [1]" |
"foo n = (case n ∈ even of
True ⇒ n # foo (n div 2) |
False ⇒ n # foo (Suc n))"
by pat_completeness auto
termination
apply (relation "measures [Suc, λn. n div 2]")
apply auto
oops
\end{code}
I know I can change the definition slightly for foo to make it pass the
termination checker using the standard lexicographical measure. I'm
learning about function package and specifically, how to write termination
proofs so I want to avoid the easy route here. I'm following this
documentation in particular:
http://isabelle.in.tum.de/doc/functions.pdf
My understanding of the above proof attempt is that it will never work
because the well founded relation needs for the "n \<notin> even" case to
decrease or stay the same, but instead it gets larger in the recursive call.
I can also imagine a proof of termination based on the fact that if n is odd
then Suc n will be even and the next call to foo will cause the argument to
shrink by more than it grew. Is it possible to write such a proof and lease
the termination checker? Perhaps there is something that can be done with
the function domain in the same way partial functions are handled? Advice
on how to get started with such a proof? Perhaps there are examples of this
somewhere already?
Thanks,
Jason
Email Gateway (Aug 18 2022 at 16:33):From: Tobias Nipkow <nipkow@in.tum.de>
Jason Dagit schrieb:
Hello,
I was trying to prove termination for the following definition:
\begin{code}
theory Termination
imports Nat Multiset Divides Datatype
Just a small remark: Nat, Divides and Datatype are subtheories of Main
and should not be imported selectively, they may not work as expect in
the absence of the rest of Main. In your case it was not a problem
because Multiset includes Main.
I'll let Alex answer your actual question.
Tobias
begin
inductive_set even :: "nat set" where
zero[intro!]: "0 ∈ even" |
step[intro!]: "n ∈ even ⟹ (Suc (Suc n)) ∈ even"function (sequential) foo :: "nat ⇒ nat list" where
"foo 0 = [0]" |
"foo (Suc 0) = [1]" |
"foo n = (case n ∈ even of
True ⇒ n # foo (n div 2) |
False ⇒ n # foo (Suc n))"
by pat_completeness auto
termination
apply (relation "measures [Suc, λn. n div 2]")
apply auto
oops
\end{code}I know I can change the definition slightly for foo to make it pass the
termination checker using the standard lexicographical measure. I'm
learning about function package and specifically, how to write termination
proofs so I want to avoid the easy route here. I'm following this
documentation in particular:
http://isabelle.in.tum.de/doc/functions.pdfMy understanding of the above proof attempt is that it will never work
because the well founded relation needs for the "n \<notin> even" case to
decrease or stay the same, but instead it gets larger in the recursive call.I can also imagine a proof of termination based on the fact that if n is odd
then Suc n will be even and the next call to foo will cause the argument to
shrink by more than it grew. Is it possible to write such a proof and lease
the termination checker? Perhaps there is something that can be done with
the function domain in the same way partial functions are handled? Advice
on how to get started with such a proof? Perhaps there are examples of this
somewhere already?Thanks,
Jason
Email Gateway (Aug 18 2022 at 16:33):From: Alexander Krauss <krauss@in.tum.de>
Hi Jason,
theory Termination
imports Nat Multiset Divides Datatype
First, you should import Parity, which already has the "even" predicate.
And as Tobias said, if you don't import Main, you may not get the tools
you expect, just some unfinished pieces lying around.
inductive_set even :: "nat set" where
zero[intro!]: "0 ∈ even" |
step[intro!]: "n ∈ even ⟹ (Suc (Suc n)) ∈ even"
If you define even yourself, proving a rewrite rule
"Suc n : even <-> ~ n : even" helps in the termination proof.
function (sequential) foo :: "nat ⇒ nat list" where
"foo 0 = [0]" |
"foo (Suc 0) = [1]" |
"foo n = (case n ∈ even of
True ⇒ n # foo (n div 2) |
False ⇒ n # foo (Suc n))"
by pat_completeness auto
termination
apply (relation "measures [Suc, λn. n div 2]")
apply auto
oops
My understanding of the above proof attempt is that it will never work
because the well founded relation needs for the "n \<notin> even" case to
decrease or stay the same, but instead it gets larger in the recursive call.
Yes. This measure does not work. In such a situation where there is a
temporary increase like this, you can anticipate this in the definition
of the measure, and assign a measure that already corresponds to the
increased value.
The following works for this example, assuming the [simp] rule mentioned
above:
termination
apply (relation "measures
[%n. if n <= 1 then 0 else if n : even then n else Suc n,
%n. if n : even then 0 else 1]")
apply auto
done
I can also imagine a proof of termination based on the fact that if n is odd
then Suc n will be even and the next call to foo will cause the argument to
shrink by more than it grew. Is it possible to write such a proof and lease
the termination checker?
I would assume that the idea above works in general.
There is also a different approach to handle this in the termination
prower itself, not in the measure function. It is sketched in Sect. 6 of
this paper:
http://www4.informatik.tu-muenchen.de/~krauss/shallowdp/shallowdp.pdf
But I never finished the implementation, mainly because these functions
don't arise so often, and if they do, there is always a simple manual
solution. Moreover, detecting the situation automatically is not so easy.
Hope this helps...
Alex
Email Gateway (Aug 18 2022 at 16:34):From: Jason Dagit <dagitj@gmail.com>
On Sun, Dec 19, 2010 at 3:20 AM, Alexander Krauss <krauss@in.tum.de> wrote:
Hi Jason,
theory Termination
imports Nat Multiset Divides Datatype
First, you should import Parity, which already has the "even" predicate.
And as Tobias said, if you don't import Main, you may not get the tools you
expect, just some unfinished pieces lying around.
Thanks, that's good to know. I must have overlooked this advice in the
Isabelle tutorial as I don't recall hearing it before.
Hope this helps...
Yes, your email was very helpful. I was able to get the proof to go through
and learned a bit about how it works in the process. I hope to send a
follow up email soon, as I have a few more questions now. I'm a bit short on
time at the moment so it may not be till the new year.
Thanks,
Jason
Last updated: Nov 21 2024 at 12:39 UTC