Re: [isabelle] Quotients and code generation for higher-order functions



Dear Wenda, dear experts of the code generator and lifting/transfer,

I have been able to reduce my problem further. Suppose that we have an infinitely branching tree, say

  datatype 'a tree = Leaf 'a | Node "nat => 'a tree"

and an equivalence relation rel on tree which is a congruence for Node. We take the quotient and lift the Node constructor:

  quotient_type 'a qtree = 'a tree / rel
  code_datatype abs_qtree
  lift_definition NODE :: "(nat => 'a qtree) => 'a qtree"

Now, the question is, what is a suitable code equation for NODE?

I do not know an answer myself. For a finitely branching tree (say we replace "nat" with "bool"), I could use an isomorphic first-order constructor such as Node' :: 'a tree => 'a tree => 'a tree to derive the code equation. But for infinitely branching trees, I have run out of ideas.

Andreas

On 25/07/15 17:03, Wenda Li wrote:
Dear Andreas,

Many thanks for your patience and comprehensive explanations, I now do realize my previous
mistakes. My current impression is that, given a term

   Go (Îx. bind (c x) f)

"bind (c x) f" is of type foo. If "f" is of type "'a => 'b bar", we have to find a mapping
of type "bar => foo" somehow and somewhere, which leads directly to the problem you were
talking about. Therefore, it seems that the problem is really about the function "f" of
type "'a => 'b bar".

A workaround may be to let "f" be of type "'a => 'a foo". That is,

   lift_definition bind_bar :: "'a bar â ('a â 'b foo) â 'b bar" is bind sorry

should have it code equations directly.

Let me know if there is any other solutions. I am really interested in this topic :-)

Best,
Wenda

On 2015-07-24 13:16, Andreas Lochbihler wrote:
Dear Wenda,

code_abstype and code abstract are normally used for types carved out
as a subset of some other type. For rat, e.g., the subset consists of
all the relatively prime pairs of integers where the second component
is positive. Although rat is constructed as a quotient from pairs of
integers, the code generator setup considers rat as isomorphic to the
subset of pairs described in the previous sentence, i.e., we have
carved out a subset. All code equations ensure that only such
normalised pairs occur at run-time, i.e., we have canonical
representatives. Conversely, the code equations can exploit that
rational numbers given as arguments are always normalised.

With code_datatype, you do not need canonical representatives. In
fact, you cannot even exploit them. As the code equations
pattern-match on the pseudo-constructors, all elements in the domain
of the pseudo-constructor are considered valid representations. Thus,
you cannot rely in the code equation on any invariant. For
pseudo-constructors, the challenge lies in defining the functions on
the abstract type such that the desired code equation is provable.

lemma [code]:"bind_bar (abs_bar x) f = abs_bar (bind x (Îu. rep_bar (f u)))" sorry

If we declare code_datatype abs_bar, then we can use this lemma as a
code equation. However, we also must provide a code equation for
rep_bar. Obviously, we would like to have the following equation

  rep_bar (abs_bar x) = x

However, this equation expresses that abs_bar does not discard any
information in x, i.e., abs_bar is injective. As bar is a
(non-trivial) quotient of foo, abs_bar clearly is not injective, as it
maps every x to the equivalence class of x. In fact, we cannot define
any function f such that f (abs_bar x) = x. Thus, we cannot find any
such unpacking function rep_bar at all. The only reason giving me some
hope in the case above is that ultimately, we are applying abs_bar on
the right-hand side again, i.e., we are ultimately throwing away all
the extra information contained in the raw type.

Best,
Andreas

PS: As bar is a quotient of foo, we know that "abs_bar (rep_bar x) =
x", but this kind of equation is only suitable for code_abstract,
which requires canonical representatives.


On 24/07/15 13:38, Wenda Li wrote:
Dear Andreas,

Thanks for reminding me of the non-canonical representation, I will have a similar issue
in my formalization :-) However, in my understanding, a canonical representation is
important when using "code abstype"/"code abstract" to restore executability (e.g. Rat.thy
Polynomial.thy), while with "code_datatype" it seems that we can deal with executability
in a more flexible way (e.g. Real.thy).

In this case, if we can prove

lemma [code]:"bind_bar (abs_bar x) f = abs_bar (bind x (Îu. rep_bar (f u)))" sorry

we should be able to evaluate

value "bind_bar (abs_bar (Stop (1::nat))) (Îu. abs_bar(Stop (u+2)))"

value "bind_bar (abs_bar (Go (Îx::nat. Stop (x+2)))) (Îu. abs_bar(Stop (u+2)))"

Please correct me if I am wrong at any point.

Wenda

On 2015-07-24 12:14, Andreas Lochbihler wrote:
Hi Wenda,

On 24/07/15 13:05, Wenda Li wrote:
lemma [code]:"bind_bar (abs_bar x) f = abs_bar (bind x (Îu. rep_bar (f u)))" sorry

Can you prove this in your theory?
Of course, this type-checks and is provable. However, I'd need a code
equation for rep_bar in the form "rep_bar (Abs_bar x) = ...". And for
this, I'd need a notion of canonical representative in the raw type,
which I don't have at the moment. It would require a lot of work (in
Isabelle) to define such a notion. Moreover, the generated code would
have to transform everything into the normal form, which can be
computationally prohibitive.

Best,
Andreas

On 2015-07-24 07:51, Andreas Lochbihler wrote:
Dear all,

I am currently stuck at setting up code generation for a quotient
type. To that end, I have declared an embedding from the raw type to
the quotient type as pseudo-constructor with code_datatype and am now
trying to prove equations that pattern-match on the
pseudo-constructor. There are no canonical representatives in my raw
type, so I cannot define an executable function from the quotient type
to the raw type.

I am stuck at lifting functions in which the quotient type occurs as
the result of higher-order functions. The problem is that I do not
know how to pattern-match on a pseudo-constructor in the result of a
function. Here is an example:

  datatype 'a foo = Stop 'a | Go "nat â 'a foo"

  primrec bind :: "'a foo â ('a â 'b foo) â 'b foo" where
    "bind (Stop x) f = f x"
  | "bind (Go c) f = Go (Îx. bind (c x) f)"

  axiomatization rel :: "'a foo â 'a foo â bool" where rel_eq: "equivp rel"
  quotient_type 'a bar = "'a foo" / rel by(rule rel_eq)
  code_datatype abs_bar

  lift_definition bind_bar :: "'a bar â ('a â 'b bar) â 'b bar" is bind sorry

My problem is now to state and prove code equations for bind_bar. Obviously,

  lemma "bind_bar (abs_bar x) f = abs_bar (bind x f)"

does not work, as bind expects f to return a foo, but f returns a bar.
My next attempt is to inline the recursion of bind. The case for Stop
is easy, but I am out of ideas for Go.

  lemma "bind_bar (abs_bar (Stop x)) f = f x"
        "bind_bar (abs_bar (Go c)) f = ???"

Is there a solution to my problem? Or am I completely on the wrong track.

Thanks for any ideas,
Andreas







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