Eta Rules

Date:     Thu, 16 Mar 89 15:07:58 GMT
>forwarding from gavinw-FdWlMGuy5EqpwOz6WmuLTfd9D2ou9A/h@xxxxxxxxxxxxxxxx

-------- ETA RULES IN POLYMORPHIC LAMBDA CALCULUS ---------

In reply to Nax Mendler's query whether the weakly initial algebras
!X.(A(X)->X)->X [weakly final coalgebras !Y.(!X.(X->A(X))->X->Y)->Y ]
are necessarily initial [final] :

It all depends on what you mean by a model of poly-\calc. Consider
the case when A(X) = 0 (supposing we have a model with an initial
object). Then poly-0 is !X.X for which we have the identity map
given by the term

           \x:(!X.X).x : (!X.X)->(!X.X)   .

However we also have a map given by the term

          \x:(!X.X).(x (!X.X)) : (!X.X)->(!X.X)

so that if poly-0 is to be genuinely initial these two terms must
be identified in the model. This is part of a general phenomenon
and corresponds to an eta-rule for initial objects. The eta rule
for I = !X.(A(X)->X)->X says, in the notation of my earlier
message, that \x:I.x and (phi I eps) should be identified. The
eta rule for F = !Y.(!X.(X->A(X)->X->Y)->Y says that \x:F.x and
(psi F eta) should be identified (please excuse the accidental
overloading of my use of 'eta' !). I would claim that these
identifications are a necessary part of the notion of model.
I believe, but do not know how to prove, that in the Tannen-
Coquand 'minimal' model we get genuine initiality [finality].
Of course the eta rules are necessary for genuine
initiality [finality] but I doubt whether they are sufficient.
For !X.X, for example, we want to know that ALL maps of
type (!X.X)->(!X.X) are the identity, whereas our eta rule just
identifies those which are \-definable (evidence that 'term models'
may be OK).
For initiality of I = !X.(A(X)->X)->X we need the following:

Given terms f:S->T, c:A(S)->S, q:A(T)->T such that A(f);q and
c;f are identified in the model, then

       f;(phi T q)  and  (phi S c)

are identified in the model. This is a xi-rule (there is an
evident dual rule for coalgebras) corresponding to the rule

         case(u v);f == case((u;f) (v;f))

for sums and

         f;pair(u v) == pair((f;u) (f;v))

for products.


Gavin Wraith
Sussex University