The Book of Shen 5th Edition

Author's Note

This is an online version of The Book of Shen, 5th edition (TBoS) available from the Great British Book Store. If you are reading TBoS to understand Shen, first click on 'How to Read this Book' in the table of contents.

Programs by Section and Chapter

3.2 3.3 3.4 3.5 3.6 3.7 4.3 4.4 4.5 5.4 6.4 6.5 7.1 8.1 8.3 8.4 8.5 8.6 8.7 9.1 12.4 9.2 10.4 10.5 11.2 12.2 13.2 13.3 13.4 13.5 13.6 13.7 13.8 13.9 14.4 14.5 14.6 14.7 15.1 15.2 15.7 17.5 17.6 17.7 18.6 19.1 19.2 19.4 19.5 19.6 19.8 20.3 20.4 20.6 20.7 20.8 20.9 21.1 21.3 21.4 21.5 22.2 22.3 23.2 23.3 23.4.1 23.4.2 24.3 24.4 24.5 24.6 24.7 24.8 24.9 25.3 25.6 25.7 27.19 28.3

Index

Table of Contents

Dedication iii
How to Read this Book xi
A Conceptual Dependency Table xii
Preface to the Fifth Edition xiii
Acknowledgements xiv

Chapter 1 Beginnings 1

1.1 Declarative Programming 1
1.2 Mathematical Foundations 2
1.3 The American Experience 7
1.4 The British Experience 11
1.5 The Forerunners of Shen: SEQUEL 13
1.6 The Forerunners of Shen: Qi 14
1.7 Shen 16


Part I The Core Language


Chapter 2 Starting Shen 20

2.1 Starting Up 21
2.2 Applying Functions 22
2.3 Repeating Evaluations 23
2.4 Strict and Non-Strict Evaluation 24
2.5 Boolean Operations 25
2.6 Defining New Functions 26
2.7 Equations and Priority Rewrite Systems 27
2.8 A Bible Studies Program 29

Chapter 3 Recursion 33

3.1 Of Numbers 33
3.2 Recursion and the Factorial Function 36
3.3 Forms of Recursion 37
3.4 Tracing Function Calls 40
3.5 Guards 40
3.6 Counting Change 43
3.7 Non-terminating Functions 44

Chapter 4 Lists 48

4.1 Representing Lists in Shen 48
4.2 Building Lists with cons 49
4.3 hd and tl Access List Components 51
4.4 Local Assignments 55
4.5 Goldbach’s Conjecture Revisited 56

Chapter 5 Strings 60
5.1 Strings and Symbols 61
5.2 Building Strings with make-string 63
5.3 Coercing Strings to Lists 64
5.4 Programming with Strings 65

Chapter 6 Higher Order Functions 69

6.1 Higher Order Functions 70
6.2 Abstractions, Currying and Partial Applications 71
6.3 fn and Abstractions 72
6.4 Overapplications 72
6.5 Programming with Higher Order Functions 73
Chapter 7 Assignments 80

7.1 Simple Assignments 80
7.2 Destructive Operations 81

Chapter 8 Vectors 84

8.1 Vectors 84
8.2 Lists and Vectors 85
8.3 Handling Vectors 87
8.4 Timing Operations 88
8.5 Hash Tables 90
8.6 Property Vectors and Semantic Nets 92
8.7 Native Vectors and Print Vectors 94

Chapter 9 I/O 98

9.1 Streams 98
9.2 Print Functions 99
9.3 Reading Input 101
9.4 Reading from a String 103
9.5 String Searching Text Files 104

Chapter 10 Macros and Packages 107

10.1 Macros 107
10.2 Changing the Order of Evaluation 110
10.3 Defining our own Notation 110
10.4 Packages 112
10.5 Packages that Use Packages 114
10.6 The Null Package and Macros 115
10.7 DSLs, Macros and Packages 117
10.8 Macro Management 118
10.9 Macroexpansion and Unpackaging 119
10.10 Working Inside a Package 120

Chapter 11 Exceptions and Continuations 122

11.1 Exceptions 122
11.2 Continuations 124

Chapter 12 Non-determinism 128

12.1 Non-deterministic Algorithms 128
12.2 Depth First Search 128
12.3 Recursive Descent Parsing 131
12.4 A Recursive Descent Parser in Shen 135

Chapter 13 Shen YACC 141

13.1 A Short History of Shen YACC 141
13.2 Programming in Shen YACC 142
13.3 The Empty Expansion and Guards 144
13.4 Non-terminals and Semantic Actions 145
13.5 Handling Lists in Shen YACC 147
13.6 Efficient Parsing 148
13.7 Consuming the Input 149
13.8 Limited Backtracking 150
13.9 Left Recursion 151

Chapter 14 Lambda Calculus 155

14.1 The Notation of the Lambda Calculus 155
14.2 Reasoning with the Lambda Calculus 157
14.3 The Church-Rosser Theorems 158
14.4 Conditionals 161
14.5 Weak Head Normal Form 163
14.6 Tuples 165
14.7 Numbers 166
14.8 Recursion and the Y-combinator 167

Chapter 15 Kλ 170

15.1 From Lambda Calculus to Kλ 170
15.2 Character Streams and Byte Streams 175
15.3 Manipulating Kλ 177
15.4 From Shen to Kλ via an Extended λ Calculus 178
15.5 Compiling Out Choicepoints 182
15.6 The Triple Stack Method 183
15.7 Factorising Kλ 185

Chapter 16 Writing Good Programs 188


Part II Working with Types


Chapter 17 Types 193

17.1 Types and Type Security 193
17.2 Modifying the Read-Evaluate-Print Loop 194
17.3 Lists, Vectors and Tuples 195
17.4 Lazy Types 197
17.5 The Small Arrow Type 198
17.6 Polymorphic Types 200
17.7 Equality Types 202
17.8 Stream Types 203
17.9 Types and Optimisation 204
17.10 Changing the Type of a Function 205
17.11 The Limits of Inbuilt Types 205

Chapter 18 Sequent Calculus 208

18.1 Sequent Calculus and Computer Science 208
18.2 Introducing Sequent Calculus 209
18.3 Propositional Calculus 211
18.4 First Order Logic (FOL) 215
18.5 Proof Trees and Goal Stacks 218
18.6 Implementing a Stack Based System: Proplog 219
18.7 Soundness and Completeness 222

Chapter 19 Concrete Types 225

19.1 Enumeration Types 225
19.2 Left and Right Rules 228
19.3 Handling Global Variables 230
19.4 Recursive Types (I): the Lambda Calculus 232
19.5 Recursive Types (II): Proplog 234
19.6 Dynamic Type Checking 235
19.7 Analytic and Synthetic Rules 238
19.8 Defining Polyadic Types 239

Chapter 20 Proof and Control 244

20.1 Controlling Timeout 244
20.2 Using spy to Trace Type Checking 245
20.3 Using Cuts 248
20.4 Type Annotations 249
20.5 preclude and include 250
20.6 Ordering Rules: Subtypes 251
20.7 Controlling Infinite Loops: Mode Declarations 254
20.8 Dependent Types 256
20.9 Creating a Tabula Rasa 258

Chapter 21 Abstract and Algebraic Datatypes 260

21.1 Concrete and Abstract Datatypes 260
21.2 Abstract Datatypes in Sequent Calculus 261
21.3 Proofs in a Hilbert System 263
21.4 Algebraic Simplification 268
21.5 Shen and ML 271

Chapter 22 Typed Shen YACC 278

22.1 The Big Arrow Type 278
22.2 Parsing Bytes to Numbers 279
22.3 Montague Grammars 282
22.4 YACC Structures 287
22.5 Abstract Operations 288
22.6 The Concrete Implementation 291
22.7 The Compilation of YACC Rules 291

Chapter 23 A Model Checker 298

23.1 An Introduction to Model Theory 298
23.2 Implementing a Model Checker 300
23.3 Dealing with Infinity 302
23.4 Super Quantification 305
23.5 Proof and Computability 307

Chapter 24 An Interpreter for Kλ 309

24.1 Formal Semantics 309
24.2 The Environment Model of Evaluation 310
24.3 The Basic SECD Machine 312
24.4 Computing with the SECD Machine 314
24.5 Adding δ Rules to the SECD Machine 321
24.6 Adding Lazy Evaluation to the SECD Machine 322
24.7 Adding Global Definitions to the SECD Machine 324
24.8 Quotation and Lexical Scope 326
24.9 List Processing in the SECD Machine 333

Chapter 25 Shen Prolog 338

25.1 A Short History of Prolog 338
25.2 Horn Clause Logic 339
25.3 Unification 342
25.4 Programming in Horn Clause Logic 346
25.5 Programming in Prolog 348
25.6 Shen Prolog 350
25.7 Implementing a Horn Clause Interpreter 356

Chapter 26 Compiling Sequent Calculus 362

26.1 The Anatomy of a Sequent Calculus Rule 362
26.2 Sequent Calculus as a Source Language 363
26.3 Enriched Horn Clause Logic as
an Object Language 368
26.4 Two Models for Compiling Sequent Calculus 367
26.5 Naïve Goal Oriented Compilation in Shen 369
26.6 Refining Goal Oriented Compilation 373

Chapter 27 Compiling Prolog 376

27.1 The Binding Vector 376
27.2 The Continuation 377
27.3 Eager vs. Lazy Dereferencing 377
27.4 Left Linear Horn Clauses 378
27.5 Implementing Unification 378
27.6 Coping with Exponential Code 380
27.7 The Twin Stack Method 381
27.8 Compiling the Head of the Clause 382
27.9 The Variable Case 384
27.10 The Negative Atom Case 384
27.11 The Negative Cons Case 384
27.12 The Positive Atom Case 385
27.13 The Positive Cons Case 385
27.14 Garbage Collection 388
27.15 Constructing the Continuation 389
27.16 Constructing a Horn Clause Procedure 391
27.17 Implementing the Cut 393
27.18 Implementing findall 397
27.19 Implementing assert(a/z) and retract 398
27.20 Optimising Shen Prolog Programs 398
27.21 Shen Prolog Performance 399

Chapter 28 The Semantics of L 403

28.1 An Overview of Our Approach 403
28.2 An Operational Semantics for L 405
28.3 An Interpreter for L 407
28.4 Compilation to Kλ and Semantics 408

Chapter 29 System S 416

29.1 Type Checking Applications 416
29.2 Type Checking Abstractions 417
29.3 Polymorphic Functions 418
29.4 Special Forms 419
29.5 Recursion, Cases, Patterns and Guards 420
29.6 Global Variables 423

Chapter 30 Type Safety 425

30.1 The Correctness of S 425
30.2 T 431
30.3 Procedure T* 435
30.4 The Equivalence of T and T* 441
30.5 T* in Shen 444


Appendices

Appendix A System Functions and their Types in Shen 452
Appendix B The Syntax of Shen 469
Appendix C The Next Lisp: Back to the Future 472

Bibliography 479

Index of System Functions Used in this Book 492

Index 494