*To*: Andrei Popescu <A.Popescu at mdx.ac.uk>, isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Parametricity for functions which ignore arguments*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Wed, 22 Jun 2016 18:06:25 +0200*In-reply-to*: <AM3PR01MB1313F01B1AE4F2D350A24B43B72A0@AM3PR01MB1313.eurprd01.prod.exchangelabs.com>*References*: <57679DD5.4080504@inf.ethz.ch> <AM3PR01MB1313F01B1AE4F2D350A24B43B72A0@AM3PR01MB1313.eurprd01.prod.exchangelabs.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.8.0

Dear Andrei,

rel_G (%_ _. False) (foo x f) (foo x f)

My proof needs the following five properties of rel_G: "rel_G op = = op =" "âR f x y. rel_G R (map_G f x) y = rel_G (Îx. R (f x)) x y" "âR f x y. rel_G R x (map_G f y) = rel_G (Îx y. R x (f y)) x y" "âR R' x y. R <= R' â rel_G R <= rel_G R'" "âR R'. rel_G (R OO R') = rel_G R OO rel_G R'"

Cheers, Andreas On 20/06/16 18:41, Andrei Popescu wrote:

Hi Andreas, I guess the question is weird enough to require my competence. ð I think your intuition is correct, and the fact that G is a BNF is helpful. AFAIS, the missing hole in your argument can be filled if you prove that, (1) for a fixed type K and a unary BNF G, any function u : (K -> 'a G) -> 'a G that is both constant (i.e., ignores its arguments) and 'a-parametric has it's image consisting of an element y with no a'-atoms, i.e., such that Gset y = {} (2) For any BNF G, any element y with no atoms is G-related to itself, i.e., Grel R y y holds for any relation R on 'a. Now, (1) should follow by contradiction: assume otherwise, and use the parametricity of u for the graphs of the functions (% a. True) and (%a. False) to contradict that u is constant. (2) should follow using the connection between Grel and Gset, via Gmap. Andrei ------------------------------------------------------------------------------------------ *From:* cl-isabelle-users-bounces at lists.cam.ac.uk <cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> *Sent:* 20 June 2016 08:40 *To:* isabelle-users *Subject:* [isabelle] Parametricity for functions which ignore arguments Dear list, Dmitriy and I are struggling with a proof about parametricity of a constant in Isabelle/HOL. Suppose we have a natural functor 'a F and a parametric function foo bnf_axiomatization 'a F consts foo :: "'a F => ('a => 'c G) => 'c G" axiomatization where foo_param: "!!A. rel_fun (rel_F A) (rel_fun (rel_fun A (rel_G B)) (rel_G B)) foo foo" where 'b G is some type expression for which rel_G is the appropriate relator (G can be a BNF, too, if this helps in any way). Further, we know that for given x :: 'a F and y :: 'b F with "rel_F A x y", the function foo ignores its second argument, i.e., !!f g. foo x f = foo x g !!f g. foo y f = foo y g Can we deduce from all of the above that "rel_G C (foo x f) (foo y g)" for any f and g? And if so, how? Intuitively, the reasoning goes as follows. Parametricity expresses that foo cannot create values of type 'c out of nothing. By its type signature, it can only create such values by using the second argument. However, for the given arguments x and y, we know that foo x and foo y ignore their second arguments, so foo cannot create a value in 'c. That is, foo must return a value of type 'c G which does not contain any 'c values at all. Therefore, there exist values a and b such that rel_G C a b for any relation C. Hence, rel_fun A (rel_G C) (%_. a) (%_. b) and therefore foo x f = foo x (%_. a) `rel_G C` foo y (%_. b) = foo y g. Is there a flaw in our intuitive reasoning? If not, how could this be formally expressed in HOL? Best, Andreas

**Follow-Ups**:**Re: [isabelle] [SPAM: 3.000] Re: Parametricity for functions which ignore arguments***From:*Andrei Popescu

**References**:**[isabelle] Parametricity for functions which ignore arguments***From:*Andreas Lochbihler

**Re: [isabelle] Parametricity for functions which ignore arguments***From:*Andrei Popescu

- Previous by Date: [isabelle] ITP 2016: Call for participation
- Next by Date: Re: [isabelle] [SPAM: 3.000] Re: Parametricity for functions which ignore arguments
- Previous by Thread: Re: [isabelle] Parametricity for functions which ignore arguments
- Next by Thread: Re: [isabelle] [SPAM: 3.000] Re: Parametricity for functions which ignore arguments
- Cl-isabelle-users June 2016 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