Index

A

a conversion, 206 , 207 , 208 , 209 , 210
AB theorem, 284
abduction, 348
Abelson and Sussman, 35 , 68 , 96 , 156
abstract data type, 15 , 184 , 199 , 200 , 201 , 202
abstract programming, 184
abstraction, 84 , 85 , 86 , 87 , 88 , 91 , 147 , 205 , 207 , 208 , 209 , 215 , 218 , 219 , 220 , 223 , 231 , 236 , 395
abstractions rule, 269 , 271 , 275 , 276 , 277 , 280 , 297
Adams, 419
Aho, 137 , 419
Ait-Kaci and Podelski, 18
Allen, 82 , 419
amplification, 335 , 337 , 341
analytic, 170 , 171
answer literal, 244
applications rule, 268 , 270 , 271 , 276 , 280 , 281 , 297
applicative order, 40 , 43 , 44 , 45 , 210 , 211 , 236
arity, 40 , 210 , 214 , 218 , 219 , 325 , 342
array, 25 , 97 , 99 , 100 , 169 , 378 , 382
assembler, 27 , 31 , 123
assignment, 18 , 19 , 31 , 78 , 97 , 98 , 140 , 164 , 277 , 341
atomic statements, 107
attachment, 91 , 105
AUM, 9 , 35 , 250 , 251 , 252 , 254 , 255 , 256 , 257 , 258 , 259 , 260 , 262 , 265 , 412
automated deduction, 25 , 300 , 304 , 345
axiom, 192 , 194 , 196 , 247

B

b redex, 210
b reduction, 206 , 207 , 208 , 209 , 210 , 231
Backhouse, 156 , 419
backtracking, 110, 111, 112, 113, 117, 118, 121, 152, 221, 289, 337, 342
Backus, 35 , 419
backward chaining, 108
Baeten, 56 , 419
Barendregt, 25, 213, 236, 420
base case, 59, 60
base types, 145
Bayes Law, 374
Bendix, 56, 136, 425
BEP, 350
Bergstra, 56 , 419
best-first, 95
Bibel, 345 , 420 , 425 , 428
binary, 80 , 162 , 163 , 168 , 301 , 302
bindings, 240 , 281 , 342
boolean, 38 , 39 , 43 , 44 , 145 , 149 , 158 , 211 , 212 , 213 , 217 , 218 , 219 , 221 , 222 , 223 , 240 , 272 , 273 , 274 , 275 , 276 , 277 , 278 , 280 , 283 , 295 , 375 , 376 , 377 , 378 , 381 , 383 , 384 , 386 , 388 , 392 , 395
Boolos, 35 , 211 , 420
bound, 22 , 40 , 205 , 206 , 207 , 208 , 210 , 214 , 217 , 222 , 236 , 272 , 321 , 322 , 325 , 327 , 342
Boyer, 346 , 420
Boyer-Moore, 420
Boyle’s Law, 23
Bratko, 121 , 420
breadth-first search, 95
bubble sort , 88 , 90 , 96
Bundy, 56 , 136 , 345 , 420 , 421
Burstall, 68 , 421

C

Caduceus, 374
Caldwell, 69
Cardelli, 29 , 421
cases rule, 274 , 276 , 283 , 289 , 296
Cerrito, 421
Chang, 341 , 345 , 421
characterise, 20 , 23
Charniak, 121 , 374 , 421
choice point, 106 , 111 , 112 , 342
chronological backtracking, 12 , 110
Church, 20 , 22 , 24 , 25 , 26 , 27 , 204 , 209 , 210 , 211 , 307 , 323 , 420 , 421
Church-Rosser theorem, 210
Clarke, 345 , 427
class, 15 , 22 , 24 , 30 , 83 , 106 , 118 , 184 , 190 , 192 , 193 , 195 , 196 , 197 , 199 , 202 , 304 , 315 , 348 , 349
clause, 208 , 329 , 330 , 332 , 334 , 335 , 337 , 340 , 341 , 342 , 343 , 346
CLIPS, 374
closed lambda expression, 205
CNF, 329
combinator, 205 , 213 , 221 , 228 , 230 , 231 , 273 , 283 , 290 , 295 , 297
combinator rule, 273 , 274 , 275 , 283 , 289
committed choice, 289
compile, 27 , 29 , 31 , 46 , 56 , 123 , 131 , 132 , 136 , 137 , 150 , 204 , 218 , 221 , 236 , 267 , 305
complement, 163 , 301 , 302 , 328 , 335 , 337 , 340 , 342
complete, 40 , 109 , 111 , 113 , 114 , 119 , 121 , 130 , 145 , 161 , 223 , 236 , 268 , 274 , 315 , 323 , 327 , 334 , 335 , 337 , 340 , 341
computable, 18 , 23 , 24 , 26 , 131 , 167
conditional equations, 48
conditional rule, 272 , 273 , 281 , 283
conjunction, 107 , 108 , 112 , 169 , 342
conjunctive normal form, 329
cons rule, 272
cons cell, 26 , 82
consing, 71 , 72
constraint programming, 121
constraint satisfaction problem, 121
constructor function, 164
context variable, 248 , 249
context-free, 125 , 395
correctness condition , 291 , 292 , 293
Cresswell, 345 , 424
Current Lisp Interpretation, 257
currying, 85 , 86 , 147 , 214
CYCL, 105 , 426

D

Darlington, 68 , 421 , 429
decidable, 241 , 315 , 323
decision procedure, 315
declarative, 18 , 19 , 20 , 35
deductively typed, 157
default, 117 , 173 , 193 , 257 , 267 , 300 , 360 , 375 , 380 , 389 , 390 , 392 , 399 , 409 , 416
DENDRAL, 374
depth-first search, 95 , 289
dereferencing, 240
Diaz, 121
Diller, 137 , 182 , 237 , 422
distinguished symbol, 125 , 126 , 134
Doyle, 426
Duffy, 56 , 114 , 136 , 182 , 345 , 422
dynamic binding, 259
dynamic type checking, 143 , 144

E

eager evaluation, 29
EBL, 374
Edinburgh LCF, 30
eight queens problem, 120
enumeration, 157 , 181
environment, 32, 46, 97, 145, 216, 217, 267, 376, 381, 394
ephemeral variable, 253
equality rule, 272 , 273
equational specification, 45 , 47 , 48 , 75 , 76
equations, 22 , 26 , 46 , 47 , 48 , 49 , 56 , 57 , 58 , 60 , 62 , 207 , 211 , 212 , 213 , 214 , 224 , 236
error message, 42 , 43 , 46 , 144 , 147 , 150 , 221 , 267 , 377
error objects, 272
eval, 131
expansive, 300
expert system, 348 , 352
explanation function, 349

F

factorial, 26 , 29 , 57 , 58 , 59 , 65 , 150 , 273 , 401
Faé, 17 , 422
failure, 108 , 109 , 110 , 111 , 112 , 113 , 117 , 118 , 121 , 127 , 128 , 147 , 152 , 220 , 221 , 240 , 270 , 343 , 392
Federhofer, 374
Ferber, 374 , 422
Fermat test, 68
Feys, 343
Fibonacci, 60 , 61 , 68
Field, 35 , 69 , 84 , 222 , 422
finite state machine, 119
first-class objects, 83
first-order logic, 318
fixpoint, 90 , 213 , 315 , 316 , 326 , 327 , 329 , 330 , 334 , 337 , 377
formal parameters, 63 , 220
frame, 28 , 105
frame problem, 104
Franz Inc, 392
free, 27 , 30 , 49 , 78 , 121 , 125 , 136 , 143 , 205 , 207 , 208 , 209 , 217 , 236 , 269 , 281 , 318 , 319 , 328 , 335 , 341 , 395
fresh, 269 , 270 , 271 , 273 , 274 , 275 , 280 , 281 , 282 , 290 , 293 , 296 , 298 , 319 , 321 , 324 , 325
Functional Abstract Machine, 29
Futamura, 137

G

Gabriel, 35
garbage collection., 26
generalisation rule , 271 , 275 , 296
generic tactic, 317
Gentzen, 114 , 182 , 423
Giarratano, 374
Girard , 423
global, 97 , 98 , 140 , 169 , 227 , 380 , 392 , 424
goal, 56 , 109 , 110 , 111 , 112 , 118 , 121 , 209 , 268 , 270 , 305 , 337 , 342
Goldbach’s conjecture, 65 , 66 , 79
Gordon, 30 , 156 , 236 , 423
graceful labelling problem, 120
grammatical, 123 , 124 , 125 , 126 , 127 , 128 , 130
ground atoms, 239
Grune, 137 , 423
guard, 62 , 65 , 219 , 274
Guha, 105 , 426
Gunter, 423

H

h conversion, 206 , 208 , 209 , 236
Halting Problem, 69 , 211
Harrison, 35 , 69 , 84 , 222 , 422
hashing functions, 103
Haskell, 31 , 35 , 36 , 86 , 429
Hausner, 96
head abstraction, 262 , 263 , 264 , 265
help function, 59
Hendrix, 105 , 423
Henkin, 345 , 424
Henson, 68 , 424
Hett, 17 , 120 , 122 , 154
heuristics, 357 , 358
Hewitt, 121 , 424
higher-order, 27 , 83 , 87 , 88 , 94 , 96 , 117 , 134 , 139 , 316
hill climbing, 95
Hindley, 204 , 236 , 424
Hodges, 36 , 345 , 424
Horn clause, 239 , 240 , 242 , 243 , 246 , 248 , 250 , 251 , 252 , 254 , 255 , 257 , 262 , 263 , 265 , 416 , 417
Hughes, 18 , 96 , 345 , 424

I

implication, 107 , 108 , 115
inconsistent, 325
indirect proof, 307 , 325 , 326
INDUCT, 419
inference pattern, 108 , 110 , 112 , 113 , 116
infinite, 21 , 46 , 57 , 58 , 60 , 82 , 114 , 118 , 136 , 167 , 217 , 300
infix, 40
information hiding, 199
inheritance , 15 , 195 , 196 , 199 , 202
integrity condition, 290 , 293
intelligent agents, 12 , 15 , 371 , 372
internal expressions, 84
interpretation, 205 , 219
interpreter, 137 , 144 , 217 , 225 , 227 , 230 , 236 , 237
inverter, 54
isomorphic , 121 , 376

J

Jackson, 372 , 374 , 424
Jacobs, 137 , 423
Jefferies, 35 , 211 , 420
Johnson, 374 , 427
Jones, 56 , 137 , 236 , 424 , 427
Jorrand, 56 , 420 , 425 , 428

K

Kac, 69 , 425
Kernighan, 425
Kesner, 17 , 421
Khowarizmi, 19
Knight, 425
knight tour, 120
knowledge base, 352 , 354 , 355 , 372
Knuth, 48 , 56 , 96 , 136 , 425
Knuth-Bendix, 48 , 56 , 136
Kripke, 345 , 425

L

Lajos, 121 , 136 , 425
lambda calculus, 24 , 25 , 27 , 30 , 35 , 204 , 205 , 206 , 207 , 208 , 209 , 210 , 211 , 212 , 213 , 214 , 215 , 216 , 217 , 218 , 219 , 231 , 236 , 237
lambda convertible, 209 , 216
Landin, 29 , 237 , 425
Larch, 56
lazy evaluation, 29 , 153
leanTAP, 343 , 420
Lee, 341 , 345 , 421
left linear, 218 , 219
left recursive, 406
lemma, 317
Lenat, 105 , 426
let rule, 272 , 273 , 281
lexical binding, 259
lexical category, 125 , 127 , 128
linear recursion, 60
Linsky, 345 , 426
Lisp, 25 , 27 , 28 , 29 , 35 , 36 , 56 , 63 , 65 , 121 , 137 , 143 , 156 , 216 , 221 , 304 , 389 , 393 , 394 , 419 , 423 , 424 , 425 , 426 , 428
Lisp machines, 28 , 29 , 35
list, 25 , 26 , 27 , 28 , 30 , 58 , 67 , 70 , 71 , 72 , 73 , 74 , 75 , 76 , 77 , 79 , 80 , 82 , 83 , 86 , 87 , 88 , 91 , 94 , 97 , 99 , 100 , 101 , 103 , 108 , 110 , 111 , 112 , 113 , 119 , 124 , 126 , 127 , 128 , 131 , 132 , 134 , 139 , 143 , 145 , 146 , 149 , 150 , 151 , 157 , 162 , 163 , 167 , 169 , 218 , 219 , 220 , 267 , 270 , 271 , 272 , 275 , 276 , 277 , 278 , 279 , 299 , 301 , 324 , 325 , 330 , 332 , 337 , 344 , 346 , 375 , 376 , 377 , 378 , 379 , 380 , 381 , 382 , 383 , 384 , 385 , 392 , 395
list evaluation rule, 70
Liu, 121 , 426
Lloyd, 121 , 426
load, 36 , 52 , 121 , 158 , 163 , 267
local assignment, 78
logical constant, 319
Lopes, 345 , 426
Loveland, 345 , 426

M

m bound, 251
m expressions, 251 , 252
m reduction, 252
m abstraction, 251
m application, 251
macroscopic, 371
Maher, 56
Martelli, 426
Martins, 345
mathematical modelling, 371
McCarthy, 25 , 26 , 27 , 29 , 35 , 137 , 426
McDermott, 121 , 374 , 421 , 426
metaprogram, 123 , 131 , 132 , 134 , 136 , 137 , 216
MGU, 240 , 241 , 269
microscopic, 371
Milner, 30 , 156 , 423
Minsky, 105 , 427
Miranda, 18 , 35 , 82 , 429
ML, 18 , 29 , 30 , 35 , 36 , 137 , 156 , 164 , 216 , 304
mode declarations, 300
model, 22 , 24 , 25 , 29 , 30 , 32 , 40 , 60 , 91 , 100 , 217
modus ponens, 348
Moore, 346 , 420
Murch, 374 , 427
mutual recursion, 61 , 80 , 221
MYCIN , 352 , 374

N

natural kinds, 105
negation normal form, 340 , 342
Newell, 25 , 26 , 30
Newton’s method, 19 , 88 , 89 , 91
non-deterministic, 106 , 109 , 119 , 125
non-monotonic, 426
non-terminating, 65 , 79
normal form, 40 , 42 , 43 , 44 , 48 , 65 , 70 , 71 , 77 , 78 , 97 , 99 , 100 , 117 , 144 , 209 , 210 , 211 , 217 , 224 , 236 , 329 , 340 , 342 , 378 , 379 , 382 , 383 , 401
normal order, 210 , 211 , 217 , 236
Norvig, 95 , 105 , 372 , 374 , 427

O

O’Donnell, 56 , 427
occurs-check, 240 , 270
Ockham’s Razor, 372
or-gate, 54
OTTER, 56 , 346

P

parallel, 56
parameterised tactics, 317
parse tree, 124 , 126
parser-generator, 131
partial application, 86 , 147 , 208
partial evaluation, 137
pattern-directed, 30 , 63 , 218
pattern-matching, 30 , 218 , 219 , 220 , 236
patterns rule, 274 , 275 , 277 , 281
Paulson, 35 , 136 , 182 , 202 , 427
PCAI, 374
Peirce, 427
Peyton-Jones, 237
Plaisted, 56 , 422 , 427
PLANNER, 121 , 424
Plato, 143
Plauger , 425
polymorphic, 149 , 156 , 271
polytype, 149 , 156 , 167 , 300
pop , 110 , 111 , 139 , 345
postfix, 40
predicate , 318 , 319
prefix, 40 , 41
premises, 247 , 248 , 249
prenex, 324 , 325 , 326 , 327 , 329 , 342 , 345
prime, 61 , 62 , 63 , 65 , 66 , 67 , 68 , 79
primitive data structure, 277
primitive object, 223 , 278
pimitive rule, 268 , 273 , 277
priority rewrite, 48 , 56
procedural, 18 , 19 , 20 , 27 , 28 , 31 , 35 , 57 , 59 , 91 , 105 , 156 , 213
product, 28 , 30 , 76 , 77 , 87 , 88 , 131 , 141 , 146 , 147 , 148 , 151 , 236
production system, 104
programmable syntax, 398
Programmar, 137
Prolog, 14 , 18 , 120 , 121 , 122 , 304 , 305 , 345 , 420 , 428
proof checkers, 304
proof language, 305
proof systems, 117 , 315 , 345
proof theory, 307
proof tree, 109 , 110 , 111 , 114 , 342 , 349
property lists, 100 , 101 , 169
Proplog, 107 , 108 , 110 , 112 , 113 , 114 , 115 , 118 , 119 , 121 , 136 , 181 , 301 , 343
propositional calculus , 307 , 318 , 328 , 343
propositional form, 318
Prospector, 374
prosthetic clauses , 263
prosthetic literals, 263 , 264 , 265
provability, 115 , 117 , 157
push, 110

Q

Qi printer, 398
Qi reader, 396
quantifier, 105 , 318 , 319 , 320 , 321 , 324 , 325 , 326 , 327 , 328 , 329
Quillian, 100 , 105 , 427

R

Ramsay, 345
random, 51 , 269 , 383
range, 45 , 121 , 345 , 358 , 359 , 361 , 362 , 392
rational hedonism, 357 , 360 , 366
read-check-evaluate-print loop, 144
read-evaluate-print loop, 38 , 144 , 217
recognisor, 123 , 126
rectified, 326 , 327
recursion, 26 , 57 , 59 , 61 , 63 , 68 , 80 , 91 , 221 , 127 , 128 , 163 , 214 , 222 , 273
recursive case, 59
reduction strategy, 210 , 217
Reeves, 345 , 427
refinement, 114 , 115 , 116 , 157 , 158 , 160 , 161 , 162 , 168 , 169 , 204 , 304 , 305 , 307 , 308 , 315 , 316 , 319 , 320 , 322 , 324 , 335 , 337 , 345 , 396
Reiter, 427
reliability problem, 305
Riley, 374
Ritchie, 31
Robinson, 30 , 241 , 422 , 427
rule abstraction, 170 , 306
Russell, 95 , 105 , 372 , 374 , 427

S

SASL, 29 , 63
Schapiro, 35 , 121 , 428
Scheme, 35 , 63 , 121 , 430
search clauses, 249
search literal, 248
search procedure, 249
SECD, 29
Seldin, 204 , 236 , 424
self-evaluating, 38 , 39 , 72 , 217 , 278
semantic nets, 100 , 101
semantics, 221 , 223 , 225 , 280 , 420
sequent, 22 , 25 , 114 , 115 , 116 , 137 , 146 , 157 , 158 , 160 , 161 , 207 , 221 , 268 , 269 , 270 , 271 , 272 , 273 , 274 , 275 , 276 , 293 , 324 , 326 , 330 , 340
sequents rule, 268 , 270 , 271 , 272 , 273
Sestoft, 137 , 424
SETL , 82 , 428
side condition, 115
side-effect, 42 , 97 , 100 , 380
Simon, 25 , 26 , 30 , 428
SISAL, 56
skolem constant, 325
skolem function, 325
skolemisation, 324 , 325 , 326 , 327 , 328 , 345
Sloman, 18 , 428
slots, 42 , 105
SML , 18 , 35 , 137 , 156 , 164 , 216 , 304
Smullyan, 345 , 428
SNOBOL, 30
Sondergaard, 137 , 424
sound, 19 , 31 , 113 , 114 , 126 , 305 , 323 , 334 , 337
spaghetti program, 140
special forms, 272
specialisation rule, 271
spreading, 92 , 98
spreadsheet, 91 , 92 , 93 , 98
square root, 19 , 61 , 83 , 89 , 90 , 384
stack, 110 , 111 , 112 , 118 , 199 , 342
standardisation apart, 243
Staples, 121 , 426
start state, 95
starved, 47
state successor function , 95
static type checking, 144
statically eliminable, 118
Steele, 392
Sterling, 121 , 428
Stickel, 121 , 345 , 428
stream, 21 , 28 , 82 , 94 , 167 , 168 , 305
strict evaluation, 44 , 45
strongly typed, 144 , 156 , 157
structure, 14 , 25 , 26 , 27 , 63 , 72 , 82 , 105 , 107 , 124 , 131 , 132 , 153 , 184 , 185 , 187 , 189 , 190 , 192 , 201 , 205 , 318 , 319
subformula property, 171
subgoal, 109 , 110 , 121 , 342
subject reduction, 278
subsumption , 340 , 341
subtype, 101 , 196
sugar functions, 40 , 202 , 397 , 399
superclasses, 197 , 199 , 202
surveyable, 359 , 361
synonyms, 159 , 160 , 353 , 359
syntactic fiction, 397 , 399
syntax, 45 , 112 , 123 , 204 , 307 , 319 , 395 , 420
synthetic, 170
system functions, 40 , 65 , 101 , 138 , 145 , 223 , 389

T

tableau, 307 , 324 , 325 , 326 , 340 , 341 , 342 , 343 , 345
tactic, 311 , 313 , 315 , 316 , 317 , 318 , 334 , 337 , 344 , 345 , 350 , 351 , 352 , 360
tactical, 316
tail recursion, 60
Tarver, 6 , 17 , 35 , 100 , 101 , 102 , 103 , 104 , 136 , 137 , 155 , 318 , 345 , 394 , 422 , 428 , 429
tautology, 340
Taylor, 237 , 423
Tecuci, 374 , 429
terminal, 125 , 126 , 127 , 132 , 133 , 134
theorem, 56 , 113 , 114 , 119 , 209 , 210 , 211 , 278 , 279 , 304 , 305 , 315 , 324 , 334 , 337 , 342 , 343 , 345 , 346 , 420
theorem-prover, 113 , 114 , 119 , 304 , 305 , 334 , 337 , 345 , 346
thinning, 317 , 318
Thompson, 31 , 35 , 429
throw-away design , 139
top down parsing, 126
top level, 38 , 39 , 40 , 41 , 51 , 52 , 90 , 92 , 112 , 117 , 138 , 144 , 145 , 158 , 267 , 402
tracking, 110 , 111 , 112 , 113 , 117 , 118 , 121 , 152 , 221 , 289 , 337 , 342 , 402 , 426
tree recursive, 61 , 68
tuple, 148 , 151 , 159 , 167 , 212 , 213 , 222 , 236 , 376 , 386
Turing, 20 , 21 , 22 , 25 , 27 , 35 , 36 , 211 , 223 , 323
Turing machine, 21 , 22 , 36
Turner, 29 , 30 , 35 , 237 , 421 , 424 , 429
type discipline, 144
type error, 30 , 143 , 144 , 145 , 146 , 149 , 150 , 163 , 267 , 299 , 301
type operator, 145 , 147 , 167

U

Ulam, 69 , 425
Ullman, 137 , 419
unification, 30 , 121 , 137 , 240 , 242 , 243 , 250 , 251 , 252 , 256 , 257 , 261 , 262 , 263 , 269 , 272 , 280 , 287 , 300 , 301 , 302 , 324 , 328 , 329 , 345 , 414 , 415 , 416 , 417 , 429
unifier, 240 , 270
UNIX, 12 , 31 , 56

V

valid, 107 , 324
value, 14 , 18 , 24 , 28 , 29 , 42 , 43 , 44 , 55 , 57 , 59 , 60 , 63 , 66 , 67 , 78 , 80 , 81 , 85 , 87 , 89 , 90 , 91 , 92 , 93 , 97 , 98 , 99 , 100 , 104 , 126 , 140 , 169 , 220 , 240 , 268 , 277 , 281 , 360 , 361 , 368 , 376 , 378 , 387 , 392
variable occurrence restriction, 49
verified objects, 165

W

Wadler , 35 , 56 , 420
Wadsworth, 30 , 156 , 423
Wardrop Principle, 356 , 371 , 422
wff, 307 , 319 , 320 , 321 , 325 , 326 , 327 , 329 , 335 , 353 , 354 , 361 , 362 , 363 , 364
Wikstrom, 35 , 136 , 182 , 202 , 430
wildcard, 52 , 53 , 218
Winograd, 105 , 420 , 430
Wright, 121 , 430

Y

Y-combinator, 213 , 214 , 215 , 221 , 222 )