Re: [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.


From: cl-isabelle-users-bounces at <cl-isabelle-users-bounces at> on behalf of Andreas Lochbihler <andreas.lochbihler at>
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?


PNG image

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