You are previewing Programming with Higher-Order Logic.
O'Reilly logo
Programming with Higher-Order Logic

Book Description

Formal systems that describe computations over syntactic structures occur frequently in computer science. Logic programming provides a natural framework for encoding and animating such systems. However, these systems often embody variable binding, a notion that must be treated carefully at a computational level. This book aims to show that a programming language based on a simply typed version of higher-order logic provides an elegant, declarative means for providing such a treatment. Three broad topics are covered in pursuit of this goal. First, a proof-theoretic framework that supports a general view of logic programming is identified. Second, an actual language called  Prolog is developed by applying this view to higher-order logic. Finally, a methodology for programming with specifications is exposed by showing how several computations over formal objects such as logical formulas, functional programs, and  -terms and ?-calculus expressions can be encoded in Prolog.

Table of Contents

  1. Title Page
  2. Copyright Page
  3. Contents
  4. Preface
  5. Introduction
    1. I.1 Connections between logic and computation
    2. I.2 Logical primitives and programming expressivity
    3. I.3 The meaning of higher-order logic
    4. I.4 Presentation style
    5. I.5 Prerequisites
    6. I.6 Organization of the book
  6. 1 First-Order Terms and Representations of Data
    1. 1.1 Sorts and type constructors
    2. 1.2 Type expressions
    3. 1.3 Typed first-order terms
    4. 1.4 Representing symbolic objects
    5. 1.5 Unification of typed first-order terms
    6. 1.6 Bibliographic notes
  7. 2 First-Order Horn Clauses
    1. 2.1 First-order formulas
    2. 2.2 Logic programming and search semantics
    3. 2.3 Horn clauses and their computational interpretation
    4. 2.4 Programming with first-order Horn clauses
    5. 2.5 Pragmatic aspects of computing with Horn clauses
    6. 2.6 The relationship with logical notions
    7. 2.7 The meaning and use of types
    8. 2.8 Bibliographic notes
  8. 3 First-Order Hereditary Harrop Formulas
    1. 3.1 The syntax of goals and program clauses
    2. 3.2 Implicational goals
    3. 3.3 Universally quantified goals
    4. 3.4 The relationship with logical notions
    5. 3.5 Bibliographic notes
  9. 4 Typed λ-Terms and Formulas
    1. 4.1 Syntax for λ-terms and formulas
    2. 4.2 The rules of λ-conversion
    3. 4.3 Some properties of λ-conversion
    4. 4.4 Unification problems as quantified equalities
    5. 4.5 Solving unification problems
    6. 4.6 Some hard unification problems
    7. 4.7 Bibliographic notes
  10. 5 Using Quantification at Higher-Order Types
    1. 5.1 Atomic formulas in higher-order logic programs
    2. 5.2 Higher-order logic programming languages
    3. 5.3 Examples of higher-order programming
    4. 5.4 Flexible atoms as goals
    5. 5.5 Reasoning about higher-order programs
    6. 5.6 Defining some of the logical constants
    7. 5.7 The conditional and negation-as-failure
    8. 5.8 Using λ-terms as functions
    9. 5.9 Higher-order unification is not a panacea
    10. 5.10 Comparison with functional programming
    11. 5.11 Bibliographic notes
  11. 6 Mechanisms for Structuring Large Programs
    1. 6.1 Desiderata for modular programming
    2. 6.2 A modules language
    3. 6.3 Matching signatures and modules
    4. 6.4 The logical interpretation of modules
    5. 6.5 Some programming aspects of the modules language
    6. 6.6 Implementation considerations
    7. 6.7 Bibliographic notes
  12. 7 Computations over λ-Terms
    1. 7.1 Representing objects with binding structure
    2. 7.2 Realizing object-level substitution
    3. 7.3 Mobility of binders
    4. 7.4 Computing with untyped λ-terms
    5. 7.5 Computations over first-order formulas
    6. 7.6 Specifying object-level substitution
    7. 7.7 The λ-tree approach to abstract syntax
    8. 7.8 The Lλ subset of λProlog
    9. 7.9 Bibliographic notes
  13. 8 Unification of λ-Terms
    1. 8.1 Properties of the higher-order unification problem
    2. 8.2 A procedure for checking for unifiability
    3. 8.3 Higher-order pattern unification
    4. 8.4 Pragmatic aspects of higher-order unification
    5. 8.5 Bibliographic notes
  14. 9 Implementing Proof Systems
    1. 9.1 Deduction in propositional intuitionistic logic
    2. 9.2 Encoding natural deduction for intuitionistic logic
    3. 9.3 A theorem prover for classical logic
    4. 9.4 A general architecture for theorem provers
    5. 9.5 Bibliographic notes
  15. 10 Computations over Functional Programs
    1. 10.1 The miniFP programming language
    2. 10.2 Specifying evaluation for miniFP programs
    3. 10.3 Manipulating functional programs
    4. 10.4 Bibliographic notes
  16. 11 Encoding a Process Calculus Language
    1. 11.1 Representing the expressions of the π-calculus
    2. 11.2 Specifying one-step transitions
    3. 11.3 Animating π-calculus expressions
    4. 11.4 May- versus must-judgments
    5. 11.5 Mapping the λ-calculus into the π-calculus
    6. 11.6 Bibliographic notes
  17. Appendix: The Teyjus System
    1. A.1 An overview of the Teyjus system
    2. A.2 Interacting with the Teyjus system
    3. A.3 Using modules within the Teyjus system
    4. A.4 Special features of the Teyjus system
  18. Bibliography
  19. Index