Re: [isabelle] polymorphic enough friend



Hi Thomas,

> another question on corecursion and friends in Isabelle/HOL development
> version 6703434c96d6:
> In theory 'Foo' below I am able to show that function "some" which
> depends on an inductive set "A" is friendly but when I try to do the
> same for function "some'" defined similarly but depending on the
> inductive set "C X" instead, I get the error message:
> 
> "Eps" not polymorphic enough to be applied like this and no friend
> 
> I'm not quite sure why the former works whereas the latter fails.
> Maybe someone besides Jasmin is able to answer this one?

At the heart of "corec" and friends is a procedure we call "surface synthesis". It is described in our paper draft "Friends with Benefits" (found e.g. on my home page).

That synthesis is difficult to explain, but in short, if it succeeds, you still have to prove parametricity of whatever polymorphic constants in ran along the way. And I can already guarantee you that you will not succeed at proving "Eps" parametric, because it is not. (In general, underspecification is a killer for parametricity.)

Cheers,

Jasmin





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