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.

Hi Andreas,

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,

- Brian





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