*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>, isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Parametricity for functions which ignore arguments*From*: Andrei Popescu <A.Popescu at mdx.ac.uk>*Date*: Mon, 20 Jun 2016 16:41:40 +0000*Accept-language*: en-GB, en-US*Authentication-results*: spf=none (sender IP is ) smtp.mailfrom=A.Popescu@mdx.ac.uk;*In-reply-to*: <57679DD5.4080504@inf.ethz.ch>*References*: <57679DD5.4080504@inf.ethz.ch>*Spamdiagnosticmetadata*: NSPM*Spamdiagnosticoutput*: 1:99*Thread-index*: AQHRysc6mcyMlm7pskKmpH3eyVNDhJ/yjB38*Thread-topic*: [isabelle] Parametricity for functions which ignore arguments

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] Parametricity for functions which ignore arguments***From:*Andreas Lochbihler

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

- Previous by Date: Re: [isabelle] Malformed dependency error with overloading
- Next by Date: Re: [isabelle] Parametrized transfer rules with lift_definition
- Previous by Thread: [isabelle] Parametricity for functions which ignore arguments
- Next by Thread: Re: [isabelle] 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