In this final chapter we focus much of the technical/logical work of previous chapters onto theories with limited (more feasible) computational strength. The initial motivation is the surprising result of Bellantoni and Cook [1992] characterizing the polynomial-time functions by the primitive recursion schemes, but with a judicially placed semicolon first used by Simmons [1988], separating the variables into two kinds (or sorts). The first “normal” kind controls the length of recursions, and the second “safe” kind marks the places where substitutions are allowed. Various alternative names have arisen for the two sorts of variables, which will play a fundamental role throughout this chapter, thus “normal”/“input” and “safe”/“output”; we shall use the input–output terminology. The important distinction here is that input and output variables will not just be of base type, but may be of arbitrary higher type.

We begin by developing a basic version of arithmetic which incorporates this variable separation. This theory EA(;) will have elementary recursive strength (hence the prefix E) and sub-elementary (polynomially bounded) strength when restricted to its Σ1-inductive fragment. EA(;) is a first-order theory which we use as a means to illustrate the underlying principles available in such two-sorted situations. Our aim however is to extend the Bellantoni and Cook variable separation to also incorporate higher types. This produces a theory A(;) extending EA(;) with higher type variables and quantifiers, having as its term system a two-sorted version T(;) of Gödel's T. T(;) will thus give a functional interpretation for A(;), which has the same elementary computational strength, but is more expressive and applicable.