Email Gateway (Aug 22 2022 at 10:39): Email Gateway (Aug 22 2022 at 10:39):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Email Gateway (Aug 22 2022 at 10:40):From: Wenda Li <wl302@cam.ac.uk>
Hi Andreas,
How about
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?
Best,
Wenda
Email Gateway (Aug 22 2022 at 10:40):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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_barlift_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
Email Gateway (Aug 22 2022 at 10:40):From: Wenda Li <wl302@cam.ac.uk>
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
Email Gateway (Aug 22 2022 at 10:40):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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.
Email Gateway (Aug 22 2022 at 10:40):From: Wenda Li <wl302@cam.ac.uk>
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
Email Gateway (Aug 22 2022 at 10:41):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Last updated: Apr 24 2024 at 08:20 UTC