“Procedural programming is a monumental waste of human energy” is a quotable polemic from coauthor Rex Page’s Web site. This point, if taken in the spirit in which it is given, is implicitly substantiated throughout this outstanding work. The book imparts much more powerful and fundamental material to the active and diligent reader, however, and without any polemics. I dare say that most of us have seen the risk in involving the use of a computer for study or for work: the computer, and particularly the idiosyncrasies of its user environment, becomes the issue, and the focus of attention. We soon forget why we logged on in the first place. The “using a computer” part of the title gave me that initial, prereading sense of unease.

This trepidation turned out to be totally unfounded; the functional programming language Haskell, in the authors’ hands, is the perfect vehicle to teach and experience the core concepts of discrete mathematics, including such deep and ultra-theoretical topics as the halting problem. And the instructions for the no-cost downloading and use of the Haskell environment, and ancillary book-specific software tools, are easy and effective.

Part 1, “Programming and Reasoning with Equations,” is made up of five chapters: “Introduction to Haskell,” “Equational Reasoning,” “Recursion,” “Induction,” and “Trees.” The Haskell chapter introduces that functional language, and imparts immediately the essence and power of that species of language, where an equation is indeed an equation, not an assignment of an r-value to an l-value. This should, by all rights, be a revelation to procedural-only programmers.

Part 2, “Logic,” contains “Propositional Logic” (chapter 6) and “Predicate Logic” (chapter 7). This part is arguably the best introduction to the application of (what is called classical) logic that I have seen, and could be a very useful book by itself. For one, the authors devoted well-spent effort to contrasting semantic (truth-table), syntactic (natural-deduction), and axiomatic/algebraic (Boolean) methods. Second, the explication of meta-language and its meta-logical symbols |=, |-, and = (the semantic and syntactic turnstiles, and equality symbol), though present in most logic books, is well sequenced and paced, as is the explanation of the difference between meta-variables and propositional variables. A good gradual unfolding of the difference between semantic (|=) and syntactic (|-) turnstiles will prepare the student for understanding the philosophies underlying model-checking, with respect to theorem-proving formal methods (which are finally in rapid ascendancy). Haskell’s representation of the theorem (here stated in standard notation)

|- Q —> ((P & R) —> (R & Q) )

epitomizes Haskell’s expressiveness and power, via the Theorem type:

thm :: Theorem

thm =

  Theorem

    [ ]

    (Imp Q (Imp (And P R) (And R Q)))

This is run through a Haskell-based proof-checker (which accompanies the book via free download), and the validity proof is displayed as Figure 6.3 in the book.

The meta-logical notions of consistency and completeness are clearly defined and explained, and are summarized by the statement that in propositional and predicate logic, “you can’t prove false theorems and if a theorem is true it has a proof.”

Part 3, “Set Theory,” is an excellent treatment of naîve, applicable set theory, and of relations and functions. Chapters 8 through 11 are titled “Set Theory,” “Inductively Defined Sets,” “Relations,” and “Functions.” Finite sets with equality “are well suited for computing applications.” (The material certainly covers infinite sets, as these are fundamental to computing science.) The discussion leads up to the definition of well-founded sets. Relations are very well covered, and the segue to functions is quite natural. The authors discuss Haskell functions that calculate the reflexive, symmetric, and transitive closures of relations, and partial, quasi, total, and well orders. The treatment of the topological sort is very efficient.

The characterization of functions as abstract models of computation that are deterministic is quite instructive, as are discussions of primitive recursive functions, computational complexity, and computations-with-state using true, deterministic functions. The book makes an insight-giving connection with weakest-precondition reasoning about imperative-language software; this explains the difficulty of finding errors in such software.

The authors go on to address higher-order functions (“user-defined control-structures”), currying (appropriately natural to Haskell), and total and partial functions. I am happy to see ⊥ as the symbol for “undefined” or “bottom,” which is what I originally learned. Some books have it stand for “false.” The existence of Haskell mechanisms for treating undefined values is welcome.

Part 4, “Applications,” has superbly chosen, elaborate examples: “The AVL Tree Miracle” (chapter 12) and “Discrete Mathematics in Circuit Design” (chapter 13). The first is about a 1950 log n insert/delete algorithm, and the last is a very efficient excursion into hardware design. The expressive perspicuity that Haskell allows keeps the reader’s attention on the theory being presented.

This excellent book has my highest recommendation.