A sequential CCC?

To: types@theory.LCS.MIT.EDU
Subject: A sequential CCC?
From: Andreas Knobel <ak%lfcs.edinburgh.ac.uk@nsfnet-relay.ac.uk>
Date: Tue, 20 Jun 89 12:03:14 EDT
Sender: meyer@theory.LCS.MIT.EDU

Date: Tue, 20 Jun 89 16:33:28-0000

I tried to generalize the notion of sequential function and came up with
the definition below. Unfortunately it does not exclude the (counter)
examples Pierre-Louis Curien mentions in his monograph (e.g. the function
g minimal such that g(lor) = t and g(ror) = f), so I stopped working on
it. Recently however I think (think = you can never be sure with so many
indices floating around) I proved that the category is Cartesian closed.

SeqAlg II is the category with

objects <P,I,|.|> where

     P is a partial order

     I is a set (of indices or information quanta or something)

     |.|  :  P --> 2^I  is a monotone function which, for every p in P,
     gives the information required to calculate it

morphisms <f,{s_x}_x in P>  :  <P,I,|.|> --> <P',I',|.|'> where

     f  :  P --> P'  is a continuous function

     {s_x}_x in P  is a set of partial functions indexed by P with
     s_x  :  I' \ |f(x)|'  -->  I \ |x|
     
f and {s_x}_x in P are connected in the following way:
             
     s_x is defined at i in I' \ |f(x)|' iff there is a y > x
     such that i in |f(y)|'  
  
     and

     for all y > x : if i in |f(y)|' then s_x(i) in |y|


A function is sequential if it is the input-output-function of some
sequential algorithm.

Products are < P x P' , I + I' , |.| + |.|' >, exponentials are somewhat
harder and quite messy to define.

Take for example as the Booleans the object B = < {t,f,bot},{*},|.| >.
Then por can evidently not be calculated by a sequential algorithm since
it lacks an index function s_<bot,bot>.

Andreas Knobel