*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>, isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] [SPAM: 3.000] Re: Parametricity for functions which ignore arguments*From*: Andrei Popescu <A.Popescu at mdx.ac.uk>*Date*: Wed, 22 Jun 2016 17:04:28 +0000*Accept-language*: en-GB, en-US*Authentication-results*: spf=none (sender IP is ) smtp.mailfrom=A.Popescu@mdx.ac.uk;*In-reply-to*: <576AB781.1050809@inf.ethz.ch>*References*: <57679DD5.4080504@inf.ethz.ch> <AM3PR01MB1313F01B1AE4F2D350A24B43B72A0@AM3PR01MB1313.eurprd01.prod.exchangelabs.com>, <576AB781.1050809@inf.ethz.ch>*Spamdiagnosticmetadata*: NSPM*Spamdiagnosticoutput*: 1:99*Thread-index*: AQHRysc6mcyMlm7pskKmpH3eyVNDhJ/yjB38gAMeYYCAAAtrww==*Thread-topic*: [SPAM: 3.000] Re: [isabelle] Parametricity for functions which ignore arguments

Hi Andreas, Much nicer! Btw, we could have axiomatized BNFs using a version of your axioms (plus the bound) and then defined the set structure from the relator structure: definition set_G :: "'a G ? 'a set" where "set_G x = {a . ALL P. rel_G (% a1 a2. a1 = a2 & P a1) x x ? P a}" Andrei ________________________________ From: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> Sent: 22 June 2016 17:06 To: Andrei Popescu; isabelle-users Subject: [SPAM: 3.000] Re: [isabelle] Parametricity for functions which ignore arguments Dear Andrei, Thanks for the idea of using map_G (%_. True) and map_G (%_. False). Rather than going for a contradiction and using set_G, I can derive from this that rel_G (%_ _. False) (foo x f) (foo x f) and thus "rel_G B (foo x f) (map undefined (foo x f))" by monotonicity. That's enough to show the rest. 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'" I am not sure how much they differ from the BNF requirements, but at least I don't need a set function (and certainly no bound). 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 >

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

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

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

- Previous by Date: Re: [isabelle] Parametricity for functions which ignore arguments
- Next by Date: [isabelle] Specification.definition: Getting theorem for Const, not Free?
- Previous by Thread: Re: [isabelle] Parametricity for functions which ignore arguments
- Next by Thread: Re: [isabelle] Malformed dependency error with overloading
- 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