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