Email Gateway (Aug 22 2022 at 13:38): Email Gateway (Aug 22 2022 at 13:38):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Email Gateway (Aug 22 2022 at 13:38):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Hi Andreas,
I guess the question is weird enough to require my competence. [:blush:]
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
OutlookEmoji-😊.png
Email Gateway (Aug 22 2022 at 13:38):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Last updated: May 07 2024 at 01:07 UTC