[Prev][Next][Index][Thread]

Re: Query: implicit recursion



Date: Wed, 15 Mar 89 15:11:08 CST

>	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 initial [final]?"

The answer to this question depends on exactly how it is 
formulated.  Here are some results.
	1)  Let (S, Sigma) be a finite single-sorted signature.  It
determines a polynomial endofunctor T : PER -> PER whose initial
algebra I satisfies:
	a)  I is the initial algebra for the signature
	b)  I = (all C).[[T(C) -> C] -> C]
	c)  I = Dinat([[T(C) -> C] -> C])
	d)  I = StrongDinat([[T(C) -> C] -> C])
In this case, I, the product of all values of [[T(C) -> C] -> C], the 
collection of all dinatural transformations from [T(C) -> C] to C,
and the collection of all strong dinatural transformations from
[T(C) -> C] to C are the same.  (Cameron Smith, thesis 1988, UIUC)

	2)  Let CCC be a cartesian closed category in which 1 is a
generator and let T be an endofunctor of CCC.  If
	i)  There is an initial T-algebra, and
	ii) There is a strong dinatural transformation 
		[T(C) -> C] -> [I -> C]
	which assigns to any global section of [T(C) -> C] (i.e., to any
	T-algebra) the unique induced morphism from the initial T-algebra I
	to C, 
then  I = StrongDinat([[T(C) -> C] -> C]).  (Gray and Smith, to appear)

The result 2 is actually very simple, but the conditions in 2 can be 
verified in categories of domains (as well as in PER) for suitable (e.g., 
cocontinuous) endofunctors T, so 2 is very useful.  It is
doubtful that 
	StrongDinat([[T(C) -> C] -> C])  =  (all C).[[T(C) -> C] -> C]
except in PER.

Notice that this does not answer the question as to when one of the
right hand sides in 1b, 1c, or 1d can be used to show that an initial
algebra for T exists for a general category CCC.

	John W. Gray