The Haskell Road to Logic, Maths and Programming. Second Edition (Texts in Computing)
Kees Doets
Language: English
Pages: 450
ISBN: 0954300696
Format: PDF / Kindle (mobi) / ePub
Long ago, when Alexander the Great asked the mathematician Menaechmus for a crash course in geometry, he got the famous reply ``There is no royal road to mathematics.’’ Where there was no shortcut for Alexander, there is no shortcut for us. Still, the fact that we have access to computers and mature programming languages means that there are avenues for us that were denied to the kings and emperors of yore. The purpose of this book is to teach logic and mathematical reasoning in practice, and to connect logical reasoning with computer programming in Haskell. Haskell emerged in the 1990s as a standard for lazy functional programming, a programming style where arguments are evaluated only when the value is actually needed. Haskell is a marvelous demonstration tool for logic and maths because its functional character allows implementations to remain very close to the concepts that get implemented, while the laziness permits smooth handling of infinite data structures. This book does not assume the reader to have previous experience with either programming or construction of formal proofs, but acquaintance with mathematical notation, at the level of secondary school mathematics is presumed. Everything one needs to know about mathematical reasoning or programming is explained as we go along. After proper digestion of the material in this book, the reader will be able to write interesting programs, reason about their correctness, and document them in a clear fashion. The reader will also have learned how to set up mathematical proofs in a structured way, and how to read and digest mathematical proofs written by others. This is the updated, expanded, and corrected second edition of a much-acclaimed textbook. Praise for the first edition: ‘Doets and van Eijck’s ``The Haskell Road to Logic, Maths and Programming’’ is an astonishingly extensive and accessible textbook on logic, maths, and Haskell.’ Ralf Laemmel, Professor of Computer Science, University of Koblenz-Landau
woman. Long ago the philosopher Bertrand Russell has proposed this logical format for the translation of the English definite article. According to his theory of description, the translation of The King is raging becomes: ∃x(King(x) ∧ ∀y(King(y) ⇒ y = x) ∧ Raging(x)). Exercise 2.35 Use Russell’s recipe to translate the following sentences: 1. The King is not raging. 2. The King is loved by all his subjects. (use K(x) for ‘x is a King’, and S(x, y) for ‘x is a subject of y’). Exercise 2.36
≡ ∀xΦ(x), 3. ∀x(Φ(x) ∧ Ψ(x)) ≡ (∀xΦ(x) ∧ ∀xΨ(x)); ∃x(Φ(x) ∨ Ψ(x)) ≡ (∃xΦ(x) ∨ ∃xΨ(x)). Proof. There is no neat truth table method for quantification, and there is no neat proof here. You just have to follow common sense. For instance (part 2, first item) common sense dictates that not every x satisfies Φ if, and only if, some x does not satisfy Φ. Of course, common sense may turn out not a good adviser when things get less simple. Chapter 3 hopefully will (partly) resolve this problem for you.
"Russell" ‘elem‘ "Cantor" *** term : "Russell" *** type : String *** does not match : Char Prelude> You would expect from this that elem has type a -> [a] -> Bool, for it takes an object of any type a as its first argument, then a list over type a, and it returns a verdict ‘true’ or ‘false’, i.e., an object of type Bool. Almost, but not quite. The snag is that in order to check if some thing x is an element of some list of things l, one has to be able to identify things of the type of x. The
(a,b) -> c), can be done by means of the procedures for currying and uncurrying a function. The procedures refer to the logician H.B. Curry who helped laying the foundations for functional programming. (The initial H stands for Haskell; the programming language that we use in this book is also named after him.) If f is of type (a,b) -> c, then currying f means transforming it into a function that takes its arguments one by one, i.e., a function of type a -> b -> c. The procedure curry is
words, from the operations that are performed on that object. Take again the definition of divides. It is clear from the definition that an operation is defined with two arguments, both of which are of a type for which rem is defined, and with a result of type Bool (for rem n d == 0 is a statement that can turn out true or false). If we check the type of the built-in procedure rem we get: Prelude> :t rem rem :: Integral a => a -> a -> a In this particular case, the type judgment gives a type