Re: [isabelle] Code generator setup for lazy lists
On Wed, Sep 14, 2011 at 8:21 AM, Andreas Lochbihler
<andreas.lochbihler at kit.edu> wrote:
> Dear all,
> I am wondering how I can efficiently implement a conversion function list_of
> between the subset of finite lists from the type of possibly infinite lists
> (as defined in AFP-Coinductive) and ordinary lists from the HOL image.
> At present, the code equations for list_of are as follows in the AFP:
> list_of LNil = 
> list_of (LCons x xs) = (if lfinite xs then x # list_of xs else undefined)
> This way, the finiteness test is executed once for every element of the
> list, which makes conversion quadratic in the length of the list. Now, I
> would like to execute the finiteness test at most a constant number of times
> by exploiting that finiteness is preserved through all recursive calls. I
> hope that I can do this with the code generator's support for invariants.
I have some suggestions that follow a different approach: Instead of
defining any new types or using invariants, you could just define an
auxiliary function to use with code generation for list_of.
My first idea was to define a variation of list_of that returns an
option type instead of using the "undefined" value:
definition opt_list_of :: "'a llist => 'a list option"
where [code del]: "opt_list_of xs = (if lfinite xs then Some
(list_of xs) else None)"
The code equations for opt_list_of are more efficient than the
standard ones for list_of, because they replace the expensive lfinite
test with a simple pattern match:
lemma opt_list_of_code [code]:
"opt_list_of LNil = Some Nil"
"opt_list_of (LCons x xs) =
(case opt_list_of xs of None => None | Some xs' => Some (x # xs'))"
unfolding opt_list_of_def by simp_all
Now you can declare a code equation for list_of so that it calls opt_list_of:
lemma list_of_code [code]:
"list_of xs = (case opt_list_of xs of None => undefined | Some xs' => xs')"
unfolding list_of_def opt_list_of_def by simp
My second idea is to define a function list_of_aux that uses an
accumulating parameter to store the list of elements seen so far:
definition list_of_aux :: "'a list => 'a llist => 'a list" where
"list_of_aux xs ys = (if lfinite ys then rev xs @ list_of ys else undefined)"
lemma list_of_aux_code [code]:
"list_of_aux xs LNil = rev xs"
"list_of_aux xs (LCons y ys) = list_of_aux (y # xs) ys"
unfolding list_of_aux_def by simp_all
lemma list_of_eq_list_of_aux [code]:
"list_of = list_of_aux "
unfolding fun_eq_iff list_of_def list_of_aux_def by simp
I suppose that list_of_aux is more efficient than opt_list_of, since
it is actually tail-recursive.
Hope this helps,
This archive was generated by a fusion of
Pipermail (Mailman edition) and