Handbook of logic in computer science. Vol. 5: Logical and algebraic methods (Q2753183)

[The articles of this volume will not be indexed individually. For reviews of Volumes 1--4 see Zbl 0806.68003, Zbl 0777.68001, Zbl 0829.68111 and Zbl 0876.68001, respectively.]NEWLINENEWLINEThis fifth volume of the series surveys a number of logical and algebraic methods useful for computer science. The first chapter [``Martin-Löf's type theory'' by \textit{B. Nordström, K. Petersson} and \textit{J. M. Smith}, pp. 1--37] presents Martin-Löf's type theory, whose original aim was to provide a clarification of constructive mathematics, as a common language for expressing specifications and programs within the same formalism. The notions of type and family of types are introduced, together with the notions of variable, assumption and substitution and the rules arising from the semantics. Next, function types and their formal rules (in the style of natural deduction) are introduced. The use of type theory as a logical framework is illustrated later on with the presentation of propositional logic by means of the Curry-Howard isomorphism between propositions and sets: a proposition is interpreted as the set whose elements represent the proofs of the proposition. Later on, type theory is used to represent a theory of sets with natural numbers, lists, functions, etc., which could be used when specifying and implementing computer programs.NEWLINENEWLINEA basic core of the interactions of category theory and mathematical logic which have been or might be used in computer science applications is introduced in the second chapter [``Categorical logic'' by \textit{A. M. Pitts}, pp. 39--128]. Three main themes are presented: the categorical semantics, the internal language in a category, and the term-model constructions. The first part of the chapter deals with the categorical semantics of many-sorted equational logic in a category with finite products. Then, the categorical semantics of some simple type constructors is considered, with the attempt of proving that the necessary categorical structure for a particular constructor can be systematically obtained from its introduction, elimination and equational rules. Finally, the term-model construction for an equational logic is presented, together with its theory-category correspondence. The second part is devoted to the categorical semantics of first-order classical logic, and that of type theories involving types that depend upon terms, such as Martin-Löf's type theory.NEWLINENEWLINEThe study of the complexity of logical theories is the main theme of the third chapter [``A uniform method for proving lower bounds on the computational complexity of logical theories'' by \textit{K. Compton} and \textit{C. W. Henson}, pp. 129--216]. A uniform method for obtaining lower bounds on the computational complexity of logical theories is presented, and several illustrations of its use are given. Essentially, theories in first-order logic and monadic second-order logic are considered for both the satisfiability and the validity problem. The complexity classes used are time-bounded classes for nondeterministic Turing machines and for the more general class of linear alternating Turing machines. One interesting feature of the proposed method is that interpretations are used to transfer lower bounds from one theory to another; this way, the need to code machine computations into the models of the theory being studied is eliminated.NEWLINENEWLINEThe next chapter [``Algebraic specification of abstract data types'' by \textit{J. Loeckx, H.-D. Ehrich} and \textit{M. Wolf}, pp. 217--316] is concerned with the specification of abstract data types: it presents algebras, logics, specification methods, specification languages and parameterization separately in terms of set-theoretical notions only, instead of using category theory. The first sections introduce the basic specification tools, from many-sorted algebras to logic; after defining the general notion of specification, three specification methods are presented (loose, initial and constructive specifications); then, a simple prototypical specification language is given, focusing on details of the language constructs; later on, it is shown how specification languages can be generalized for modularization and parameterization purposes. A brief introduction to the use of categorical constructs for abstract data types specification finishes this chapter.NEWLINENEWLINEThe final chapter [``Computable functions and semicomputable sets on many-sorted algebras'' by \textit{J. V. Tucker} and \textit{J. I. Zucker}, pp. 317--523] deals with computability. Computability theories on particular and general classes of algebras address central concerns in both mathematics and computer science. The theory presented is built on arbitrary many-sorted algebras, which allows us to consider computability issues on more general sets than \(\mathbb{N}\), such as the real and complex numbers, and other data sets such as matrices, polynomials, power series, algebraic curves, manifolds, etc. The objective of the chapter is to provide a general theory of computable functions on an arbitrary algebra that possesses generalizations of many of the important results in computability theory on natural numbers with a wide range of applications in mathematics and computer science. The theory is shown to satisfy a generalization of the Church-Turing thesis for functions and sets computed by algorithms on any abstract algebraic structure, as well as to cover other less general but still abstract and algebraic theories of finite computation, including effective algebra and computable analysis.