Email Gateway (Aug 18 2022 at 18:22): Email Gateway (Aug 18 2022 at 18:22):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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. So far, I came up with
the following:
(* Identify the subset of the type that is of interest *)
typedef (open) 'a llist_fin = "{xs :: 'a llist. lfinite xs}"
morphisms llist_of_fin Abs_llist_fin
proof
show "LNil : ?llist_fin" by simp
qed
(* Setup the abstype *)
lemma llist_of_fin_Abs_llist_fin [simp, code abstype]:
"Abs_llist_fin (llist_of_fin xs) = xs"
by(rule llist_fin.llist_of_fin_inverse)
(* Define the abstract operation *)
definition list_of2 :: "'a llist_fin => 'a list"
where "list_of2 xs = list_of (llist_of_fin xs)"
(* Prove a new code equation for list_of that uses the abstract operation *)
lemma list_of_code [code]:
"list_of xs = (if lfinite xs then list_of2 (Abs_llist_fin xs) else undefined)"
by(simp add: list_of2_def Abs_llist_fin_inverse list_of_def Abs_llist_fin2_def)
Now, I am stuck at two problems:
list_of_code uses the abstraction function Abs_llist_fin, which the code
generator does not allow. But from the calling context, I know that all
assumptions are satisfied.
I have no idea how to state the code equations for list_of2. I would imagine
something like
"list_of2 (Abs_llist_fin LNil) = []"
"lfinite xs ==> list_of2 (Abs_llist_fin (LCons x xs)) = x # llist_of2
(Abs_llist_fin xs)"
I have been going in circles here for quite some time. Can someone point me in
the right direction how to do this? Do I have the right approach? Or is it
impossible in general?
Thanks in advance,
Andreas
Email Gateway (Aug 18 2022 at 18:23):From: Brian Huffman <brianh@cs.pdx.edu>
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,
Email Gateway (Aug 18 2022 at 18:23):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi Brian,
thanks for your ideas, they are much simpler and more elegant than what I had in
mind. I'll add it to the AFP when I update Coinductive the next time.
Andreas
Last updated: Apr 25 2024 at 01:08 UTC