J Log Lang Inf (2008) 17:233–236 DOI 10.1007/s10849-007-9040-7 BOOK REVIEW

Book Review Hans-Jörg Tiede

Ganesh Gopalakrishnan, Computation Engineering: Applied Automata Theory and Logic, Springer, New York, NY, 2006, ISBN: 0387244182 As was pointed out in the preface of the third edition of Hopcroft and Ullman’s Introduction to Automata Theory, Languages, and Computation (now co-authored with Motwani) (Hopcroft and Ullman 2007), the subject matter of their book has undergone significant changes since the publication of its first edition in 1979 (Hopcroft and Ullman 1979). Among the changes they list are a shift in automata theory from an area of “direct research” to research related to applications and a shift of the material from the graduate to the undergraduate curriculum. Both of these have significantly affected how theoretical computer science is taught and how textbooks cover the material. However, during that time the core material itself has changed very little. It consists of the standard progression of language recognizers from finite automata, via pushdown automata, to Turing machines, with some detours to regular expressions and context-free grammars. Some books venture into computational complexity theory, some don’t. A common aspect of many books in this area is the lack of emphasis of the relationship between logic and automata/computability theory. This is unfortunate, since this relationship has been very important for the development of both subjects. Given that the logic/automata connection is increasing in importance due to applications in areas as diverse as linguistics (Moss and Tiede 2006; Rogers 1998) and hardware verification (Kropf 1999), textbooks that introduce logic and automata/computability theory together would be a very welcome addition. Although two of the, in the my opinion, best textbooks on this subject, that by Kozen (1997) and that by Sipser (2006), cover some applications of computability theory to logic, they do not cover the decidability of the monadic second-order theories of strings and trees (MSO), which play central roles in the logic/automata connection. A recent book by Khoussainov and Nerode (2001) is the only textbook, to the best of my knowledge, that discusses MSO, however,

H.-J. Tiede (B) Department of Mathematics and Computer Science, Illinois Wesleyan University, Bloomington, IL, USA e-mail: [email protected]

234

Book Review

it concentrates only on finite automata theory, and not other models of computing, and so is too narrowly focussed for an undergraduate introductory course. The book under review aims to “restore the Automaton-Logic connection missing in most undergraduate textbooks” (p. XXVII). It contains the following material. The first seven chapters cover background material, including sets, relations, logic, proof techniques, fixed-point theory, and strings and languages. This material takes up over a quarter of the book, which is certainly on the long side for a book aimed at advanced undergraduate or beginning graduate students. Its presentation is also very uneven; more on this below. The next five chapters are concerned with finite automata. The only “non-standard” topic covered here is a brief chapter on Binary Decision Diagrams as finite automata. After two chapters on context-free grammars and pushdown automata, three chapters are dedicated to Turing machines and undecidability proofs, including a proof of Church’s theorem on the undecidability of first-order logic. The next three chapters cover some meta-theory of propositional logic, a brief introduction to computational complexity theory, and proof of the decidability of Presburger arithmetic using finite automata. The book concludes with three chapters on model checking, which include a discussion Büchi automata and temporal logics. However, while MSO is mentioned in these chapters, its decidability is not covered here. As is apparent from the summary of the book’s contents, most of the material is that of a standard automata theory book. The only unusual material is that related to model checking, which, however, appears so late in the book that most undergraduate courses would not be able to cover that material without eliminating or rushing through several chapters. The sample syllabi listed in an appendix reflect this. There are two sample undergraduate syllabi: the one that covers the material on model checking simply covers all preceding chapters in fewer weeks. Most of the other material is already covered in Sipser’s book (2006), which does not suffer from the many defects listed below. Since computability has moved into the undergraduate curriculum, one of the aims of such a course is usually to teach students how to write mathematical proofs. Thus, an appropriate book should present proofs well, so that students have a good “role model”. To that end this book contains what must surely be one of the worst discussions of proof by contradiction, which is illustrated with a mistaken proof of Russell’s paradox. It begins by defining Russell’s set not with respect to a universal set, but with respect to some given set D: S = {x ∈ D | x  ∈ x}. At this point, any contradiction depends on the assumption that S ∈ D, which is not assumed. Thus, if S  ∈ D, no contradiction will result. While it is discussed later on that the Russell’s paradox implies that a universal set cannot exist, even then is the discussion mistaken, as it confuses membership with existence (p. 18): Now, if D were to be a set that contains “everything,” a set such as S must clearly be present inside D. However, we just argued that S must not exist, or else a contradiction will result. But even a universal set wouldn’t contain non-existent objects! The discussion concludes with the claim that Russell’s paradox is, in general, avoided by employing type theory, which is of course, in general, not true. Later in chapter 3, the difference between countable and uncountable sets is motivated by contrasting discrete and dense linear orders, claiming that the latter have

Book Review

235

to be of a “bigger infinity”. However, the rational numbers are densely ordered and countable. The book also frequently makes use of concepts before they are introduced. For instance, the just mentioned section on Russell’s paradox includes a demonstration that “it is essential to avoid contradictions in mathematics” in which the material conditional is used, while it is defined three chapters later. This makes the “proof” of Russell’s paradox is even less comprehensible. The relationship between finite automata, pushdown automata, and Turing machines are frequently cited as examples before any of them are defined. For instance, Sect. 4.3 defines an order relation on machine models, none of which have yet been defined. The incomplete, graphical representation of this relation is also just about maximally confusing. The relation is described as containing “(i) the pairs corresponding to the solid edges, (ii) the pairs indicated by the dotted edges, (iii) and those pairs indicated by those dotted transitive edges not shown” (p. 61). It left me wondering how to tell that the edges that are not shown are dotted. Following Barwise and Etchemendy’s groundbreaking Turing’s World program (1995), the use of software tools has had an important impact on the pedagogy of automata/computability theory. Unfortunately, frequently the author presents material related to software tools that are not really explained in the text. It also presents all algorithms in the programming language Ocaml without any explanation, which makes the book much less self-contained. Since computability theory developed together with logic in the 20th Century, it historically had significant ties to philosophical concerns. During its development within computer science, such philosophical concerns have been more and more de-emphasized, which is of course similar to the development of mathematical logic. However, this does not justify the hostility which is expressed early in the book under review (p. 2): The short answer is that we cannot have either a comprehensive or a permanent definition of what ‘computation’ means. Unless we employ the precise language offered by mathematics, philosophical or emotionally charged discussions are bound to lead nowhere. What is worse, no reason is given why such discussions are bound to lead nowhere, nor any references that can serve as examples of such discussions. One feels compelled to answer, with Kripke, that there is no mathematical substitute for philosophy. Furthermore, since Church’s thesis is concerned with an informal notion, that of intuitive computability, this dictum misses the point completely. It is a little surprising then that the author’s subsequent discussion of Church’s thesis is simply copied, with proper attribution, from the Stanford Encyclopedia of Philosophy. Although the author gives many useful references to important papers in the history of theoretical computer science, some dubious historical claims are made without giving any reference. For instance, on page 23, it is claimed in a footnote, without any reference, that Church’s response to the question why he chose λ as the function abstraction symbol was “Eenie meenie mynie mo!” This contradicts the account given by Rosser (1984), who states (p. 338) that the symbol was derived from Russell’s set abstraction operator: xˆ .1 1 On the other hand, Jonathan Seldin (p.c.) pointed out to me that Church himself didn’t remember it this way. Even so, the lack of reference to a source for Church’s quote and to Rosser (1984) are questionable.

236

Book Review

A final word on style. As the author warns in the preface (p. XXXV): A reader expecting to read “the usual theory book” is in for a surprise: they will find me joking about at various junctures, as I normally do when I lecture. Although humor is obviously a matter of taste, all I can say is that I found it to be very distracting and sometimes downright annoying. In addition to the jokes in the text, hand drawn cartoons can be found at the end of many chapter which usually consist of puns related to some of the concepts introduced. In conclusion this book unfortunately wastes, both in terms of style and substance, an important opportunity to change the direction in the teaching of automata theory and computability theory.

References Barwise, J., & Etchemendy, J. (1995). Turing’s World 3.0. Stanford, CA: Center for the study of Language and Information Publications. Hopcroft, J. E., & Ullman, J. D. (1979). Introduction to automata theory, languages, and computation. Reading, MA: Addison-Wesley Publishing Co.. Hopcroft, J. E., & Ullman, J. D. (2007). Introduction to automata theory, languages, and computation. Boston, MA: Pearson/Addison Wesley. Khoussainov, B., & Nerode, A. (2001). Automata theory and its applications. Boston, MA: Birkhäuser Boston Inc. Kozen, D. C. (1997). Automata and computability. New York: Springer. Kropf, T. (1999). Introduction to formal hardware verification. Berlin: Springer. Moss, L. S., & Tiede, H.-J. (2006). Applications of modal logic in linguistics. In Blackburn, P., van Benthem, J. & Wolter, F (Eds.), Handbook of modal logic. Amsterdam: Elsevier. Rogers, J. (1998). A descriptive approach to language-theoretic complexity. Stanford, CA: CSLI Publications. Rosser, J. B. (1984). Highlights of the history of the lambda-calculus. Annals of the History of Computing, 6(4), 337–349. Sipser, M. (2006). Introduction to the theory of computation (2nd ed.). Boston, MA: Thomson Course Technology.