Like other works I’ve encountered by this author [1,2,3], this book is characterized by consummate logico-mathematical rigor, coupled with commensurate expository and pedagogical merit. Rigor is certainly a necessary attribute of real theory of computation books, but those books, unlike this one, lack additional motivational, annotational, metaphoric, and even humorous material. Use of the pejorative term “rigor mortis” [4] is often contextually and provisionally justified among physicists and their fellow travelers, but here it is emphatically the case that The Proof’s the Thing. (The Shakespeare allusion is mine.)

The late mathematician Lipman Bers stated that “all mathematicians are Platonists, whether they admit it or not.” Though I personally go only as far as regarding this assertion as a psychological truth, Bers’ assertion serves to provide context and contrast for conveying a great strength of this book: its theoretical and pedagogical handling of abstraction. The following statement in the preface illustrates the author’s perspective:

We apply this principle: Before the student studies the (meta)theory, he must have attained a good grasp of the practice that this theory attempts to dissect and discuss. Thus, it is natural to start our story with the (meta)theory of general-purpose computer programs.

(Emphases are the author’s, and “he” is posited to stand for “he or she” throughout the book. The author also states, in good humor, that it is the metatheory of computation that is being treated, but that common usage has dictated his compromise in titling his book.) The oft-neglected path from concrete to abstract is given its due in this book, to great pedagogical--and I daresay philosophical--effect. Ditto regarding the nature and role of axioms. Here is the author, in a footnote: “Induction is not a provable principle [... ,] it is an axiom. However, this will not stop us from arguing its plausibility.”

The choice of unbounded register machines (the URMs of Shepherdson and Sturgis) as one of the main models of computation and as abstractions of general-purpose (high-level language) computing is a tour de force. Turing machines (TMs) are by no means ignored, but are quite aptly (and respectfully) regarded as models of computation at the assembly-language level.

There are five chapters, of which the second, and longest, treats computation theory proper. The chapters are “Mathematical Foundations,” “Algorithms, Computable Functions and Computations,” “A Subset of the URM Language: FA [Finite Automata] and NFA [Nondeterministic FA],” “Pushdown Automata [PDA],” and “Computational Complexity.” The author’s “special attention to correctness of exposition” pervades the entire book, and is in line with his previous works [1,2,3]. There is, however, evidence, especially in chapter 1, that some final editing may have been relegated to automatic means, or may have been a mite too quick. For example, many instances of “intention” should have been “intension.” A bound variable is, once in a while, missing from a quantifier. The second negation is missing from some examples of De Morgan’s laws. And the sum of a triangle’s angles is pi, not two pi. As the target audience comprises advanced undergraduates and up, these are harmless.

The discussion of bound versus free variables is the clearest I’ve seen, and “x = x is not a tautology” is not for shock value, but is emblematic of appropriate rigor and formality. The treatment of logical versus non-logical axioms is superb, as is the discussion of the axiom of choice. The explication of (Cantor) diagonalization sets the stage for its use throughout the book. Chapter 2 treats Hilbert’s decision problem. Minimal lambda-calculus is used very effectively in this and subsequent chapters. The treatment of primitive recursive functions is very theoretical, but is indispensable and should not be speed-read. The Meyer-Ritchie loop programming model of computation is presented as another high-level alternative to Turing machines. The pauses are delightful and enlightening: “Why not forget about these acrobatics and just rest the case ... above?” Church’s thesis is explicated in the clearest possible way. The author states early in the book that ZFC (Zermelo-Fraenkel with choice) is the set theory he is using (naively). “The selection theorem is a computable version of the Axiom of Choice.” Gödel’s First Incompleteness Theorem is one climax of the book.

The routine use of the lambda calculus, Gödel-like encoding, and diagonalization is a strength that enables incremental, almost osmotic, learning. The last three chapters are applications and extensions of the theory so expertly and thoroughly treated in the first half of this excellent book. I guarantee that you’ll learn something new from them, whoever you are. This is an outstanding book, and I recommend it highly to students and practitioners alike.