×

Combinatory logic. (La logique combinatoire.) (French) Zbl 0873.03011

Que sais-je? Paris: Presses Universitaires de France. 127 p. (1997).
The book yields an elementary introduction to Combinatory Logic (henceforth CL), and it is apparently conceived for non-mathematicians. The first chapter (Theory of combinatorial applications) is an overview of the basic ideas and principles underlying CL, as they were conceived by the founding fathers M. Schoenfinkel and H. B. Curry (elimination of variables as unnecessary building blocks of Mathematical Logic; replacement of \(n\)-ary functions and \(n\)-ary application, in favor of suitable operators (combinators) and a basic ground operation of unrestricted unary function application; analysis of substitution by means of combinators). It further describes the fundamental applicative language of CL. The second chapter is devoted to the theory of elementary combinators: the basic combinators I, K, W, B, C are introduced, together with the notion of reduction, standard reduction, normal form and the statement of the Church-Rosser theorem. The chapter ends with the notion of combinatory law and a discussion of intensional and extensional equality. The third chapter deals with algebraic features of combinators (in essence, the definition of the semigroup of the so-called regular combinators under composite product; existence of combinatory bases) and with combinatory completeness (in the form that every applicative combination is a product of suitable combinators, i.e. identifiers, eliminators, duplicators, permutators and compositors). The author also lists a number of applications of combinatory logic to humanities, ranging from ethymology, theoretical grammar, philosophy, psychology (reformulations of certain ideas of Piaget’s school) to proper logic. Possible definitions of conversion (axiomatic, via reduction to a common reduct) are also analysed and Church’s undecidability theorem is stated. Chapter IV is partly historical and presents (i) Schoenfinkel’s method to reduce the basic notions of logic and bound variables by means of combinators; (ii) Curry’s ideas on paradoxes. Only at this point, Church’s lambda calculus is introduced and contrasted with CL (elimination of bound variables versus lambda abstraction). Ch. V introduces the reader to the theory of functionality and illative logic. A basic aim of this part is to devise rich type systems that allow to interpret more and more terms of CL as suitable operators of a given type. The author only discusses a version of the so-called subject construction property, according to which the construction of a type for a term M closely follows the construction of M. Moreover, if a combinator M has a type, then one can construct a canonical, direct derivation assigning that type to M and such derivation (normal derivation) is unique. The final chapter is devoted to Quine’s Predicate Functor Logic (PFL). PFL is compared with with CL, on the basis of its (weaker) ontological commitment (see Quine’s criticism to the presumed platonistic vein underlying CL).
Reviewer’s remarks. The most valuable feature of the book lies in the effort to motivate the basic ideas and techniques of combinatory logic, its underlying philosophical ideas and its potential import for the humanities. But the author has a hard task in front of him, as CL is notoriously a refractory subject to intuitive and sketchy treatments (see the confession of H. B. Curry and R. Feys [Combinatory Logic I (1958; Zbl 0081.24104), p. VIII]. As to the claimed applications to the humanities, the examples which are explicitly discussed in the book ought to be supplemented with more details and deeper insights, in order to be fully convincing and appreciated. Although the book under review is only introductory, we believe that the logico-mathematical part is unbalanced and insufficient. No proof of the consistency (Church-Rosser) theorem for CL is given, and there is hardly a proof’s sketch for the subject reduction theorem. In our opinion, the most important omission concerns (at least an introduction to) the set-theoretic semantics. For instance, the Plotkin-Scott graph model could have been outlined; its des cription is certainly technically simpler than some syntactical notions, introduced by the author in the book. In the chapter about illative CL, the so-called Curry-Howard isomorphism (the formula-as-type/term-as-proof interpretation) and the semantics of proofs are only implicitly hinted at, though the topic is highly relevant for applications (even in theoretical linguistics and in philosophy). As to the deep and natural links with computability theory and Computer Science, they are neglected and this could have been explicitly motivated by the author. In our opinion, some definitions are not sufficiently justified by subsequent use or they look rather unnatural (e.g. action-at-distance, pp.43-45, the distinction normal form-paranormal form, pp.35-38).

MSC:

03B40 Combinatory logic and lambda calculus
03-01 Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations
00A06 Mathematics for nonmathematicians (engineering, social sciences, etc.)

Citations:

Zbl 0081.24104
PDFBibTeX XMLCite