LOGICAL RELATIONS AND FEASIBILITY IN HIGHER TYPES

Abstract. We apply logical relations to define two hierarchies of functionals in all finite types as new candidates for higher type feasibility. The first hierarchy uses logical relations to generalize Cobham’s Limited Recursion on Notation to all finite types. The hierarchy coincides with Cook and Kapron’s Basic feasible Functionals (BFF) up to type level two, but at higher types our hierarchy might be strictly larger than BFF. The second hierarchy is defined by a generalized Kripke logical relation. The new point here is that the starting relations are not defined at base types, i.e. type level 0, but at types of any chosen level k. This requires a new construction of the relation for function types that in general differs from the usual one. The second hierarchy coincides with BFF up to type level k and is probably strictly larger at type level k + 1. We prove that if we work in the model of partial continuous functionals, all elements of our hierarchies are computable (which is not obvious for the second hierarchy). Both our hierarchies are closed under λ-definability. We neither know whether our hierarchies can be effectively generated nor how they are related in general