Index

∈ (element of), 13 ∩ (intersect), 13 ∪ (union), 13 ⊆ (subset), 13 × (ordered pairs), 13 ∃ (there exists), 12 ∀ (for all), 12 ⊃ (implies), 12 ∧ (and), 12 ¬ (not), 12 iff (if and only if), 12 [[e]] (meaning of e), 25 A[[M]]η, 152, 283, 369 ⊧ (satisfies, implies), 158, 283, 290,

414

⊢ (provable), 35, 38, 162, 259 ⊢^{(emptyI ,E)} , 296

= (equal), 12 =_{ax}, 77, 339 =_{den}, 77, 339 =_{op}, 77, 339 =^{def} (defined to be), 12, 58, 65 ≡ (syntactic equality), 12, 47 ::= (production in grammar), 12, 22 ≃ (equal if either defined), 77, 368 ≅ (isomorphic) See isomorphism. ∼_{E,Γ} , 175 [a]_{∼}, 173 A/∼, 173

→ (function), 8, 18 ⇀ (partial function), 19 → (reduction), 7, 75, 79 → →, 7, 79 ← ←, 205 → → ∘ ← ←, 205

→^{eager} , 93

→^{lazy} , 89

→ →^{left}, 87

⇒, 91 ⇒ ⇒, 92 →_{R}, 204

⟶^{R,β,p,lab_{+}} , 564

eval , 394 exec , 395

↦^{exec} , 399

M ↓ (defined), 359, 368 M ↑ (undefined), 368 d ↑ d′ (consistent), 348

≤_{D → E}, 314 ≤_{D × E}, 310 ≤_{den}, 354 ≤_{op}, 354 ⊥_{D} (least element), 309 ⋁S (least upper bound), 309

f∘g (function compostion; λx. f(g(x))),

20

f; g (composition in diagrammatic order; λx. g(f(x))), 449 f_{i,j} (composition along ω -chain), 514 f(S) (function applied to set of argu-

ments), 312

S(d) (set of functions applied to argu-

ment), 314

λx: σ. M (lambda notation for function),

3

MN (application of function expression to argument), 4,5

M^{n}N (iterated application), 66 M · N (strict application), 402 M ⋄ N (strict composition), 402 M|n⃗ (subterm at a position), 206 [N/x]M (substitution) , 150 ⟨M_{1}, …, M_{n}⟩ (tupling on terms), 97 ⟨h_{1}, …, h_{n}⟩ (tupling on arrows of cat-

egory), 470

σ_{1} × … × σ_{n} (iterated product type),

97

σ^{k} (iterated product of single type),

97

⌈n⌉ (numeral for number n), 50

(→ Intro) typing rule, 243, 622, 628 (→ Elim) typing rule, 244, 622, 628 (→ U_{1}) type formation, 620 (→ Cong) type equation, 695 (→ <:) subtyping, 707, 720 (× Intro) typing rule, 248 (× Elim) typing rule, 248 (+ Intro) typing rule, 249 (+ Elim) typing rule, 249 (⌊ ⌋ Intro) typing rule for lifted type

σ_{⊥}, 135, 402

(⌊ ⌋ Elim) typing rule for lifted type

σ_{⊥}, 135

(∀ Intro), 639; See (Π Intro). (∀ Elim), 639, 658; See (Π Elim). (∃ Intro) typing rule, 681 (∃ Elim) typing rule, 681 (= <:) subtyping, 746 (⊥ <:) subtyping, 750 (<: context) structural rule, 751 (abs) type inference, 782 (acong) for approximations, 335 (add hyp) type inference, 782 (add var) equational rule, 162, 258 (add var) typing rule, 243, 469, 620,

696

(app) type inference, 782, 803 (asg) for Hoare logic, 416 (asym) for approximations, 335 (α) equation, 6, 53, 259 (α)_{Π} equation, 628 (α)_{∃} equation, 683 (bot) for approximations, 335 (botf ) for approximations, 335 (β) equation, 6, 7, 53, 259, 268 (β)_{Π} equation, 628 (β)_{∃} equation, 682 (case)_{1} equation, 123, 264 (case)_{2} equation, 123, 264 (case)_{3} equation, 123, 125, 264 (cond) for Hoare logic, 416 (cong) equational rule, 164 (conseq) for Hoare logic, 415 (cst) typing axiom, 242, 621, 628, 782,

793

(cst U_{1}) type formation, 620 (empty I ) equation, 296 (empty E) equational rule, 296 (empty context) structural rule, 619 (eq) for approximations, 335 (η) equation, 54, 81, 259, 268 (η)_{Π} equation, 629 (η)_{∃} equation, 683 (fcong) for approximations, 335 (fix) equation, 62 (fix)_{alt} alternate axiom, 84 (fpind) for approximations, 336 (gen) type inference, 792 (inst) type inference, 792 (let) equation, 636 (let) typing rule, 635, 792 (let ⌊ ⌋) equation, 135 (lookup) equation, 393 (μ Intro) typing rule, 127, 741 (μ Elim) typing rule, 127, 741 (μ <:) subtyping, 746, 749 (μ ⊥) type equation, 749 (μ unique) type equation, 749 (nonempty) equational rule, 177, 293 (null) equation, 265, 270 (null Elim) typing axiom, 250 (ν) equational rule, 259 (ν)_{Π} equational rule, 629 (proj ) equation, 51, 264, 270 (Π Intro) typing rule, 615, 622, 628,

693

(Π Elim) typing rule, 616, 622, 628,

693

(Π U_{2}) type formation, 620, 693 (Π <: Intro) typing rule, 752 (Π <: Elim) typing rule, 752 (Π <: F Intro) typing rule, 756 (Π <: F Elim) typing rule, 756 (Π Cong) type equation, 695 (ΠF <: Intro) typing rule, 761 (ΠF <: Elim) typing rule, 761 (rec ind) equational rule, 72 (record Intro) typing rule, 716 (record Elim) typing rule, 716 (record ext) equation, 717 (record selection) equation, 96, 716 (record <:) subtyping, 715 (ref ) equation, 35, 53, 162, 258 (ref <:) subtyping, 707, 720 (seq) for Hoare logic, 415 (sp) equation, 52, 81, 264, 270 (store_{⊥} Elim) typing rule, 402 (subst) equational rule, 162, 260 (subsumption) typing rule, 709, 719 (subsumption eq) equational rule, 711 (sym) equational rule, 71, 162, 258 (Σ Intro) typing rule, 693 (Σ Elim) typing rule, 693 (Σ U_{2}) type formation, 693 (Σ Cong) type equation, 695 (Σ first) equation, 695 (Σ second) equation, 695 (Σ sp) equation, 695 (term eq) type inference, 784 (trans) equational rule, 35, 53, 162,

258, 335

(trans <:) subtyping, 707, 720 (type eq) typing rule, 622 (type label) equation, 712 (TypeCond) typing rule, 645 (Type → Type <:) subtyping, 761 (U_{1} context) structural rule, 619 (U_{i} type context) structural rule, 619 (U_{1} ⊆ U_{2}) typing rule, 620, 623 (U_{2} ⊆ U_{1}) typing rule, 625 (U_{1}: U_{2}) typing rule, 623, 625, 699 (U_{1} = U_{2}) typing rule, 625, 700 (unfold) type equation, 126, 741 (unit) equation, 122, 264, 270 (unit Intro) typing axiom, 250 (update) equation, 393 (up/dn) equation, 127 (while) for Hoare logic, 418 (with) typing rule, 759 (ξ) equational rule, 258, 301 (ξ)_{Π} equational rule, 629 (var) typing axiom, 243, 620, 628, 782 (var)_{alt} typing axiom, 624

1-section theorem, 574

anf (M), 340 A_{⊥}, 310 A_{0} -valid, 421 A_{pcf}, 148 abstract syntax, 21 acceptable enumeration of p.r. func-

tions, 356

acceptable meaning function, 539 Ada programming language, 607 adequacy of semantics, 77, 344 ad hoc polymorphism, 613 adjoint situation, 467 admissible (inclusive) predicate, 337,

339

admissible logical relation, 540

with product types, 560 Alg_{Σ} , 449 Alg_{Σ,E}, 449 algebra, 145, 151 algebraic

CPO, 348 datatype, 145 function, 148 function type, 149 specification, 147, 157, 161, 188 term, 150

alias, 392

ambiguous grammar, 23

antecedent, 163 antisymmetry, 18 application in lambda notation, 3 applicative structure, 280 in a category, 493 extensional, 281 impredicative, 633, 663 polymorphic, 631, 663 type:type, 633

appropriate (environment and store),

435

approximate normal form, 340 approximation theorem, 340 arrow of a category, 447 associativity

left- or right-, 24 associativity of composition, 21 axiom, 35 axiomatic semantics, 6

B_{⊥}, 310

base case of induction, 27 base type (in λ^{→}), 241 BCPO, 353 beta-reduction, 7 bijective function, 20 binary tree, 30 Böhm tree, 276, 341 bool

as sum type, 124 in λ^{→,∀}, 642 in PCF, 47, 49, 71

bound variable, 4, 243

bounded complete CPO, 353 bounded polymorphism, 751

C[ · , …, ·], 116 C[ ], 77 C^{E}, 520 C^{op}, 451 C_{Σ}(E), 462 C_{→,∀}, 653 C programming language, 584 C++ programming language, 607 call-by-value reduction, 93 canonical rewrite system, 205 carrier of multi-sorted algebra, 148, 151 cartesian

closed category, 280, 293, 458, 459,

460, 461 closed functor, 464 product, 14

of CPOs, 310 of modest sets, 359

Cat , 453 categorical

combinator, 474 duality, 457 function space (exponential), 454 product, 454 sum (coproduct), 457

category, 447 formal (in a typed language), 652 generated by a theory, 462 of embeddings, 520 of projections, 520 of types and terms, 653

cc-functors, 464 CCC See cartesian closed category. CCC (category of cartesian closed cat-

egories), 464

Church’s theory of simple types, 262 Church’s thesis, 105 Church-Rosser property, 8, 80, 556 Church numeral, 642 CL(Σ), 297 closed expression, 4 closure, 667 coalesced sum, 326 cocone in a category, 511 codomain of function, 19 codomain of morphism, 447 coherence, 286, 475, 705 combinator, 298 combinatory

algebra, 227 algebra, partial, 368 logic, 222, 226, 297 model condition, 297, 298 structure for λ, record, 729 term, 297

comma category, 466, 596 commuting diagram, 448, 510 compact element of CPO, 347 complete

induction, 29 partial order (CPO), 239, 305, 309

bounded complete, 353

pairwise consistent complete, 348 pointed, 309

predicate, 588 proof system, See completeness.

completeness, 157 deductive, 172 least model form, 172 for λ^{→}

with empty types, 295

without empty types, 293 for multi-sorted algebra, 161, 172

completion, 228 composite number, 29 composition, 17, 19

diagrammatic order (f; g), 449 function and relation, 20 in a category, 447 set closed under, 106, 110

compositionality, 74, 388 computable

function on numbers, 105 function on modest sets, 359 increasing sequence, 378 test, 377

computational adequacy, 76, 77, 344 cone in a category, 510 confluence, 8, 80, 205, 556

from a term, 227 congruence proof rule

in algebra, 164 congruence relation, 70, 173

partial, 177 consequent, 35, 163 conservativity, 260, 265, 266 consistent, 193, 199, 200

elements of CPO, 348 lifted types and fixed-points, 133 proof system, 72, 78 set of equations, 163 sums and fixed-points, 125

constant symbol in algebra, 149 in λ^{→}, 241

constructor of a datatype, 190 of an algebra, 192 context (term with hole), 77

evaluation, 114 multiple holes, 116 σ, τ -context, 560 typing; See typing context

contextual theory, 649 continuous function, 239

on CPO, 312 hierarchy, 238, 318 on lifted CPO, 313 of several arguments, 316, 317

contractive, 750 contravariant functor, 455 conversion, 205 covariant functor, 455 CPO, 239, 305, 309

bounded complete, 353 pairwise consistent complete, 348 pointed, 309

Cpo , 449, 463 Cpo_{⊥}, 452, 463 Cpo_{⇀}, 520 Cppo , 464, 520 critical pair, 216, 221

trivial, 221 Curry-Howard isomorphism, 252, 615 currying, 55, 321 Curry type inference rules, 782 Curry typing, 770

D^{C}, 456 D_{⊥}, 310 Δ^{prj} , 519, 523 dag (directed acyclic graph), 775 datatype, in ML, 131, 194 datatype induction, 192 deductive completeness, 172 definable function

implicitly, 50 partial function, 110 in PCF, 106

denotation, 50, 73 denotational

equivalence, 77 semantics, 6, 73, 388

dependent types, 614 derivation tree, 22 derived inference rule, 56, 163 Diaconescu cover, 503 diag(A), 367 diagonal functor, 468 diagram in category, 448, 510 directed-complete predicate, 588 directed subset of a CPO, 239, 309 discrete order, 308 disjoint union (sum) type, 122, 239,

303

domain of definition, 19 of function, 19 of morphism, 447 ordered set of values, 305, 308

dynamic lookup, 740, 748 dynamic scope, 60

e_{n}, 666 η[x ↦ a], 156 η_{∼}, 174 eager evaluation, 46, 86 eager reduction, 93 effective CPO, 378 elimination context, 354, 559 embedding, 519 embedding-projection pair, 519 empty set, 14 empty types, 295, 664 enumeration types, 124, 125 environment, 73, 152, 283

satisfying sort assignment, 152 satisfying type assignment, 283 model condition, 283

equalizer in a category, 457, 511 equation

between algebraic terms, 158 between typed lambda terms, 258

equational logic, 145 equivalence class, 173, 546 equivalence relation, 18, 161, 173 erasure function (Erase), 658, 673, 728,

766, 767, 790

evaluation context, 114 evaluation partial function (eval), 75,

84

existential type, 614, 680 explicit typing for untyped term, 777 exponential (function) object, 454 expressive (in Hoare logic), 424 extended equation, 295 extensional

applicative structure, 281 Kripke, 494 impredicative, 664 polymorphic, 632

collapse, 547 extensionality, 76, 302

for sets, 14

F -algebra, 512 F -bounded polymorphism, 755 final algebra, 147, 195 finitary retraction, 669 finite (compact) element of CPO, 348 first-order

dependent products, 614 function, 148 function type, 149

fix^{[n]} F , 307 fixed-point

induction, 336 of function, 61 of functor, 513 operator, 61, 306, 318, 381

untyped, 96 untyped eager, 96

flat CPO, 310 floor function, 710 formulas-as-types, 252, 614, 640, 649 free variable, 4 full abstraction, 78, 345 full set-theoretic function hierarchy, 284 full subcategory, 449 function, 18

composition, 17 object (in category), 454 space functor, 452 symbol (in algebra), 149

functor, 452 category, 456 definable, 653

FV (M ), 4, 53

Γ (sort/type assignment), 240 Γ, x: s, 150, 240 Γ ▷ M: τ, 240 Γ ▷ M = N: τ, 258 M ↔_{R} N [Γ], 205 Γ ▷ τ, 649 Γ ⊢ M: σ, 241 Γ_{f}, 470 Γ_{M}, 245 Gandy hull, 547 general product (Π) type, 613 general sum (Σ) type, 613 generated algebra, 195 generated semantics, 195 global element

functor into Set , 595 of category, 486 of Kripke model, 492

Gödel’s T , 571 Gödel numbering, 358 graph of function, 18 ground

instance of equation, 186 instance of term, 186 substitution, 186 term, 186

halting problem, 112, 113 Haskell programming language, 607 head normal form, 110 height of a tree, 30 Henkin model, 280

for higher-order logic, 292 impredicative, 633, 663, 664 polymorphic, 633 type:type, 633

hereditary permutation, 538, 544 higher-order logic, 292, 295 higher-order subtype bounded polymor-

phism, 755

holds (formula… in model), 158 hom-set Hom(a, b), 449 homomorphism

between algebras, 179

between applicative structures, 281

imperative programs, 387 implementation (model with standard

observables), 581

implication, semantic, 161 implicit typing, 782 impredicative polymorphism, 611, 625,

639, 700

inclusion, 458 inclusive predicate, 337, 339 inconsistent (See consistent.)

proof system, 72

sums and fixed-points, 125, 133, 463 index of p.r. function, 356 induction, 27

fixed-point, 336 hypothesis, 27, 29, 150 on natural numbers, 27 on proofs, 34 on terms, 32, 150 recursion, 73 well-founded, 38

inequational full abstraction, 354 inference rule, 35

derived, 56, 163 inheritance, 706, 748 initial

algebra, 147 for class C, 181 for equations E, 183 semantics, 191

F -algebra, 512 weak, 652, 654 object, 456 type, 297

injective function, 20 instance relation on typings, 771 intended model, 183 intersection, 15 intrinsic preorder, 377 invariant

of while loop, 418 isomorphism (≅), 12, 17

and recursive types, 127 between algebras, 181 between applicative structures, 281 in a category, 450 of modest sets, 360 of partial equivalence relations, 366 recursive, 360

K combinator , 297, 788 K(D), 348 Kleene normal form, 112 Knuth-Bendix completion, 228 Knuth-Bendix test, 228 Kripke

applicative structure, 491 lambda model, 494 logical relation, 590

k-tuple, 16

L–value, 389 λ^{→}, 237 λ\overrightarrow{t}, 769 λ^{→,×}, 237 λ^{→,×,+} , 237 λ^{→,Π} , 620, 627 λ^{→,∀}, 639 λ^{→,Π,Σ} , 692 λ\overrightarrow{<:} , 706 λ_{<:}^{→,record} , 714 λ_{<:}^{→,record,μ}, 740 λ⟨x: σ, y: τ⟩. M, 59, 66 lab(M), 342 lab_{+(0 )} , 563 lab_{+,0} , 563 lab_{+} , 563 lab_{0} , 563 label constants, 729 labeled

fixed-point operator, 342, 563 reduction, 563 positive, 563 term, 342, 563

lambda– abstraction, 3 algebra, typed, 301 calculus, 5 definable, 543 expression, 3 interpretation, 658 term, 3 late binding, 740, 748 lazy evaluation, 46, 86 lazy normal form, 89 LCF, 334 least

fixed point, 318

model completeness, 172 model property, 172 upper bound, 309

left– linear rewrite rule, 222 most evaluation, 46, 85, 86 normal rewrite rules, 272, 570 adjoint, 467 inverse, 519 Leibniz equality, 262 length of a lambda term, 637 let-depth of term, 637 let-reduction, 636 lexicographic order, 40, 210, 797 lifted

function, 313 set, 309 type, 122, 132, 401 lifting functor, 452, 514

limit in a category, 510 linear rewrite rule, 222 list datatype, 196 locally

confluent, 216, 559 continuous, 526 determined ω -colimits, 524 monotonic, 526

logical partial equivalence relation, 545 partial function, 544 relation, 536

on environments (R^{Γ}(η_{1}, η_{2})),

538, 736 satisfies (β), 547

logic for computable functions (LCF),

334

loose semantics, 191, 195

μ: c → Δ, 511 μ: Δ → c, 511 μt.σ, 126 m, n-function, 470 many-sorted algebra, 152 meta-language, 21, 47, 389 minimal element, 39 minimization, 98, 106, 110 Miranda programming language, 607 ML programming language, 11, 390,

607, 635, 766 datatype, 131, 194 let declaration, 635 type inference problem, 791

model (See also Henkin…)

of a logic, 279 of λ^{→}, 279 untyped lambda calculus, 659, 666

modest set, 238, 355, 357

category of (Mod ), 449 monotonic function on partial order,

312

morphism (arrow) of a category, 447 most general substitution, 220 multi-sorted algebra, 152 mutual recursion, 63 N_{⊥}, 310 natural deduction, 251 nat

as recursive type, 128 in λ^{→,∀}, 642 in PCF, 47, 49, 71

Newman’s lemma, 227 non-overlapping rewrite system, 222 nonempty types, 293, 664 noninformative, 134 nonlogical axioms, 37 nonterminals, 22 nontrivial model, 294 nonvoid sort in algebraic signature, 178 normal form, 8, 80, 205, 268 normalization, 8, 553 n-tuple, 16 numerals, 47, 50 numeric function, 106 numeric partial function, 110

O (order of); O(f(n)), 786, 806 O-category, 518 O-colimit, 521 ω -category, 515 ω -chain, 514 ω -chain CPO, 312 ω -chain in a CPO, 312 ω -complete pointed category, 515 ω -continuous, 515 ω^{op} -chain, 517 object-oriented programming, 740 object language, 21, 47 object of a category, 447 observable type, 68, 78 observable value, 68 observational congruence, 77 observational equivalence, 77 observationally equivalent models, 582 observer of a datatype, 190 one-step reduction, 79 one-to-one function, 20 operational equivalence, 77 operational semantics, 6, 387, 388 operator of a datatype, 190 opposite category, 451 order (collection of types), 9 ordered pair, 14, 15 orthogonal rewrite systems, 568 ϕ_{i} (ith partial recursive function), 356 pairwise consistent complete, 348 pairwise consistent subset of CPO, 348 parallel-or, 113, 345, 574 parallel reduction, 223 parametric polymorphism, 613, 645 parse tree, 22 partial

applicative structure, 729 combinatory algebra (pca), 305,

368, 734 correctness assertion, 389, 413 enumeration function, 357 equivalence relation (per), 355, 364,

365, 545, 718, 734 interpretation, 735 model, 663, 672 notation n: R for per R, 367

function, 19, 311 order, 18, 308 recursive function, 111 surjection, 575

recursive, 576 pass-by-reference, 440 pass-by-value, 440 PCF, 45 pcf_{+,0} -reduction, 566 pcf_{+} -reduction, 566 PCPO, 348 per (See partial equivalence …) permutation invariant, 544 Pfn , 525 pointed

CPO, 309 effective CPO, 381 predicate, 588

point of a category, 486 polymorphic

composition, 609 function, 609 identity, 610 lambda calculus, 611

position in a term, 205 positive labeled reduction, 563 powerset, 16 pre-fixed-point, 325 pre-term

of λ^{→}, 255, 269 of λ^{→,Π} , 621, 657 of λ^{→,Π,Σ} , 692 precedence, 24, 25

in type expressions, 237 predecessor, 100 predicate, 18 predicative polymorphism, 611 prefix order, 308 preorder, 707 prime number, 29 primitive recursion, 101, 106, 110, 571 primitive recursive function, 112 principal function symbol, 206 principal typing, 777, 783 product category, 450 product functor, 452 program (closed term of observable type),

68, 581

PR, 356 Proj_{i}^{a_{1} ×... × a_{n}}, 470 Proj_{i}S, 310, 312 projection, 519 proof, 35, 162

from assumptions, 38

from nonlogical axioms, 38 proper function symbol, 149 provable equation, 162 provably total functions of a theory,

641

Pω, 666

queue, 200 quotient

algebra, 173

applicative structure, 546 Henkin model, 548

R–value, 389 R, β, proj , lab_{+} , 564 range of function, 19 reachable algebra, 195 reachable semantics, 195 records

combination, 759 concatenation, 759 in λ^{→} or PCF, 96 with subtyping, 713

recursion theorem, 375 recursive

embedding, 576 function, 105

hierarchy, 238 hierarchy over modest sets, 361 on modest sets, 238, 359 in PCF, 105

isomorphism, 360 types, 122, 126, 739

redex, 49, 268 reduction, 6, 79, 268, 629

axiom, 49, 75 call-by-name, 85 eager (call-by-value), 86 lazy, 86, 89 left-most outer-most, 85, 87 one-step, 204, 268 parallel, 223 strategy, 84

reflexivity, 18 related environments, 736 relation, 17 relative completeness, 423 representation of CCC, 464 result (closed term of …), 69 retract, 578, 665 retraction, 665 rewrite rules, 145, 203 right adjoint, 467 rule of consequence

for Hoare logic, 415 Russell’s paradox, 14, 236

S combinator , 297 Σ (signature), 149, 241 Σ_{→}, 242, 247 Σ-CCC, 468 satisfaction

in CCC, 480 equation by lambda model, 290 equation by per interpretation, 737 formula by model, 158, 290 Hoare logic, 414 partial correctness assertion, 414 by a set of algebras, 158 of set of formulas, 158 of sort assignment, 152 of type assignment, 283

scone of a category, 587, 595 scope

dynamic, 60 static, 7, 54, 59

search, 99 second-order lambda calculus, 611 semantic functions, 405 semantics of programs, 69 semantic theory, 176 semi-unification, 806 separated sum of CPOs, 326 sequences

finite sequences (S^{+} ), 311 finite and infinite (S^{∗}), 311 infinite sequences (S^{∞}), 311

sequential-or, 113 set, 13 Set (category of sets), 449 set-theoretic function hierarchy, 238, 282 set union, 15 signature

for λ^{→}, 241 for λ\overrightarrow{<:} , 706 for multi-sorted algebra, 149 polymorphic, 620

simple semantics (of types), 709, 784 simply-typed lambda calculus, 237 simultaneous substitution (exercise), 160 single-sorted algebra, 152 singleton set, 14 small category, 451 smash product, 326 sort (in algebra), 145, 149 sort assignment for algebraic terms, 149 soundness, 37, 74, 157

for CCC’s, 480 for λ^{→}, 290 for multi-sorted algebra, 161, 165 of typing rules, 288

specification of algebraic datatype, 161,

188

start symbol, 22 static scope, 7, 54, 59 step function, 349 store (“memory state”), 387, 388, 392 strict function application, 402 strict function on CPO, 313 string, 42 strong induction, 29 strong normalization, 8, 268, 553, 770 strongly confluent reduction, 224 structured operational semantics, 87 subcategory, 449 subject reduction property, 268, 629 subquotient of a set, 366 subscone, 596 subset, 16 subset interpretation, 732 substitution, 6, 53

as environment, 159

identities, 54

inference rule, 162, 169, 260 lemma, for algebra, 156 lemma, for CCC’s, 478 lemma, for Henkin models, 290 on algebraic terms, 150 on lambda terms, 6, 53 on PCF terms, 54 on type assignment, 771 on types, 771

subtype, 703 subtype-bounded polymorphism, 751 sum types, 122, 123 surjective function, 20 surjective pairing, 52, 76, 272 symmetry, 18 syntactic sugar, 57, 58, 65 syntactic theory, 176 System F, 611; See impredicative poly-

morphism.

tail-recursive function, 102 term, 3

algebra, 159

category, 462, 483 constant (in λ^{→}), 241 generated algebra, 195 model (for λ^{→}), 294, 550

Terms^{s}(Σ, Γ ), 150 terminal object, 264, 265, 456 terminals, 22 termination assertion, 389 termination property, 8, 205 theory, 176

of an algebra (Th(A)), 161, 163 determined by set of equations, 259 semantic, 161 syntactic, 163

total order, 18 total recursive function, 106 transitivity, 18 trivial algebra, 159 tuples, 16 Turing machine, 108 type, 9, 46, 145

abstraction, 609 application, 610 assignment, 240

as ordered sequence, 469, 618 checking, 255, 768 constant (in λ^{→}), 241 error, 288 expression λ^{→}, 237 λ\overrightarrow{t}, 769 λ^{×,→}, 237 λ^{→,Π} , 620, 627 λ^{→,∀}, 639 λ\overrightarrow{<:} , 706 λ_{<:}^{→,record} , 714 frame for λ^{→}, 282 inference, 765, 767, 769 of untyped term, 777 set relative to S, 661 soundness, 288 system, 9 theory, 262 universe, 9, 618

type-closed property of terms, 556 for λ^{×,→}, 560

for λ^{→,∀}, 661

type t = τ, 740

typed applicative structure, 280 function symbol (in algebra), 149 lambda term, 244 lambda theory, 259

typing axiom, 240 context (type assignment), 240, 618 as ordered sequence, 469

derivation, 244 judgement, 241

for untyped term, 783 type: type , 612, 625, 665

unambiguous grammar, 23

undefined, 19 unification, 772 union, 15 unit and ∗: unit , 122 universal algebra, 145 universe of types, 9, 618 untyped lambda calculus, 96, 131, 227, 236, 267, 295, 369, 657

model, 292 upper bound, 309

valid formula, 158, 421 value (in eager reduction), 92 value-result parameters, 444 Var(M ), 150 variable (in algebra), 149 variant types, 124

weak Church-Rosser, 559 weakest liberal precondition (wlp), 424 weakest precondition, 424 weakly initial, 652, 654 weak normalization, 268 well-founded relation, 38, 210 well-pointed category, 486 while programs, 387 with (record combination), 759

Yoneda embedding, 486, 503 Yoneda lemma, 504