[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