[Prev][Next][Index][Thread]
Eta Rules
Date: Thu, 16 Mar 89 15:07:58 GMT
>forwarding from gavinw@uk.ac.sussex.syma
-------- 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