Index

A

accessors (list) (list, revisited) (stream) accumulators (for binary trees) (for lists) (for non-negative integers) (the many uses of) addition (function, linear) (function, logarithmic) ALGOL 60 (programming language) algorithm

andmap (for binary trees) (for lists) association lists associativity (of addition, observable) (of boolean conjunction) (of boolean disjunction) (of integer addition) (of integer multiplication) (of list concatenation) (of sequencing) (of string concatenation) atoi

B

backward propagation base case (mathematical induction) (structural induction over lists) binary_tree_ (andmap) (fold) (map) (ormap) binding times bits

BNF body (of a for-loop) (of a lambda-abstraction) (of a let-expression) (of a letrec-expression) (of a while-loop) boolean (conjunction, calculating) (conjunction, in OCaml) (conjunction, testing) (disjunction, calculating) (disjunction, in OCaml) (disjunction, testing) (equivalence, calculating) (exclusive disjunction, calculating) (exclusive disjunction, testing) (implication, calculating) (negated conjunction, calculating) (negated conjunction, testing) (negated disjunction, calculating) (negated disjunction, testing) (negation, calculating) (negation, in OCaml) (negation, testing) bootstrapping (cognitive)

C

C (programming language) call by name call by need call by value (left to right) (right to left) Cartesian product (of 2 sets) (of 3 sets) (of a list of sets) Church encoding circular lists code coverage command (in OCaml) (syntactic unit) commutativity (of addition, observable) commuting diagram comparing ordered values compile time

compiler (bootstrapping a) (compiling a) (interpreting a) (self-) completeness (of a computation) (of a representation) computation (incremental, for Fibonacci numbers) computer science computing science cons (List.) (right-associativity of) context (delimited) (delimited, for call by need) continuations cooking recipe (the four causes of a) copy rule (the) Coq proof assistant (chicken or egg) coverage (branch) (code) (condition) curry (un)

D

data (processing) data science data type (abstract) (concrete) datalogy datatype (constructors) dead code

definiens (in a global let-expression) (in a local let-expression) delay (by name) (by need) (by value) diagram (I-) (T-) digital signature (composing a) dynamic programming

E

effect (computational) (side) emacs environment (type) (value) environments (as association lists in a module) (as association lists) (as functions in a module) (as functions) (in a module) equality (ground) (physical) (structural) equivalence (observational) (observational, first shot) (of functions) (of programs) errors (in OCaml) (message) (syntax) (type, in OCaml) (type, with a slash)

evaluation order evaluator exceptions (catching) (declaring new) (raising) exponentiation (function, linear) (function, logarithmic) expression (syntactic unit) expressions (regular) extension vs. intension

F

Factorial function (unit-test function) Factorial imperative program Factorial logic program Factorial numbers Factorial relation Factorial rewriting program fibfib (recursive definition of) (tail-recursive definition of) Fibonacci function (unit-test function) Fibonacci numbers fold (for binary trees) fold-left (for lists) (for natural numbers)

fold-right (for lists) (for natural numbers) Fortran (names of variables in) function (computable) (uncomputable) function abstraction function applications (left-associativity of) function type (right-associativity of the) functional abstraction functional instantiation functions (as parameterized expressions) (generic) (graphs of) (mathematical) (partial) (that are applied to functions) (that return functions) (total) functors (that are applied to functors) (that return functors)

G

Gauss (to the rescue) goal (sub-)

graph of a function

H

halting predicate (the) halting problem (the)

Haskell (programming language)

I

induction (mathematical) (nested) (structural, for lists) (structural, for natural numbers) induction hypothesis (mathematical induction) (structural induction over lists) induction step (mathematical induction) (structural induction over lists) inequality (ground) inferring (a monomorphic expression) (a polymorphic expression) informatics inlining functions intension vs. extension

interpreter (compiling an) (interpreting an) (self-) interpreters (tower of) invariant (loop) involution involutory iota isomorphism (type)

K

knapsack problem (the)

L

lambda-abstraction lambda-dropped definition lambda-lifted definition language (meta-) (source) (target) lazy lists left associativity list concatenation (right associativity of) list-fold-left, in essence

list-fold-right, in essence list-map, in essence list-mapi, in essence List. (append) (cons) (exists) (for_all) (hd) (init) (length) (map) (sort) (tl) list_ (andmap) (appendmap) (map) (ormap) (permutations) (powermap) listlessness lists (association) (concatenating) (copying) (imperative) (lazy, see lazy lists) (length of) (linked) (polymorphic) loop fusion

M

map (for binary trees) (for lists) (for streams) (for strings) (power) match-expressions (don'ts) (dos) memoization (built-in) microprocessor

modus ponens (computational content of the) multiplication (function, linear) (function, logarithmic) Murphy's law

N

naming convention (plural) nat-fold-left, in essence nat-fold-right, in essence nil (the empty list)

non-associativity (of integer division) (of integer subtraction) None (option) numbers (factorial) (Fibonacci)

O

observational equivalence OCaml (Booleans) (aliasing formal parameters) (applications) (assertions) (backslash character) (begin and end) (characters) (comments) (comments, exercise about writing) (conditional expressions) (control stack) (double quote character) (for-loops) (formal) (formals) (functions) (functors) (global let-expression declaring one variable) (global let-expression declaring several variables) (global letrec-expression declaring one variable) (global letrec-expression declaring several variables) (identifiers) (if-expressions) (integers) (libraries) (local let-expression declaring one variable) (local let-expression declaring several variables) (local letrec-expression declaring one variable) (local letrec-expression declaring several variables) (match-expressions) (modules) (modules, nested) (modules, signatures of) (names) (pairs) (quote character) (references) (semicolon) (sequencing) (signature, declaring a) (strings) (tuples) (typing judgment) (variables) (while-loops) OCaml expressions (impure) (pure) OCaml keywords (... ...) (... as ...) (assert ...) (fun ... -> ...) (if ... then ... else ...) (let ... = ... and ... and ... = ... in ...) (let ... = ... and ... and ... = ...) (let ... = ... in ...) (let ... = ...) (let rec ... = ... and ... and ... = ... in ...) (let rec ... = ... and ... and ... = ...) (let rec ... = ... in ...) (let rec ... = ...)

onions (grammar) (type) option type (polymorphic) ormap (for binary trees) (for lists) overflow (buffer) (control stack) (runtime stack)

P

paradox (computational content) parafold-left (for natural numbers) parafold-right (for natural numbers) parameters (actual) (formal) (formal, specifying their type) parser parsing partial evaluation partial evaluator Peano numbers Peirce's arrow Platonism pleonasm (redundant) polymorphic (conditional expressions) (pairs) (tuples) polymorphism (first encounter) polynomial function (degree 0) (degree 1) (degree 2) (degree 3) (degree 4) (in Horner form)

polynomials (decimal integers as) (in Horner form) power (function, see exponentiation) powerset (revisited) (tail-recursive) pred (ecessor) predicates primitive iteration primitive recursion Printf. (printf) (sprintf) program (processor) programming (dynamic) (functional) (imperative) (logic) programming languages (dynamically typed) (statically typed) programs (equivalence of) (meaning of) projections (for pairs) (for quadruples) (for triples) propagation (backward) Pythagorean triples

Q

queues (first in, first out in a module) (first in, first out) (in a module) (last in, first out in a module) (last in, first out)

R

recursion (mutual) (nested) (structural, for binary trees) (structural, for lists) (structural, for natural numbers) (tail) recursive data types (mutually) recursive functions regular expressions (abstract-syntax trees) (BNF of) (proof trees) (type for) relations (binary)

representation (completeness of a) (soundness of a) reward (see: tail recursion) rewriting right associativity run time

S

S-m-n (function) (theorem) S-m-n theorem (much) samefringe (the problem) Scheme (Chez) (programming language) scope (lexical) (shadowed bindings in lexical) self- (compiler) (interpreter) self-reference (in a circular list) (in a sentence) semantics semantics vs. syntax semiotics set comprehension sets as lists (re1visited, using an accumulator) (re2visited, using fold-right) (re3visited, using fold-left) shadowing shallots (grammar) (type) Sheffer stroke (the) short-circuit evaluation sieve (Eratosthenes's) Some (option)

soundness (of a computation) (of a representation) specializing a program specializing a specializer (with respect to a specializer) (with respect to an interpreter) specializing an interpreter stack (runtime) stacks (in a module) Standard ML (programming language) stream (of even natural numbers) (of natural numbers) (of odd natural numbers) (transducers) stream_ (append) (filter_in) (filter_out) (make) (map) (nth) (powermap) (prefix) (prepend) (reverse) streams (comparing prefixes of) (concatenating) (filtering) (indexing) (mapping) (merging) (prefixing) (prepending) (reversing) (suffixing) string-map, in essence string-mapi, in essence String. (get) (get, syntactic sugar for) (init) (length) (make) (map) (mapi) succ (essor) syntactic sugar syntax (abstract) (concrete) syntax vs. semantics

T

tail call tail recursion (see: reward) test coverage testing (complete) (complete, adage) (incomplete) (incomplete, adage) tests (regression) (unit) the proof is trivial (grammar) (type) thunks (by name) (by need) (by value) (memo)

tilde notation for negative numbers tree (abstract syntax) (binary, with payloads in the leaves and in the nodes) (binary, with payloads in the leaves) (binary, with payloads in the nodes) (proof) type (checking) (checking, a concrete example) (inference) (inference, a concrete example) type constructor (data) type errors (circularity) (in OCaml) (with a slash and a number) type variables (weak) types (in OCaml) (monomorphic) (polymorphic)

U

unfolding (a function call) (a let-expression) unit tests (functions implementing) (functors implementing) unparser

unparsing (Booleans) (characters) (integers) (polymorphic binary trees) (polymorphic lists) (polymorphic pairs) (polymorphic triples) (strings) (values) unused variables

V

value (denotable) (expressible) (storable) variables

virtual machine Von Neumann (architecture)

Y

YOYOYOLOOO

Z

zipping lists (un)