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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.