Book review

Agostino Dovier
Dip. di Matematica e Informatica, Univ. di Udine (IT).

Set Theory for Computing:
From Decision Procedures to Declarative Programming with Sets
Domenico Cantone, Eugenio Omodeo, and Alberto Policriti
Monographs in Computer Science, Springer-Verlag, 2001
ISBN 0-387-95197-0, hardcover, $ 69.95
xviii + 409 pages
http://turing.dipmat.unict.it/$\sim$cantone/SetTheoryForComputing

1 In Short

This book is an up-to-date and well-organized collection of techniques and results concerning the problem of dealing with sets in computer science. Being an intuitive and widespread notion, sets are commonly used by scientists for formalizing problems. Thus, this notion can be included as a first-class citizen in a programming language, allowing a set-based declarative style of programming. However, when implementing such a language, one need to face satisfiability problems involving set-based formulas. Set-based notations can be naturally used to assign abstract semantics to programs: verification of program properties in this case amounts at checking the satisfiability of a set-based formula. Moreover, it is well-known that Modal/Temporal logics can serve as a tool for program verification. Satisfiability in these logics can be mapped into set-based satisfiability (such a translation technique is described in the book). Thus, it goes without saying that a good starting point for dealing with sets in computer science is to study the satisfiability test for set-based formulae. Although this problem is in general undecidable, finding decidable classes of formulas whose test is decidable and finding suitable axiomatizations for them are two challenging activities and they are the main concern of the so-called Computable Set Theory (CST) area. The authors of the book have worked in this field for nearly twenty years and they are co-authors of most of the results and techniques presented. However, the book does not only deal with CST, but also with inference techniques suitable for reasoning with sets (e.g., $T$-resolution, Semantic tableaux) and with programming languages developed for dealing with sets (in particular, the imperative language SETL and the constraint logic programming language {log}). The book presents several algorithms written in these languages and, moreover, it is described how common programming data structures can be naturally encoded in set theory.

Jacob T. Schwartz, the undisputed father of CST, writes in his excellent foreword to the book: ``this range of mathematical investigation must be approached with a cautious respect for the bottomless pit of undecidability that lies near.'' Thus, it is not astonishing that some parts of the book are, for their intrinsic nature, rather difficult and addressed prevailingly to mature readers. In particular, the book can be very interesting for postgraduate students and researchers in computer science and logic. Graduate students can also cheat fruitful ideas from the reading of the general parts of the book and can learn a lot by carring out some of the several proposed exercises. The book is largely self-contained and the style of presentation is extremely rigorous and accurate. Nevertheless, some more examples could help the comprehension of some, extremely concise, definitions.

2 Contents

The book consists of 14 chapters, divided into four parts:

I.

Introduction

1.

What is Computable Set Theory?

2.

Logical Background

II.

Basics for Set-Theoretic Reasoning

3.

Axiomatic Views of Aggregates

4.

Semantic Views of Aggregates

5.

Sets for Problem Solving

6.

Decision Problems and Some Solutions

7.

Inference Techniques and Methods

III.

Decision Methods

8.

Set/Hyperset Unification Algorithms

9.

A Syllogistic Solitaire

10.

Stratified Syllogistics

IV.

Set-specific Inference Engines

11.

Quantitative Set Reasoning

12.

Set Theory for Nonclassic Logics

13.

Logic Programming with Sets

14.

Syllogistic Tableaux

1 I. Introduction.

In this part of the book the authors describe what is Computable Set Theory and its possible impact on ``traditional'' computer science (Chapter 1). Chapter 2 presents the propositional calculus, the first-order calculus, and the (perhaps less known) ``map'' calculus. I appreciate very much the complete descriptions of the algorithms for reaching normal forms (often only sketched in logic surveys): for propositional calculus, how to obtain an equisatisfiable disjunctive/conjunctive normal form avoiding inessential size exponential growth; for first-order calculus, how eliminating quantifiers using Skolem functors (this part can be also read together with Section 6.3.1: ``Reduction to prenex normal form''). I find very instructive the inclusion of the Hilbert descriptor $\varepsilon$ ( $\varepsilon\: x$ means ``an $x$ s.t.'') and of the Peano descriptor

(

$x$ means ``the $x$ s.t.'') in the set of quantifiers.

2 II. Basics for Set-Theoretic Reasoning.

This part touches on several foundamental issues and takes up more or less half of the book. In Chapters 3 and 4 the notion of ``aggregate'' is presented both axiomatically and semantically. Aggregate is a term that embodies the notion of set as well as some possible variants of it emerging from different axiomatizations. For instance, it can be used to address in one word sets, multisets, and lists. In Chapter 5 the authors show how to use sets for implementing tuples, graphs, functions, deterministic and non-deterministic automata. Moreover, some interesting puzzles are encoded in set-based formalisms, some classical algorithms are implemented in (tiny) SETL, and the notion of ``declarative specification'' is presented. Section 5.6 deals with ``Sets for Program Verification''. The section is very interesting but it lacks of a comparison to the similar approach of the community of ``Set Constraints'', born and developed with that specific aim. Chapter 6 presents the satisfiability and validity problem for set-based formulas and the main classes of formulas that have been successfully faced in the past, while Chapter 7 introduces the notion of $T$-resolution. In $T$-resolution, syntactic unification can be replaced by a more complex inference mechanism (e.g., a simple set-based theorem prover) in the derivation step and it is therefore well-suited for set-based reasoning. Moreover, semantic tableaux are introduced (they are used next in the book for decision methods). The chapter also presents a self-contained, quite traditional, introduction to logic programming.

3 III. Decision Methods.

In Chapter 8 the authors present the set and hyperset-unification problem and some algorithms for solving it: a guess and verify method that works with few changes in the two cases, and a goal-driven method for each problem. Chapter 9 is labeled by (*) and addressed, using the words of the authors, to ``more mature readers'': the decision problem for a class of formulas is presented as a (syllogistic) game. Chapter 10 is devoted to show algorithms for solving the satisfiability problem for ``stratified'' sets. Basically, sets in this case can have elements that are non-sets (level 1). Then there are sets that can have as elements sets of level 1 and other, possibly different, non-sets (level 2), and so on. Several classes involving particular operators are studied.

4 IV. Set-Specific Inference Engines.

In Chapter 11 it is shown how to transform the satisfiability problem for a class of set-formulas into a problem of integer linear programming. Since decision algorithms for sets are often intractable, one can take advantage from the efficiency of branch-and-bound, cutting planes, or approximated methods developed for this field. Chapter 12 presents modal logics and the so-called $\Box$-as-$\cal P$ translation of propositional modal formulas into set terms. This chapter establishes an important link between CST and the typical applications of modal/temporal logics, e.g., analysis and verification of programs and reactive systems. In Chapter 13 the authors present the constraint logic programming language {log} and show its expressive power on some examples. In the ``Commentary'' at the end of the chapter they also give references to the recent development of that language (also known as $CLP({\cal SET})$, being now an instance of the CLP scheme) whose running implementation can be freely obtained from the Web. Chapter 14 shows the elegance of tableaux-like methods for proving decidability of the class of formulas known as MLSS (and of some of its extensions). It looks very promising both for proving new results and for restating known decidability results in a general framework.

3 To Conclude

The book is a deep and self-contained collection of topics concerning Sets in Computer Science and, in particular, a general and up-to-date survey of Computable Set Theory. I guess that it will become a sort of classic work for automated deduction and declarative programming and surely it deserves to find its place in all scientific libraries. The book is supported by a WWW page which contains the solution of some exercises, the implemented code, an errata corrige list, and various related material. The book contains a very long list of references (more than 250 items) and several historical quotations that allow the interested reader to increase his knowledge of the history of set theory and automated deduction.