Re: [isabelle] Code generation for inductive predicates



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:
> 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
>     *}
>
>   






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.