Re: [isabelle] [SPAM: 3.000] Re: 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
>



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