[Prev][Next][Index][Thread]
implicit recursion
Date: Wed, 5 Apr 89 16:09:52 JST
Return-Path: <ryu@kurims.kurims.kyoto-u.ac.jp>
> IMPLICIT RECURSION IN THE POLYMORPHIC LAMBDA CALCULUS
>
> Gavin Wraith
> From: nax@gvax.cs.cornell.edu (Nax)
> ". . . is there a non-trivial sufficient
> condition on models (better, a characterization) for when
> these constructions are intial [final]?"
In my master thesis, I studied such a problem on PL categories and obtained
a sufficient condition, relating to parametric polymorphism.
In a category with a terminal object 1, any arrow k:A->B can be considered
as representing a relation of A*B, that is, a:1->A relates to b:1->B
under k if and only if a;k = b. This is naturally extended to S(k) for any
multivariate endofunctor S(X-,X+), viz., a:1->S(A,A) relates to b:1->S(B,B)
under S(k) if and only if a;S(1,k) = b;S(k,1) :1->S(A,B).
I will state the definition of parametricity informally.
Let T(X-,X+) be another endofunctor. An arrow t:S->T over X is
called parametric if, for any A and B, and k:A->B, that a relates to b
under S(k) implies that a;t(A) relates to b;t(B) under T(k). This can be
taken for a categorical interpretation of Reynolds' parametricity, which
was originally defined on a set model.
In the thesis above, a parametric condition on PL categories is proposed,
and under it, it is showed, that (AX).(T(X)->X)->X is an initial T-algebra
where A stands for a universal quantification and T(X) is a positive
endofunctor, that some logical encodings, 0 = (AX).X,
A+B = (AX).(A->X)->(B->X)->X, and (EX).T(X) = (AY).((AX).(T(X)->Y)->Y),
have appropriate categorical meanings, and also that (EX).(X->T(X))*X is
a final T-coalgebra.
Unfortunately I have not yet found any concrete models satisfying that
condition, and am serching for them.
Ryu Hasegawa
Kyoto University