Index

A

accessors (list) (list, revisited) (stream) accumulators (for binary trees) (the many uses of) addition (function, linear) (function, logarithmic) ALGOL 60 (programming language)

andmap (for binary trees) (for lists) (for strings) 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) 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

C

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) comparing ordered values compile time compiler (bootstrapping a) (compiling a) (interpreting a) (self-)

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

D

data 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 signatures dynamic programming

E

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) (of functions) (of programs) errors (syntax) (type, with a slash)

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

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) functions (graphs of) (mathematical) (partial) (that are applied to functions) (that return functions) (total) functors (that are applied to functors) (that return functors)

G

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) informatics inlining functions 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. (append) (cons) (hd) (length) (map) (sort) (tl) listlessness lists (association) (concatenating) (copying) (lazy, see lazy lists) (length of) (linked) (polymorphic) loop fusion

M

map (for binary trees) (for lists) (for streams) (for strings) 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) nil (the empty list) non-associativity (of integer division) (of integer subtraction)

None (option) numbers (factorial) (Fibonacci)

O

observational equivalence OCaml (Booleans) (assertions) (begin and end) (characters) (comments) (comments, exercise about writing) (conditional expressions) (control stack) (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) (impure expressions) (integers) (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) (pure expressions) (quote character) (references) (semicolon) (sequencing) (signature, declaring a) (strings) (tuples) (typing judgment) (variables) (while-loops) onions (grammar) (type)

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

P

paradox parafold-left (for natural numbers) parafold-right (for natural numbers) parameters (actual) (formal) parser parsing partial evaluation partial evaluator Peano numbers Peirce's arrow Platonism pleonasm (redundant) polymorphic (conditional expressions) (pairs) (tuples)

polymorphism (first encounter) power (function, see exponentiation) powerset (revisited) (tail-recursive) pred predicates primitive iteration primitive recursion Printf. (printf) (sprintf) programming (dynamic) (functional) (imperative) (logic) programming languages (statically typed) programs (equivalence of) (meaning of) projections (for pairs) (for quadruples) (for triples) propagation (backward)

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) 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 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 semiotics set comprehension sets as lists (re1visited, using an accumulator) (re2visited, using fold-right) (re3visited, using fold-left) shallots (grammar) (type) Sheffer stroke (the) short-circuit evaluation sieve (Eratosthenes's)

signatures (digital) Some (option) soundness (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) streams (comparing prefixes of) (concatenating) (filtering) (indexing) (mapping) (merging) (prefixing) (prepending) (reversing) (suffixing) String. (get) (get, syntactic sugar for) (init) (length) (make) (map) (mapi) succ syntactic sugar syntax (abstract) (concrete)

T

tail call tail recursion (see: reward) test coverage testing (complete) (incomplete) 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) (proof) type (checking) (inference) type constructor (data) type errors (circularity) (with a slash and a number) types (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)