Email Gateway (Aug 22 2022 at 14:57): Email Gateway (Aug 22 2022 at 14:57):From: Artur Gomes <gomesa@tcd.ie>
Hi there,
I've seen a few emails in this list's history, sent a couple years ago
regarding lexicographic termination order whilst using fun definitions in
Isabelle, but I couldn't find what I was looking for.
I'm implementing a Haskell application that transforms a few constructs
over an AST defined by myself. But I'm doing it recursively. The code is
translated with Haskabelle. I'd like to understand what is the
lexicographic termination order means as a way to evaluate my code.
Another question: is there any difference regarding proofs of lemmas
involving a function defined as "fun" or "function" or even "function
(sequential)"?
I'm following the "Defining Recursive Functions in Isabelle/HOL" material
(from Isabelle's pdfs), and I went from "fun" to "function (sequential)"
and "by pat_completeness auto", but could't find termination with
"lexicographic_order".
I'm really curious about this lexicographic termination, if there's
anything I could do in order to "fix" (if possible). That would probably
help me to lear more about my coding skills or at least to point out if the
desired result of my code is being implemented reasonably.
Moreover, what I'm expecting from Isabelle is to prove that my
implementation (in Haskell) is equivalent to someone else's theoretical
work. I'll probably be dealing with structural induction and recursion. If
anyone has any previous experience with this kind of work, can I ask you
for some suggestions and background material?
Best regards,
Email Gateway (Aug 22 2022 at 14:58):From: Tobias Nipkow <nipkow@in.tum.de>
Maybe this paper helps:
Lukas Bulwahn, Alexander Krauss, Tobias Nipkow.
Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
http://www.in.tum.de/~nipkow/pubs/tphols07.html
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 14:58):From: Lars Hupel <hupel@in.tum.de>
Hi Artur,
Another question: is there any difference regarding proofs of lemmas
involving a function defined as "fun" or "function" or even "function
(sequential)"?
as long as you prove termination after defining a function with
"function", the resulting simp and induct rules will be identical to
when you use "fun" (which proves termination automatically).
(NB, unless you now what you're doing, avoid plain "function" without
"(sequential)".)
I'm following the "Defining Recursive Functions in Isabelle/HOL" material
(from Isabelle's pdfs), and I went from "fun" to "function (sequential)"
and "by pat_completeness auto", but could't find termination with
"lexicographic_order".
Could you show us the function where the function package can't
automatically prove termination?
Cheers
Lars
Email Gateway (Aug 22 2022 at 14:58):From: Artur Gomes <gomesa@tcd.ie>
Hi there,
Thank you all for the replies. I'm attaching a minimal example
where termination isn't automatically proved.
Cheers,
MinimalExample.thy
Prelude.thy
Email Gateway (Aug 22 2022 at 14:58):From: Christian Sternagel <c.sternagel@gmail.com>
Hi Artur,
I did not have a close look and thus do not know what your functions are
supposed to do.
Anyway, your current definition does not terminate. Consider the
following call sequence, where "c" is not of the shape "ACom d Nil":
transf_MAct (ActCom c a)
~> myfun1 transf_MAct c a
~> transf_MAct (ActCom c a)
Even if this is solved (e.g., by dropping "f" from the second case of
"myfun1") you will have to look into what is called "congruence rules"
(see the documentation of the function definition package) in order to
handle the recursive call in the second case of "transf_MAct".
hope this helps,
chris
Last updated: Apr 26 2024 at 20:16 UTC