Chapter 2 The Qi Top Level 38

2.1 Starting Up 38
2.2 Applying Functions 39
2.3 Repeating Evaluations 40
2.4 Input/Output 41
2.5 Strict and Non-Strict Evaluation 43
2.6 Boolean Operations 44
2.7 Defining New Functions 45
2.8 Equations and Priority Rewrite Systems 47
2.9 A Fruit Machine Program 50

Chapter 3 Recursion 57

3.1 Recursion and Infinity 57
3.2 Forms of Recursion 59
3.3 Guards 61
3.4 Counting Change 63
3.4 Non-terminating Functions 64

Chapter 4 Lists 70

4.1 Representing Lists in Qi 70
4.2 Building Lists with Cons 71
4.3 Head and Tail Access Parts of Lists 73
4.4 Characters 74
4.5 Recursive List Processing 75
4.6 Local Assignments 77
4.8 Goldbach’s Conjecture Revisited 79

Chapter 5 Higher Order Programming 83

5.1 Higher Order Functions 83
5.2 Abstractions, Currying and Partial Applications 84
5.3 Using Abstractions in Higher Order Programs 86
5.4 Getting Rid of One-Off Functions 87
5.5 Taking Advantage of Similarities 88
5.6 Using Functions as Data 91

Chapter 6 Assignments 97

6.1 Simple Assignments 97
6.2 Arrays 99
6.3 Property Lists 100

Chapter 7 Non-determinism 106

7.1 Non-deterministic Algorithms 106
7.2 Backward Chaining 106
7.3 Representing Proof Trees 110
7.4 Chronological Backtracking in Qi 111
7.5 Soundness and Completeness 113
7.6 Writing Refinement Rules: a Preview 114
7.7 Selecting the Failure Object 117
7.8 The Static Elimination of Backtracking 118

Chapter 8 Metaprograms 123

8.1 Building a Parser in Qi 123
8.2 Recursive Descent Parsing in Qi 127
8.3 The eval Function 131

Chapter 9 Writing Good Programs 138

Part II Working with Types

Chapter 10 Types 143

10.1 Types and Type Security 143
10.2 Modifying the Read-Evaluate-Print Loop 144
10.3 Base Types and Operators 145
10.4 Using Type Checking 150
10.5 Lazy Types 153

Chapter 11 Defining Types 157

11.1 Enumeration Types 157
11.2 Side Conditions 158
11.3 Synonyms 159
11.4 Left and Right Rules 160
11.5 Defining Recursive Types 162
11.6 Simulating a Calculator 163
11.7 Verified Objects 165
11.8 Defining Type Operators 167
11.9 Working with Functions Other than Cons 168
11.10 Analytic, Synthetic, the Subformula Property 170
11.11 Optimising the Type Checking Environment 172
11.12 A Type Secure Whist Program 173

Chapter 12 Abstract Programming 183

12.1 Mastering Change and Complexity 183
12.2 Structures 184
12.3 Classes 189
12.4 Defaults 193
12.5 Inheritance 195
12.6 Abstract Data Types 199

Part III Theoretical Foundations

Chapter 13 Compiling Qi 204

13.1 The Lambda Calculus 204
13.2 Reasoning with the Lambda Calculus 206
13.3 The Church-Rosser Theorems 209
13.4 Representing Things in Lambda Calculus 211
13.5 Recursion and the Y-combinator 213
13.6 From Lambda Calculus to Functional Programming 215
13.7 The Compilation of Qi to L 218
13.8 Representing Mutual Recursion 221
13.9 An Operational Semantics for L 223
13.10 Implementing the Operational Semantics 225
13.11 The Compilation of L to Lambda Calculus 231
13.12 The Optimisation of Pattern Matching 235

Chapter 14 The Compilation of Sequent Calculus 238

14.1 The Architecture of the Sequent Compiler 238
14.2 Horn Clause Logic and its Implementation 239
14.3 Compiling Sequent Rules to Horn Clauses 247
14.4 Compiling Horn Clauses to m Expressions 250
14.5 The Abstract Unification Machine 252
14.6 Mode Declarations and Complex Terms 256
14.7 Compiling the AUM to Lisp 257
14.8 The Semantic Primitives of CLI 260
14.9 Head Abstraction 262

Chapter 15 Type Checking as Proof 267

15.1 The Qi Type System 267
15.2 Type Checking Applications 268
15.3 Type Checking Abstractions 269
15.4 Polymorphic Functions 271
15.5 Typing Special Forms 272
15.6 Recursion, Cases, Patterns and Guards 273
15.7 Global Variables 277
15.8 The Type Security of the L Type System 277
15.9 The Termination of T* 284
15.10 Procedure T* 289
15.11 From Type Checking to Automated Deduction 299

Part IV Models of Reasoning

Chapter 16 Logic 304

16.1 Implementing Reasoning Programs 304
16.2 Rule Abstractions 306
16.3 A Simple Proof Assistant 311
16.4 A Decision Procedure for PC 315
16.5 Generic Tactics 317
16.6 First Order Logic (FOL) 318
16.7 Automating Proof in FOL 323
16.8 Prenex Form 326
16.9 Rectification 327
16.10 Universal Quantifiers and Unification 328
16.11 Working with Clauses 329
16.12 The Incompleteness of autofol 334
16.13 A Complete Theorem Prover 337
16.14 Optimising our Theorem Prover 340

Chapter 17 Reasoning About the Physical World 347

17.1 Diagnosis as Explanation 348
17.2 Explanation and Proof Trees 349
17.3 Coding an Expert System in Qi 350
17.4 Coding a Descriptive Model in Qi 356
17.5 Implementing Rational Hedonism 366
17.6 Mathematical Modelling vs. Intelligent Agents 371

Appendices

Appendix A System Functions and their Types in Qi 375
Appendix B Installing and Using Qi under Lisp 389
Appendix C The Syntax of Qi and the Qi Reader and Printer 395
Appendix D The Qi Debugging Environment 401
Appendix E Qi-YACC 404
Appendix F Qi Prolog 412

Bibliography 419
Index 431