Theory of Computation

2.2  A PROGRAMMING FORMALISM FOR THE PRIMITIVE RECURSIVE FUNCTIONS

Loop programs were introduced by Meyer and Ritchie (1967) as a program-theoretic counterpart to the number-theoretic introduction of the set of primitive recursive functions . This programming formalism is analogous to the URM formalism, but, unlike the latter, it corresponds—i.e., is able to “compute” —precisely the primitive recursive functions. It also provides a connection between the definitional (or structural) complexity of primitive recursive functions—that is, the complexity of their syntactic definition—with their (run time) computational complexity as we show in Chapter 5.

Loop programs are very similar to programs written in the old programming language FORTRAN, but have a number of simplifications—notably, they lack an unrestricted do-while instruction (equivalently, they lack a goto instruction).

While we have an infinite supply of (program) variables, each loop program—being a finite string—references (uses) only a finite number of variables. We will most often denote variables metamathematically by single letter names (upper or lower case is all right) with or without subscripts or primes.⁶³

Let us define by induction (cf. 1.6.0.12), at first somewhat loosely, the structure (syntax) of loop programs. ...