[Prev][Next][Index][Thread]
Implicit Recursion
Date: Tue, 14 Mar 89 15:03:50 GMT
>Forwarding to types@theory.lcs.mit.edu from gavinw%uk.ac.sussex.syma
IMPLICIT RECURSION IN THE POLYMORPHIC LAMBDA CALCULUS
Gavin Wraith
Department of Mathematics
University of Sussex
13/3/89
If A(X) is a type expression in poly-\ that is covariant in the
type variable X (upper case for types, lowercase for values),
then it is fairly well known that !X.(A(X)->X)->X is a weak
initial A-algebra. To be more explicit, let
def : I = !X.(A(X)->X)->X
Here ! stands for A standing on its head.
def : phi = \X.\f:A(X)->X.\w:I.w X f : !X.(A(X)->X)->I->X
def : eps = \h:A(I).\X.\f:A(X)->X.f (A(phi X f) h) : A(I)->I
Then for any A-algebra f : A(T)->T we have the term
y=(phi T f) : I->T and eps;y => A(y);f.
So we can say that the 'recursive equation' eps;y=A(y);f has an
explicit (least fixed point) solution. For example
if A(X) = 1+Y*X (so that I=list(Y)) then phi=listrec.
What seems to be less well known is that, dually, we can construct
weakly terminal coalgebras, as follows:
Def : F = !Y.(!X.(X->A(X))->X->Y)->Y
where Y does not occur as a free type variable in A(X) and X occurs
covariantly (in fact F=EX.X*(X->A(X)) where E stands for existential
quantifier).
def : psi = \X.\f:A(X).\x:X.\Y.\h:!Z.(Z->A(Z))->Z->Y.h X f x
so that psi : !X.(X->A(X))->X->F,
def : eta = \w:F.w A(F) (\X.\f:X->A(X).\x:X.A(psi X f) (f x))
so that eta : F->A(F). Then given an A-coalgebra f:T->A(T), if we
define y = (psi T f) : T->F we get
y;eta => f;A(y)
So for example, if A(X)=X*Y (so that F=stream(Y)) we get psi=streamrec.
In summary, poly-\ already contains a lot of implicit recursion, i.e.
that which is definable by equations of the forms
eps;y = A(y);f
or y;eta = f;A(y)
for A( ) covariant. Explicit fixpoint (least for alg-type, greatest
for coalg-type) operations are not needed for them.
Gavin Wraith 13/3/89