Programming with Higher-Order Logic

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. Cover 1 Abstract 3 Title Page 5 Contents 9 Preface 13 Introduction 17 I.1 Connections between logic and computation 17 I.2 Logical primitives and programming expressivity 19 I.3 The meaning of higher-order logic 21 I.4 Presentation style 22 I.5 Prerequisites 23 I.6 Organization of the book 24 1 First-Order Terms and Representations of Data 26 1.1 Sorts and type constructors 26 1.2 Type expressions 28 1.3 Typed first-order terms 30 1.4 Representing symbolic objects 35 1.4.1 Representing binary trees 36 1.4.2 Representing logical formulas 38 1.4.3 Representing imperative programs 40 1.5 Unification of typed first-order terms 42 1.6 Bibliographic notes 48 2 First-Order Horn Clauses 50 2.1 First-order formulas 50 2.2 Logic programming and search semantics 54 2.3 Horn clauses and their computational interpretation 59 2.4 Programming with first-order Horn clauses 62 2.4.1 Concrete syntax for program clauses 62 2.4.2 Interacting with the λProlog system 65 2.4.3 Reachability in a finite-state machine 69 2.4.4 Defining relations over recursively structured data 72 2.4.5 Programming over abstract syntax representations 73 2.5 Pragmatic aspects of computing with Horn clauses 76 2.6 The relationship with logical notions 78 2.6.1 The cut rule and cut-elimination 79 2.6.2 Different presentations of fohc 79 2.7 The meaning and use of types 82 2.7.1 Types and the categorization of expressions 82 2.7.2 Polymorphic typing 83 2.7.3 Type checking and type inference 84 2.7.4 Types and run-time computations 85 2.8 Bibliographic notes 88 3 First-Order Hereditary Harrop Formulas 91 3.1 The syntax of goals and program clauses 91 3.2 Implicational goals 93 3.2.1 Inferences among propositional clauses 94 3.2.2 Hypothetical reasoning 95 3.3 Universally quantified goals 98 3.3.1 Substitution and quantification 100 3.3.2 Quantification can link goals and clauses 102 3.4 The relationship with logical notions 104 3.4.1 Classical versus intuitionistic logic 105 3.4.2 Intuitionistic versus minimal logic 105 3.4.3 Notable subsets of fohh 107 3.5 Bibliographic notes 109 4 Typed λ-Terms and Formulas 112 4.1 Syntax for λ-terms and formulas 113 4.2 The rules of λ-conversion 116 4.3 Some properties of λ-conversion 117 4.4 Unification problems as quantified equalities 121 4.4.1 Simplifying quantifier prefixes 123 4.4.2 Unifiers, solutions, and empty types 124 4.4.3 Examples of unification problems and their solutions 126 4.5 Solving unification problems 127 4.6 Some hard unification problems 129 4.6.1 Solving Post correspondence problems 130 4.6.2 Solving Diophantine equations 131 4.7 Bibliographic notes 132 5 Using Quantification at Higher-Order Types 134 5.1 Atomic formulas in higher-order logic programs 134 5.1.1 Flexible atoms as heads of clauses 135 5.1.2 Logical symbols within atomic formulas 137 5.2 Higher-order logic programming languages 138 5.2.1 Higher-order Horn clauses 138 5.2.2 Higher-order hereditary Harrop formulas 140 5.2.3 Extended higher-order hereditary Harrop formulas 141 5.3 Examples of higher-order programming 142 5.4 Flexible atoms as goals 148 5.5 Reasoning about higher-order programs 150 5.6 Defining some of the logical constants 152 5.7 The conditional and negation-as-failure 153 5.8 Using λ-terms as functions 154 5.8.1 Some basic computations with functional expressions 154 5.8.2 Functional difference lists 156 5.9 Higher-order unification is not a panacea 159 5.10 Comparison with functional programming 162 5.11 Bibliographic notes 163 6 Mechanisms for Structuring Large Programs 166 6.1 Desiderata for modular programming 166 6.2 A modules language 167 6.3 Matching signatures and modules 172 6.4 The logical interpretation of modules 176 6.4.1 Existential quantification in program clauses 176 6.4.2 A module as a logical formula 178 6.4.3 Interpreting queries against modules 179 6.4.4 Module accumulation as scoped inlining of code 180 6.5 Some programming aspects of the modules language 181 6.5.1 Hiding and abstract datatypes 181 6.5.2 Code extensibility and modular composition 183 6.5.3 Signature accumulation and parametrization of modules 184 6.5.4 Higher-order programming and predicate visibility 186 6.6 Implementation considerations 188 6.7 Bibliographic notes 189 7 Computations over λ-Terms 191 7.1 Representing objects with binding structure 191 7.1.1 Encoding logical formulas with quantifiers 193 7.1.2 Encoding untyped λ-terms 194 7.1.3 Properties of the encoding of binding 195 7.2 Realizing object-level substitution 196 7.3 Mobility of binders 199 7.4 Computing with untyped λ-terms 201 7.4.1 Computing normal forms 201 7.4.2 Reduction based on paths through terms 203 7.4.3 Type inference 206 7.4.4 Translating to and from de Bruijn syntax 208 7.5 Computations over first-order formulas 211 7.6 Specifying object-level substitution 215 7.7 The λ-tree approach to abstract syntax 219 7.8 The L_λ subset of λProlog 220 7.9 Bibliographic notes 224 8 Unification of λ-Terms 227 8.1 Properties of the higher-order unification problem 228 8.2 A procedure for checking for unifiability 230 8.2.1 Simplification of rigid-rigid equations 230 8.2.2 Substitutions for equations between flexible and rigid terms 230 8.2.3 The iterative transformation of unification problems 232 8.2.4 Unification problems with only flexible-flexible equations 233 8.2.5 Nontermination of reductions 234 8.2.6 Matching trees 235 8.3 Higher-order pattern unification 236 8.4 Pragmatic aspects of higher-order unification 240 8.5 Bibliographic notes 242 9 Implementing Proof Systems 245 9.1 Deduction in propositional intuitionistic logic 245 9.2 Encoding natural deduction for intuitionistic logic 247 9.3 A theorem prover for classical logic 251 9.4 A general architecture for theorem provers 256 9.4.1 Goals and tactics 256 9.4.2 Combining tactics into proof strategies 259 9.5 Bibliographic notes 261 10 Computations over Functional Programs 263 10.1 The miniFP programming language 263 10.2 Specifying evaluation for miniFP programs 266 10.2.1 A big-step-style specification 266 10.2.2 A specification using evaluation contexts 269 10.3 Manipulating functional programs 271 10.3.1 Partial evaluation of miniFP programs 271 10.3.2 Transformation to continuation passing style 272 10.4 Bibliographic notes 274 11 Encoding a Process Calculus Language 277 11.1 Representing the expressions of the π-calculus 277 11.2 Specifying one-step transitions 279 11.3 Animating π-calculus expressions 282 11.4 May- versus must-judgments 285 11.5 Mapping the λ-calculus into the π-calculus 289 11.6 Bibliographic notes 291 Appendix: The Teyjus System 293 A.1 An overview of the Teyjus system 293 A.2 Interacting with the Teyjus system 294 A.3 Using modules within the Teyjus system 299 A.4 Special features of the Teyjus system 301 A.4.1 Built-in types and predicates 302 A.4.2 Deviations from the language assumed in this book 303 Bibliography 305 Index 317 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 [lambda]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 [lambda]-terms And [pi]-calculus Expressions Can Be Encoded In [lambda]prolog--provided By Publisher. Introduction -- 1. First-order Terms And Representations Of Data -- 2. First-order Horn Clauses -- 3. First-order Hereditary Harrop Formulas -- 4. Typed [lambda] Terms And Formulas -- 5. Using Quantification At Higher-order Types -- 6. Mechanisms For Structuring Large Programs -- 7. Computations Over [lambda]-terms -- 8. Unification Of [lambda]-terms -- 9. Implementing Proof Systems -- 10. Computations Over Functional Programs -- 11. Encoding A Process Calculus Language -- Appendix: The Teyjus System. Dale Miller, Gopalan Nadathur. Includes Bibliographical References (pages 289-299) And Index. "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 [Lambda]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 [lambda]-terms and [pi]-calculus expressions can be encoded in [Lambda]Prolog"-- Provided by publisher La 4e de couverture : "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 [Lambda]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 [lambda]-terms and [pi]-calculus expressions can be encoded in [Lambda]Prolog." Machine generated contents note: 1. First-order terms and representations of data; 2. First-order horn clauses; 3. First-order hereditary Harrop formulas; 4. Typed lambda terms and formulas; 5. Using quantification at higher-order types; 6. Mechanisms for structuring large programs; 7. Computations over [lambda]-terms; 8. Unification of [lambda]-terms; 9. Implementing proof systems; 10. Computations over functional programs; 11. Encoding a process calculus language; Appendix A. The Teyjus system.