Browse Books

Reviewer: Vladik Ya. Kreinovich

For good or bad, modern mathematics is mainly based on the language of set theory. Therefore, when we formalize our problems, we usually use either set theory itself or some mathematical formalism that is reducible to set theory. Set theory is thus a natural specification language. Alas, set theory is very far from algorithms; sometimes, however, we can find algorithms for set-theoretic specifications, and it is desirable to grasp as large an algorithmic part of set theory as possible. Some approaches (such as the Z specification language) have tried to follow this idea, but their main drawback is that they use only set-theoretic language; in reality, when we think about a problem, we can use several languages, including mathematical languages (in essence, set theory), the language of programs and algorithms, and the language of proofs and derivations. Martin-Lo¨f's basic idea was to develop a general formalism that would include all these languages and still be constructive, so that any specification in any of these languages (or in their combination) could still be automatically translated into a program. His idea is that there is a similarity between the following statements: “ a is an element of a set A ,” “ a is a program that satisfies the specification A ,” “ a is a proof of the proposition A ,” and “ a is a solution to a problem A .” Martin-Lo¨f started with sets for which algorithms exist that decide whether a given element belongs to the set and whether two given elements are equal. He showed that when we apply practically all set-theoretic operations (except factor-set) to such sets, we also get sets with such algorithms. Some properties of the resulting theory are easy to grasp in set-theoretical language, but some are better understood if we use the proof-theoretic reformulations. The advantage of this approach is that in reasonable cases it leads not only to algorithms but to algorithms of reasonable time complexity. All this material is covered by the book. The introduction places Martin-Lo¨f's theory among its rivals. Part 1 describes the basic constructions of his set theory. Part 2 adds the construction of subsets. In principle, this fragment is already sufficient to express many reasonable properties. In this pure set theory, we consider variables running only over arbitrary sets, while in informal mathematical reasoning we mostly use phrases like “for all functions” and “there exists a real number.” Of course, these expressions can be explicitly translated into pure set theory, but this translation leads to additional unrestricted quantifiers and hence to unnecessary computational complexity. It is therefore reasonable to add these restricted quantifiers to our specification language. Such restrictions are called types, because they correspond to abstract data types in programming languages. (Martin-Lo¨f's types are actually more powerful because they allow very general types and families of types.) Part 3 covers this extension of the theory, and Part 4 contains examples. For those who already believe in this approach, this is a good book to study systematically. For those in doubt, however, the book will not be very convincing: all the examples are located at the end of the book, and their main purpose is to illustrate the material rather than to convince. Someone who wants to use it as a textbook should find convincing examples elsewhere.