[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