In this chapter we will develop a somewhat more general view of computability theory, where not only numbers and functions appear as arguments, but also functionals of any finite type.

Abstract computability via information systems

There are two principles on which our notion of computability will be based: finite support and monotonicity, both of which have already been used (at the lowest type level) in section 2.4.

It is a fundamental property of computation that evaluation must be finite. So in any evaluation of Φ(ϕ) the argument ϕ can be called upon only finitely many times, and hence the value—if defined—must be determined by some finite subfunction of ϕ. This is the principle of finite support (cf. section 2.4).

Let us carry this discussion somewhat further and look at the situation one type higher up. Let ℋ be a partial functional of type 3, mapping type-2 functionals Φ to natural numbers. Suppose Φ is given and ℋ(Φ) evaluates to a defined value. Again, evaluation must be finite. Hence the argument Φ can only be called on finitely many functions ϕ. Furthermore each such ϕ must be presented to Φ in a finite form (explicitly say, as a set of ordered pairs). In other words, ℋ and also any type-2 argument Φ supplied to it must satisfy the finite support principle, and this must continue to apply as we move up through the types.