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.