Half tiers and linear space (and time)

James Otto

(A slightly longer version of this note is linked to our web page cited below.)

We conjecture a fibrational reformulation of our categorical reformulation [thesis.ps.gz + update, see cited web page below] of the Bellantoni-Ritchie characterization of the linear space functions. (In the longer version, we also mention the linear time functions on multi-tape machines. We characterized these in [thesis.ps.gz].) This sets up for conjectures such as one for characterizing Nlog space relations using Boolean arrays as `finite models' and quantification over arrays of choices. (Actually, D. Leivant is also writing up finite models as Boolean arrays results and M. Hofmann's use of gluing will likely allow us to prove things.) We have characterized the linear space functions as the image in set^2 of an initial category. In set^2 we took terminal and identity maps N0 = (- : N ---> 1) and N1 = (id : N --> N) to be (in D. Leivant's terminology) tier 0 and tier 1 numbers. Now we replace the category set^2 by the chain of fibrations

                      d0           d0
               set^3 -----> set^2 -----> set
Then we have the half tiers of numbers N0 = (N --> 1 --> 1), N.5 = (N --> 1), and N1 = N in the categories set^3, set^2, and set. We introduce tier .5 as each of a chain --> --> of fibered FP (i.e. having fibered finite products) locally small fibrations adds 1 to the possible rank of higher types and as we wish a recursor R : N1 --> ((N0^2)^(N0^2))^((N0^2)^(N0^2)). We conjecture that the linear space functions are the image in d0 : set^3 --> set^2, d0 : set^2 --> set (with set^3, set^2 forgotten) of the initial chain of fibrations
                      p             p
              C^(0) -----> C^(.5) -----> C^(1)
among chains of fibrations restricted as follows. The categories C^(j) are FP (i.e. have finite products). The fibrations p : C^(j) --> C^(j+.5) are fibered FP and locally small. In the fiber in C^(0) over 1 in C^(.5) there is a sum cocone
                       0          s
                   1 -----> N0 <----- N0
stable under product and instance. Finally, there is weak safe recursion as in the longer version of this note.

James Otto

507 North Dunton Avenue, Apartment 427
Arlington Heights
IL 60004-5941
Email: otto@triples.math.mcgill.ca
Home page: ftp://triples.math.mcgill.ca/pub/otto/otto.html

Back to the list of talks