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