*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] Quotients and code generation for higher-order functions*From*: Wenda Li <wl302 at cam.ac.uk>*Date*: Sat, 25 Jul 2015 16:03:18 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <55B22C88.9070801@inf.ethz.ch>*References*: <55B1E06E.3060006@inf.ethz.ch> <d3865855c7dcfe2b15408c4d3329611f@cam.ac.uk> <55B21E31.40606@inf.ethz.ch> <ba23a31ac30b51d5b961462994fcf89f@cam.ac.uk> <55B22C88.9070801@inf.ethz.ch>*User-agent*: Roundcube Webmail/1.0.2

Dear Andreas,

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

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

should have it code equations directly.

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 (fu)))" sorryIf 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 willhave a similar issuein my formalization :-) However, in my understanding, a canonicalrepresentation isimportant when using "code abstype"/"code abstract" to restoreexecutability (e.g. Rat.thyPolynomial.thy), while with "code_datatype" it seems that we can dealwith executabilityin a more flexible way (e.g. Real.thy). In this case, if we can provelemma [code]:"bind_bar (abs_bar x) f = abs_bar (bind x (Îu. rep_bar (fu)))" sorrywe 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)))" sorryCan 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, AndreasOn 2015-07-24 07:51, Andreas Lochbihler wrote:Dear all, I am currently stuck at setting up code generation for a quotienttype. To that end, I have declared an embedding from the raw typetothe quotient type as pseudo-constructor with code_datatype and amnowtrying to prove equations that pattern-match on thepseudo-constructor. There are no canonical representatives in myrawtype, so I cannot define an executable function from the quotienttypeto the raw type.I am stuck at lifting functions in which the quotient type occursasthe result of higher-order functions. The problem is that I do notknow how to pattern-match on a pseudo-constructor in the result ofafunction. 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" isbind sorryMy 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 abar.My next attempt is to inline the recursion of bind. The case forStopis 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 wrongtrack.Thanks for any ideas, Andreas

-- Wenda Li PhD Candidate Computer Laboratory University of Cambridge

**Follow-Ups**:**Re: [isabelle] Quotients and code generation for higher-order functions***From:*Andreas Lochbihler

**References**:**[isabelle] Quotients and code generation for higher-order functions***From:*Andreas Lochbihler

**Re: [isabelle] Quotients and code generation for higher-order functions***From:*Wenda Li

**Re: [isabelle] Quotients and code generation for higher-order functions***From:*Andreas Lochbihler

**Re: [isabelle] Quotients and code generation for higher-order functions***From:*Wenda Li

**Re: [isabelle] Quotients and code generation for higher-order functions***From:*Andreas Lochbihler

- Previous by Date: [isabelle] New AFP article: Generating Cases from Labeled Subgoals
- Next by Date: [isabelle] AFP repository now on bitbucket
- Previous by Thread: Re: [isabelle] Quotients and code generation for higher-order functions
- Next by Thread: Re: [isabelle] Quotients and code generation for higher-order functions
- Cl-isabelle-users July 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list