Email Gateway (Aug 18 2022 at 13:22): Email Gateway (Aug 18 2022 at 13:22):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all,
I tried out code generation for inductive predicates, and wonder when
the generated code will terminate.
In the code below, I inductively formulate the reflexive, transitive
closure of a transition relation.
No I want code to enumerate all the words that lead from one state to
another. This works well
if there exists such words. However, if there exists no such word, the
generated code simply does not terminate.
This is the same for the predicate w_nempty, that checks whether there
exists a word between two given states.
So what happens here? When does the generated code terminate? And is
there a simple way to generate code for "w_nempty" that terminates?
Many thanks in advance for any hints,
Peter
-- "A transition relation"
inductive_set d1 :: "(nat * char * nat) set" where
"(1,CHR ''a'',2) : d1" |
"(2,CHR ''b'',2) : d1"
-- "Reflexive, transitive closure"
inductive word where
"word \<delta> q [] q" |
"[| (q,a,qh):\<delta>; word \<delta> qh w q' |] ==> word \<delta> q
(a#w) q'"
-- "Whether a word from q to q' exists"
inductive w_nempty where
"word \<delta> q w q' ==> w_nempty \<delta> q q'"
code_module test
contains
test1 = "word d1 1 _ 2"
test2 = "word d1 2 _ 1"
test3 = "%d q q'. w_nempty d q q'"
(*
test4 = "w_nempty d1 2 1" However, with this, code generation does
not terminate.
*)
-- "These behave as expected: "
ML {*
DSeq.pull (test.test1);
*}
ML {*
let val d = [(0,(#"a",1)), (1,(#"b",1))] in
test.test3 d 0 1
end
*}
-- "These does not terminate:"
ML {*
DSeq.pull (test.test2);
*}
ML {*
let val d = [(0,(#"a",1)), (1,(#"b",1))] in
test.test3 d 1 0
end
*}
Email Gateway (Aug 18 2022 at 13:22):From: Tobias Nipkow <nipkow@in.tum.de>
Hi Peter,
The simple answer is, that code generation for inductive definitions
yields a functional version of what Prolog would give you, except that
there is no unification, only matching. If you give your clauses to
Prolog, you should see the same (non)termination behaviour as in Isabelle.
Your example 2 does not terminate because there is no path from 2 to 1,
but there is an edge from 2 to 2 and thus a recursive call with 2 and 1
is made etc. The fact that you don't need to answer the same query twice
on the same branch is not part of a Prolog interpreter because you need
to tabulate your queries, which can be expensive. If you want it, you
want "tabled logic programming", which Isabelle does not (yet?) provide.
However, you are not the only one who would like this, and Stefan
Berghofer has recently provided a theory of tabled transitive closure,
which can be used for code generation to avoid nontermination where the
answer should be No. Unfortunately it did not quite make it into
Isabelle 2009, out any day now. But Stefan can send you a copy and it
should solve your problem. (It is a little bit involved because you
essentially need to prove that it suffices to consider paths without loops).
Tobias
Peter Lammich wrote:
Last updated: May 03 2024 at 04:19 UTC