Logic & Programming

This book shows how to formalize some very basic mathematical notions from Logic, Abstract Algebra, Analysis, Linear Algebra, Differential Equations and Probability Theory, inside the functional programming language Haskell. Haskell is appropriate for expressing such notions since it encourages the use of high-order functions (resulting in concise, category-theory-like formulations), its variables are immutable (just like in Mathematics, eliminating computational side-effects related to variable mutation in imperative programming languages), it has algebraic data types (allowing inductive/recursive formulations and reasoning), and type classes (useful for treating mathematical theories in a compositional way). These same features are shared by proof assistant software such as Coq, which have been used extensively for formalization of Mathematics, however, what is different in the approach of this book, with respect to formalization efforts in settings with richer type systems, is that it allows one to build up an abstract mathematical concept more rapidly and experiment with it computationally, making it an interesting setting for doing experimental mathematics.

The book could be useful (indeed, it started as a coursebook for undergraduate students) for Mathematics students studying functional programming or Computer Science students studying Mathematics, but it could also be useful for researchers learning how to efficiently formalize their favorite mathematical theory inside a proof assistant. The formulations of the exponential function, the Laplace transform and the “axiomatization” of probability are elegant (concise!). One could perhaps regret the absence of definition of real numbers in the framework (real numbers are treated abstractly).

Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net