Programming with Higher-Order Logic

Programming with Higher-Order Logic
Dale Miller and Gopalan Nadathur
Cambridge University Press 2013

Church's higher-order logic, based on the typed $\lambda$-calculus, is a foundation of mathematics and computer science.  It underpins a number of other influential logics and type theories, including systems for formalized mathematics such as LF, HOL and Coq, which in turn have led to interesting developments relevant to mainstream mathematics such as formal proofs of the Four-Color Theorem and Feit-Thompson Theorem in Coq, as well as the Homotopy Type Theory program initiated by Voevodsky.  This book is about higher-order logic viewed in a different light, as a foundation for programming, specifically following the computation-as-deduction approach taken in logic programming languages such as Prolog.  Higher-order logic programming builds on higher-order unification, and generalizes Horn clauses over first-order terms in Prolog to hereditary Harrop formulas over higher-order terms in languages such as $\lambda$Prolog. One might view (higher-order) logic programming as a tool deserving a place in a logician's toolbox analogous to numerical or symbolic tools for analysis: not a replacement for mathematical reasoning, but a framework for experimentation and automation.



There are several accessible textbook presentations of unification and logic programming in the first-order case, following the classical approach to the semantics of logic programs via Herbrand models and least fixed points.  However, foundations for higher-order logic programming do not follow directly from the conventional approach to first-order logic programming.  The semantics of higher-order logic programs is better understood in terms of (intuitionistic) proof theory based on Gentzen-style sequent calculus. To date there has been no uniform and accessible book-length treatment of higher-order logic programming including its semantics, pragmatics, and applications. It is therefore difficult for interested researchers to gain an overview of the topic without a review of the extensive literature. Miller and Nadathur's Programming with Higher-Order Logic seeks to fill this lacuna.

A preliminary chapter introduces the subject and places the book in context.  The first five numbered chapters develop foundations, starting with concepts from first-order logic.  The main themes of the area are developed at a leisurely pace, and should be accessible to undergraduate students already familiar with ordinary logic programming, or graduate students in logic or theoretical computer science.  The exposition of first-order terms and Horn clauses in chapters 1 and 2 serves as a self-contained definition of the semantics of a Prolog-like language from a proof-theoretic perspective, which should aid readers independently of their familiarity with other treatments of logic programming.  Chapter 3 generalizes first-order logic programming from Horn clauses to hereditary Harrop clauses, in which universal quantification and local implication are allowed in goals; these extensions demonstrate advantages of the proof-theoretic approach to logic programming even within first-order logic.  Chapter 4 introduces typed $\lambda$-calculus and the higher-order unification problem.  Chapter 5 presents full higher-order logic programming, including quantification over higher-order $\lambda$-terms and the subtleties arising from the possibility of flexible atoms appearing in goal formulas as a result of quantification over propositions or predicates. Conventional extensions to logic programming such as conditionals and negation as failure are also discussed.

Subsequent chapters explore pragmatics and applications of higher-order logic programming.  Chapter 6 shows how modularity can be supported using higher-order abstractions.  Chapter 7 introduces $\lambda$-tree abstract syntax, that is, the idea of using $\lambda$-terms as a data structure for meta-programming and reasoning about abstract syntax, and describes the well-behaved $L_\lambda$ subset of $\lambda$Prolog.  Chapter 8 investigates algorithms for higher-order unification in greater detail, including the special case of higher-order pattern unification which is efficiently decidable, and covers pragmatic issues such as handling of mixed quantifier prefixes.

The remaining chapters present case studies of applications of higher-order logic programming in $\lambda$Prolog.  Chapter 9 presents simple implementations of theorem provers for intuitionistic and classical logics, and outlines a general architecture for such systems.  Chapter 10 illustrates the use of $\lambda$-tree abstract syntax for specifying a small functional programming language and program transformations on it.  Chapter 11 presents an encoding of Milner's $\pi$-calculus in $\lambda$Prolog, including specifications of transitions and a translation from  $\lambda$-calculus into $\pi$-calculus.  These applications highlight the strengths of higher-order logic programming for lightweight specification and experimentation with formal systems.

Although the book is not intended to be a programming manual, key ideas are illustrated throughout using $\lambda$Prolog, and an appendix presents the Teyjus implementation of $\lambda$Prolog.

Miller and Nadathur have not recapitulated the major underlying research results on higher-order logic programming (such as cut-elimination or uniform proofs); instead, the book presents the applications of these ideas explained in a computational setting, and points the reader towards relevant research literature for more details.  Formal details are generally minimized in favor of discursive explanation, and for most readers this choice should be satisfactory, though readers already familiar with some concepts might find some parts of the book prolix.

Programming with Higher-Order Logic is a valuable complement to the research literature on logic programming and proof theory, and could serve as a basis for self-study or graduate-level teaching on computational aspects of higher-order logic.