Wiki

2-SAT is Boolean satisfiability restricted to formulas in conjunctive normal form whose clauses have at most two literals. Unlike 3-SAT it is solvable in linear time: each clause (a or b) is a pair of implications, not a implies b and not b implies a, and the formula is unsatisfiable exactly when some variable and its negation lie in the same strongly connected component of the resulting implication graph. A satisfying assignment can be read off a topological order of the components. Random 2-SAT has a sharp satisfiability threshold at one clause per variable.

An algebraic data type is a type built from sums, where a value is one of several alternatives, and products, where a value has several components at once, possibly recursively. The name comes from counting: the number of values of a sum is the sum of the counts, and of a product their product, so types obey the laws of algebra. Values are taken apart by pattern matching, which the compiler checks for missing cases.

An anamorphism is the generalization of unfold: it builds a value of a recursive data type from a seed, using a function (a coalgebra) that produces one layer of the structure together with new seeds for its recursive positions. It is the categorical dual of the catamorphism, the unique homomorphism from any coalgebra into the final coalgebra of a functor. Anamorphisms can produce infinite structures such as streams, and they are the way to write corecursive programs that are guaranteed to be productive.

An applicative functor is a functor with pure : a -> f a and an operation that combines independent computations, <*> : f (a -> b) -> f a -> f b, or equivalently a product f a -> f b -> f (a * b), satisfying four laws. It sits between functors and monads: every monad is applicative, but because later steps cannot depend on earlier results, an applicative computation can collect all errors, run its parts in parallel, or be inspected before it runs.

Berlekamp's algorithm factors a square-free polynomial f over a finite field F_p by linear algebra. The polynomials v with v^p = v modulo f form a vector space whose dimension is exactly the number r of irreducible factors of f; it is the null space of Q - I, where Q is the matrix of the Frobenius map v -> v^p. Any nonconstant v in it splits f as the product of gcd(f, v - s) over s in F_p. For large p a random element of the space and one exponentiation split f with probability about one half.

β-reduction is the computation rule of the lambda calculus: an application of a function to an argument, (λx. e) a, is replaced by the body e with a substituted for x. Substitution must avoid capturing free variables of the argument. A term with no reducible subterm is in normal form; by the Church–Rosser theorem the normal form, if it exists, is unique, and normal-order reduction, which always contracts the leftmost outermost redex, finds it. Evaluation strategies of programming languages are restrictions of β-reduction.

Bit-blasting decides formulas over fixed-width bit-vectors, the machine integers of programs and hardware, by translating every variable into one Boolean variable per bit and every operation into a Boolean circuit, then handing the resulting clauses to a SAT solver. Addition becomes a ripple-carry adder and multiplication a shift-and-add array of adders, encoded with the Tseitin transformation. It is complete and simple, and it is how SMT solvers handle bit-vectors after word-level simplification; its weak point is multiplication, whose circuits are large and hard for SAT solvers.

A Bloom filter is a probabilistic data structure for set membership that uses a bit array of m bits and k hash functions. Adding an element sets the k bits its hashes select; a query answers “possibly present” if all k bits are set and “definitely absent” otherwise. It never gives a false negative, and its false-positive rate is about (1 − e^(−kn/m))^k after n insertions, which for the best k is about 0.6185^(m/n): around 10 bits per element give a 1% error, however large the elements are. Bloom filters are used to skip expensive lookups for keys that are not there, in databases, caches, networks and spell checkers.

Boxing is storing a value in a separately allocated heap block and handling it through a pointer to that block. Polymorphic languages box values so that every value fits in one machine word and generic code can copy and pass any value the same way; OCaml boxes floats, tuples and other structured values but keeps small integers and constant constructors unboxed as tagged words. The cost is an allocation and an indirection per value, which compilers avoid where they can by unboxing values whose type is known.

A Braun tree is a binary tree in which, at every node, the left subtree has either the same number of nodes as the right subtree or exactly one more. The shape is therefore determined by the size alone, and the height is ⌊log₂ n⌋ + 1. Used as a flexible array, element 0 is at the root and the bits of an index choose the path, so indexing, updating, and adding or removing an element at the front all take logarithmic time without any rebalancing.

The Brzozowski derivative of a regular expression r with respect to a character a is a regular expression for the strings w such that a w matches r. It is computed syntactically, by rules much like those of calculus, so a string can be matched by taking one derivative per character and checking whether the result matches the empty string. Up to simple algebraic identities a regular expression has finitely many derivatives, which are the states of a deterministic automaton, and the method extends directly to intersection and complement.

In computer algebra, a canonical form is a representation in which mathematically equal expressions are written identically, so that equality becomes a syntactic comparison and zero-testing a look at the representation. A normal form is the weaker requirement that expressions equal to zero are represented by 0. Expanded polynomials with sorted terms, reduced rational functions and remainders modulo a Gröbner basis are canonical; for expressions with exponentials, logarithms and absolute values, Richardson proved in 1968 that zero-equivalence is undecidable, so no canonical form can exist. Where no canonical form is practical, randomized evaluation, justified by the Schwartz–Zippel lemma, tests identities with high confidence.

The Cantor–Zassenhaus algorithm is a randomized method for factoring polynomials over a finite field. After the input is made square-free, distinct-degree factorization separates the irreducible factors by degree, using the fact that x^(p^d) − x is the product of all monic irreducibles whose degree divides d. Each group, a product of factors of the same degree d, is then split by taking the gcd with a^((p^d − 1)/2) − 1 for a random polynomial a: by the Chinese remainder theorem, this power is +1 or −1 independently in each factor's field, so the gcd separates the factors with probability about one half. It runs in expected polynomial time and is the standard method in computer algebra systems.

A catamorphism is the generalization of fold from lists to any recursive data type: it replaces each constructor of a value with a function and combines the results bottom up. Formally it is the unique homomorphism from the initial algebra of a functor to any other algebra of that functor. Writing a recursive data type as the fixed point of a base functor lets a single cata function fold every such type, with the recursion written once and each computation reduced to an algebra that handles one layer.

Conflict-driven clause learning (CDCL) is the algorithm of modern SAT solvers. It extends DPLL backtracking search with three ideas: when propagation falsifies a clause, conflict analysis derives a new clause that explains the conflict and adds it to the formula; the solver then backjumps non-chronologically to the decision level at which the new clause forces a literal; and branching follows the variables involved in recent conflicts. With watched literals, restarts and clause deletion, CDCL solvers decide industrial formulas with millions of variables, and with restarts they are as strong as general resolution, exponentially stronger than DPLL.

The Chase–Lev deque is the lock-free double-ended queue used by work-stealing schedulers. Its owner thread pushes and pops tasks at the bottom with plain reads and writes, and other threads steal from the top with a compare-and-swap; the two ends only contend when one element is left, which both sides resolve with the same compare-and-swap on the top index. The buffer is a circular array that grows when full. Correctness depends on a store-load ordering in pop that weak memory models require a fence to provide.

Cheney's algorithm is a copying garbage collector that moves every live object from one half of the heap, from-space, to the other, to-space, in breadth-first order, using the copied objects themselves as the queue: a scan pointer follows the free pointer through to-space, copying whatever the scanned objects point to. It needs no stack or extra memory, leaves a forwarding address in each moved object so shared and cyclic structures are copied once, compacts the live data, and costs time proportional to the live data, not the heap. It is the basis of the young-generation collectors of most language runtimes.

Church encoding represents data in the pure lambda calculus, which has only functions, by functions: a natural number n is the function that applies its argument n times, a boolean is a function choosing between two alternatives, and a pair is a function waiting for a selector. In general a value is represented by its own fold. Arithmetic, logic and data structures all become lambda terms, which is how the lambda calculus was shown to express every computable function; in typed form the encoding needs polymorphism, as in System F.

The Church–Rosser theorem states that β-reduction in the λ-calculus is confluent: if a term reduces to two different terms, both can be reduced further to a common term. It follows that a term has at most one normal form, so the order in which redexes are reduced cannot change the result of a terminating computation, and that the λ-calculus is consistent, since two different normal forms are never equal. Church and Rosser proved it in 1936. The standard modern proof, due to Tait and Martin-Löf, uses parallel reduction, which has the diamond property that single-step reduction lacks. Confluence is the central property of rewriting systems in general.

A closure is a function value together with the environment in which it was created: the bindings of the free variables its body refers to. Closures are what make functions first-class values in a lexically scoped language. Compilers implement them by closure conversion, which turns each function into a code pointer paired with a record of captured values.

A propositional formula is in conjunctive normal form (CNF) when it is a conjunction of clauses, each clause a disjunction of literals, and each literal a variable or its negation. Every formula is equivalent to one in CNF, but the equivalent CNF can be exponentially larger; the Tseitin transformation instead produces an equisatisfiable CNF of linear size by adding variables. CNF is the input format of SAT solvers and resolution provers, and restricted forms such as Horn clauses and 2-CNF can be solved in linear time.

A comonad is the categorical dual of a monad: a functor w with extract : w a → a, which reads the value in focus, and extend : (w a → b) → w a → w b, which applies a function that looks at a whole context to every position of that context. Where a monad describes producing a value with an effect, a comonad describes computing a value from a context, such as a cell from its neighbourhood, a value from its history, or a field from a whole structure.

Congruence closure is the algorithm that decides whether an equation between terms follows from a set of ground equations, using only the laws of equality and the congruence rule that equal arguments give equal function applications. It maintains equivalence classes of subterms in a union–find structure and, whenever two classes merge, merges any applications of the same function whose arguments have become equal. It runs in O(n log n) time and decides the quantifier-free theory of equality with uninterpreted functions (EUF), which makes it a core theory solver in SMT; the same data structure, the e-graph, underlies equality saturation in compilers.

ConstraintKinds is the GHC extension that gives constraints their own kind, Constraint, so that the thing to the left of => becomes a first-class type-level entity that can be named with a synonym, passed as a parameter, returned by a type family, and stored in a data type. It lets a class leave to each instance what that instance needs of its element types, as when a container class requires Ord for sets and nothing for lists, and it lets dictionaries be packaged as ordinary values with Dict.

Continuation-passing style (CPS) is a way of writing programs in which no function returns: each takes an extra argument, its continuation, a function that represents the rest of the computation, and calls it with the result. Every call becomes a tail call, evaluation order is made explicit, and control operators such as exceptions, backtracking and call/cc become ordinary functions. Compilers for functional languages use CPS, or the closely related A-normal form, as an intermediate language.

Craig's interpolation theorem states that if a formula A implies a formula B, there is a formula I, the interpolant, built only from the symbols A and B have in common, such that A implies I and I implies B. In verification it is used in the equivalent refutation form: when A ∧ B is unsatisfiable, an interpolant is implied by A, inconsistent with B, and mentions only shared variables. For propositional logic, an interpolant can be computed from a resolution refutation of A ∧ B in linear time, which McMillan used in 2003 to build an unbounded model checker from a SAT solver.

Currying turns a function of several arguments into a chain of functions of one argument each: f : A * B -> C becomes curry f : A -> (B -> C). The two forms are in one-to-one correspondence, which in mathematics is the exponential law C^(A*B) = (C^B)^A. In OCaml and Haskell every function is curried, so partial application, supplying only some of the arguments, is ordinary.

A representation of lambda terms without variable names: each variable is the number of binders between it and the lambda that binds it. Alpha-equivalent terms become identical and substitution cannot capture a variable, at the price of shifting indices when a term moves under a binder.

Defunctionalization is a whole-program transformation that removes higher-order functions. Each lambda expression in the program is replaced by a constructor of a data type, carrying the lambda's free variables, and each call of an unknown function is replaced by a call to a single first-order apply function that matches on the constructor and runs the corresponding body. Applied to the continuations of a program in continuation-passing style, it turns a recursive evaluator into an abstract machine whose stack is an explicit data structure.

A dependent type is a type that may mention values, so that a vector's length can appear in its type and a function's result type can be computed from its arguments. Function types generalize to dependent products Π(x : A). B(x), and pairs to dependent sums Σ(x : A). B(x). Because types can express propositions and programs can be proofs, languages with dependent types, such as Agda, Coq (Rocq), Lean and Idris, double as proof assistants. The price is that type checking involves evaluating programs, so these languages require functions to terminate, and type equality is decided up to computation.

A deriving strategy is an explicit choice of how GHC produces a derived type class instance: stock, generated by the compiler from the constructors; newtype, reusing the wrapped type's instance by coercion; anyclass, an empty instance that takes the class's default methods; or via, reusing the instance of another type with the same representation. Several strategies can apply to the same declaration, with different results, so naming the strategy removes the ambiguity. The two coercing strategies are sound only when the class's methods can be coerced, which GHC checks with type roles.

Dictionary passing is the standard way to implement type classes. Each class becomes a record type whose fields are its methods, each instance becomes a value of that record type, and each function with a class constraint receives the record, the dictionary, as an extra argument, which the compiler supplies at every call site after resolving which instance applies. An instance that itself has a context, such as equality on lists given equality on elements, becomes a function from dictionaries to a dictionary, and a superclass becomes a field. The same technique written by hand is the usual way to get type-class-like overloading in OCaml, with records, first-class modules or functors.

Difference logic is the fragment of linear arithmetic whose atoms bound the difference of two variables by a constant, x − y ≤ c, over the integers or the reals. A conjunction of such constraints is satisfiable exactly when the graph with an edge from y to x of weight c for each constraint has no negative cycle, so it can be decided by shortest-path algorithms such as Bellman–Ford, and a negative cycle is a short explanation of unsatisfiability. Boolean combinations of difference constraints are handled by SMT solvers through DPLL(T); they express scheduling problems and the timing constraints of timed automata.

DIMACS CNF is the standard plain-text format for Boolean formulas in conjunctive normal form, read by essentially every SAT solver. After optional comment lines beginning with c, a header p cnf V C gives the number of variables and clauses; each clause is then a list of non-zero integers, v for a variable and −v for its negation, terminated by 0. It was defined for the Second DIMACS Implementation Challenge in 1993 and has variants for quantified formulas (QDIMACS), weighted MaxSAT (WCNF) and unsatisfiability proofs (DRAT).

DPLL, the Davis–Putnam–Logemann–Loveland procedure, is the backtracking search algorithm for Boolean satisfiability on which all complete SAT solvers are built. It repeatedly simplifies a CNF formula by unit propagation and pure literal elimination, then chooses an unassigned variable and tries both of its values in turn, backtracking to the most recent choice when a clause becomes false. It is sound and complete, uses memory linear in the formula, and its runs on unsatisfiable formulas correspond to tree-like resolution proofs, which gives exponential lower bounds such as the n! − 1 decisions it needs for the pigeonhole formulas. Clause learning turned it into CDCL.

DPLL(T) is the architecture of lazy SMT solvers: a CDCL SAT solver searches over the Boolean structure of a formula, treating each theory atom as a propositional variable, and a theory solver for T checks the consistency of the atoms it assigns. When the theory solver finds the assigned literals inconsistent, it returns an explanation, whose negation the SAT solver learns as a clause before backjumping; it may also propagate literals the assignment implies. The approach separates a generic engine from pluggable theory solvers and is used by nearly all SMT solvers, including Z3, cvc5 and Yices.

Earley parsing is an algorithm that parses any context-free grammar, including ambiguous and left-recursive ones. For each position in the input it builds a set of items, grammar rules with a dot marking how much of the right-hand side has been recognized and the position where recognition began, using three operations: prediction adds the rules for a nonterminal the parser expects, scanning moves past a matching token, and completion advances the rules that were waiting for a nonterminal that has just been recognized. It runs in O(n³) time in general, O(n²) on unambiguous grammars and linear time on most grammars used in practice. Jay Earley published it in 1970.

An effect handler runs code that may perform effects, and handles each effect by receiving it together with the continuation from the point where it was performed, which it can resume, discard or store. Handlers generalize exception handlers, and let generators, async I/O, schedulers, state and nondeterminism be written as libraries while the code that uses them stays in direct style. They come from the theory of algebraic effects of Plotkin, Power and Pretnar. OCaml 5 implements them with one-shot continuations: each can be resumed at most once, which keeps them cheap, since a continuation is the suspended stack itself.

The fast Fourier transform (FFT) computes the discrete Fourier transform of n values, the evaluation of a polynomial at the n complex n-th roots of unity, in O(n log n) operations instead of O(n^2). The Cooley-Tukey algorithm splits the input into even and odd positions, transforms each half recursively, and combines them with n/2 butterflies. Because the transform turns convolution into pointwise multiplication, the FFT multiplies polynomials and large integers in near-linear time; over a finite field with suitable roots of unity the same algorithm is exact.

A persistent sequence with amortized constant-time access at both ends, and concatenation and splitting in logarithmic time. The ends are kept in buffers of one to four elements, and the middle is a finger tree of 2-3 nodes, one level deeper at each step down the spine.

Conflict analysis is the step of a CDCL SAT solver that explains a conflict by a new clause. Starting from the clause that became false, the solver repeatedly resolves it with the reason clauses of literals assigned at the current decision level, in reverse order of assignment, until only one literal of that level remains. That literal is the first unique implication point (UIP), a node through which every path from the decision to the conflict passes in the implication graph. The resulting clause is learned; it is implied by the formula, it forbids the combination of assignments that caused the conflict, and after backjumping to the second-highest level in it, it immediately propagates the negation of the UIP.

Foldable is the abstraction of a container whose elements can be combined in order: a list, a tree, an option. A fold replaces the constructors of the structure with a function and a starting value, and every summary of the elements, their sum, length, maximum, list of elements or whether any satisfies a predicate, is derived from it. Equivalently, a foldable container maps each element into a monoid and combines the results (foldMap). The universal property of fold characterizes exactly which functions are folds.

Fourier–Motzkin elimination removes a variable from a system of linear inequalities by combining every inequality that bounds the variable from below with every inequality that bounds it from above. The result has a solution exactly when the original system does, over the real or rational numbers, and describes the projection of the solution set. Eliminating all variables decides satisfiability, and back-substitution recovers a solution, but the number of inequalities can grow doubly exponentially.

The free monad on a functor F is the monad whose values are trees of F-shaped instructions with results at the leaves: Pure a | Free (F (Free F a)). It adds exactly the monad structure and nothing else, so a program written in it is a description of a sequence of instructions that different interpreters can run, inspect or transform. Any mapping from F into a monad M extends uniquely to an interpreter from the free monad into M. Left-nested binds take quadratic time, which the Church-encoded form avoids.

A functional queue is a first-in first-out queue built from immutable lists. The standard design keeps a front list to take elements from and a reversed rear list to add them to, and reverses the rear into the front when the front runs out; each operation then takes amortized constant time. When old versions of the queue are reused, the amortized bound fails, and Okasaki's banker's queue restores it by making the reversal lazy and memoized.

In functional programming, a functor is a type constructor f with an operation fmap : (a -> b) -> f a -> f b that applies a function inside the structure without changing its shape, preserving identity and composition. Lists, options, trees and functions out of a fixed type are functors. The notion comes from category theory. In OCaml the word also names parametrised modules such as Map.Make.

A generalized algebraic data type (GADT) is an algebraic data type whose constructors may each give a more specific result type than the declared one, instead of all sharing one polymorphic return type. Matching on a constructor then tells the type checker what the type parameter was, so a single well-typed eval can return an int for an Add node and a bool for an Eq node, checked at compile time rather than by a run-time tag test. GADTs express typed syntax trees, type representations and equality proofs, typed format strings and length-indexed data. The price is that type inference needs annotations.

A garbage collector that splits the heap by age, because most objects die young: new objects go to a small nursery collected often by copying, and survivors are promoted to a larger heap collected rarely. A write barrier records old-to-young pointers so that a minor collection need not scan the old heap.

Green threads are threads scheduled by a language runtime or library instead of the operating system kernel. A suspended green thread is just a saved continuation or a small stack on the heap, so creating and switching between them costs little and a program can run hundreds of thousands at once. They are cooperative or preempted by the runtime at safe points, and they are multiplexed onto a smaller number of kernel threads (M:N scheduling), which requires blocking system calls to be turned into non-blocking ones. Erlang processes, Haskell threads, goroutines and Java virtual threads are examples.

A Gröbner basis of an ideal of multivariate polynomials is a generating set with respect to which multivariate division behaves as in one variable: the remainder of any polynomial is unique, and it is zero exactly when the polynomial lies in the ideal. Formally, the leading terms of the basis, for a fixed monomial order, generate the ideal of all leading terms. Buchberger's algorithm computes one from any generating set by adding the remainders of S-polynomials until they all reduce to zero. Gröbner bases decide ideal membership, solve systems of polynomial equations, count their solutions and eliminate variables; Bruno Buchberger introduced them in 1965.

The Gruntz algorithm computes limits of exp-log functions, those built from x and constants by arithmetic, exp and log, as x tends to infinity. It finds the set of most rapidly varying subexpressions, rewrites the function as a power series in one of them, and reads the limit off the leading term, recursing when the leading coefficient is itself a function of x. It succeeds where expansions in powers of 1/x fail, because exponentially small terms are invisible to them, and it is the limit algorithm of SymPy and Maple. Like the Risch algorithm, it is complete relative to an oracle that decides whether an expression is identically zero.

A hash array mapped trie (HAMT) is a trie over the bits of the keys' hash values: each level consumes a few bits, usually five, to choose one of 32 children, and each node stores only its occupied children in a compact array, located by counting bits in a 32-bit bitmap. Lookups follow about log32 n levels. Updated by copying the path to the changed leaf, a HAMT is a persistent hash map with small, cache-friendly nodes, and it is the standard implementation of immutable maps and sets in Clojure, Scala and Haskell's unordered-containers.

Hensel lifting turns a factorization of a polynomial modulo a prime p into a factorization modulo p², p⁴ and so on, as long as the factors modulo p are coprime. Each step solves a linear equation using the Bézout relation between the factors, and in quadratic form it doubles the precision, the p-adic analogue of Newton's method. It is the core of Zassenhaus's algorithm for factoring integer polynomials: factor modulo a small prime, lift until the modulus exceeds twice the Landau–Mignotte bound, and recombine the lifted factors into true factors over the integers.

Hermite reduction is the step of symbolic integration that splits the integral of a rational function A/D into a rational function and an integral whose denominator is square-free, using only gcds and the extended Euclidean algorithm, with no factorization of D. The rational part of the antiderivative comes entirely from the repeated factors of D, and each reduction step lowers their multiplicity by one. What remains integrates to a sum of logarithms, whose coefficients are the roots of the Rothstein–Trager resultant. Together the two steps integrate any rational function over a field of characteristic zero exactly, introducing algebraic numbers only where the answer needs them.

A higher-kinded type is a type constructor, such as Maybe or List, that takes types as arguments, and higher-kinded polymorphism is the ability to abstract over such constructors with type variables, so that Functor f can be instantiated at Maybe or at lists without naming their element types. Kinds classify types the way types classify values: Int has kind Type, Maybe has kind Type → Type. Higher-kinded variables are what make a single Functor or Monad class usable across every container. Haskell and Scala support them directly; OCaml expresses the same abstraction with module functors or an encoding, and Java and Go cannot express it.

Horner's method evaluates a polynomial a_n x^n + ... + a_0 by nesting the multiplications, (...(a_n x + a_(n-1)) x + ...) x + a_0, which takes n multiplications and n additions, the fewest possible for a general polynomial. The intermediate values are the coefficients of the quotient on division by x - c, so the same loop performs synthetic division, and repeated divisions give the derivatives and the shifted polynomial p(x + c). It is backward stable, but near a multiple root the result can be dominated by rounding errors.

A function that unfolds a seed into a recursive structure and folds that structure into a result, written so the structure is never built: hylo f g = f . fmap (hylo f g) . g. The call tree of the recursion is the intermediate structure.

Karatsuba multiplication is a divide-and-conquer algorithm for multiplying large integers or polynomials. Splitting each factor into a high and a low half, it computes the product from three half-size products, a₁b₁, a₀b₀ and (a₀ + a₁)(b₀ + b₁), instead of the four the schoolbook method needs, and recurses. Its cost is O(n^log₂3) ≈ O(n^1.585) digit operations instead of O(n²). Anatoly Karatsuba found it in 1960, disproving Kolmogorov's conjecture that n² was optimal. Because of its extra additions it is used above a size threshold, and it is the first of a family that leads through Toom–Cook to FFT-based multiplication.

In computer algebra, a kernel is a maximal subexpression that is not built from sums, products and integer powers, such as sin(x), exp(x + 1) or √x, which the system treats as an opaque variable so that polynomial and rational-function algorithms can operate on the expression around it. Expanding (sin x + 1)² treats sin x as a variable k and returns k² + 2k + 1 with k replaced by sin x. Equal kernels must be recognized as the same variable, which requires their arguments to be in canonical form. Kernels are not algebraically independent in general, as exp(2x) = exp(x)², and full simplification requires rewriting them into an independent set, which the structure theorems of Risch and Rosenlicht describe for elementary functions.

Kleisli composition composes two functions that return monadic results, f : a → m b and g : b → m c, into a function a → m c, by applying f and binding its result to g. It is written >=> in Haskell. Functions of this shape are the arrows of the Kleisli category of the monad, with return as the identity, and the monad laws are exactly the statement that this composition is associative and has return as a unit on both sides.

Knuth's Algorithm D divides one multiple-precision integer by another: schoolbook long division in base 2^k, where each quotient digit is guessed from the leading limbs of the remainder and divisor. After normalizing the divisor so its top limb is at least half the base, the guess is never too small and at most two too large, a cheap test with one more limb removes almost all errors, and a rare add-back step fixes the rest. It takes O(mn) operations for an (m+n)-limb dividend and an n-limb divisor.

The Landau–Mignotte bound limits the coefficients of any factor of an integer polynomial in terms of the polynomial itself: if g of degree k divides f, then each coefficient of g is at most binom(k, j) times the Euclidean norm of f, up to the ratio of leading coefficients, so all are below 2^k ‖f‖₂. It follows from Landau's inequality for the Mahler measure. Computer algebra algorithms use it to decide how large a modulus is needed to recover a factor or a gcd from its image modulo a prime power or a product of primes, as in Hensel lifting and the modular gcd. Factors can have larger coefficients than the polynomial they divide, so some such bound is necessary.

Lazy evaluation, or call-by-need, delays computing an expression until its value is needed and then remembers the value, so it is computed at most once. It lets programs define infinite structures and consume only part of them, separates generating candidate values from choosing among them, and avoids work whose result is never used. Its costs are the memory held by unevaluated suspensions, which can cause space leaks, and harder reasoning about when work happens. Haskell is lazy by default; OCaml provides it explicitly through Lazy.t and Seq.

A leftist heap is a priority queue represented as a heap-ordered binary tree in which, at every node, the right spine of the left child is at least as long as the right spine of the right child. The right spine of the whole tree then has at most log₂(n + 1) nodes, and two heaps can be merged in O(log n) time by merging their right spines like sorted lists. Insertion and deletion of the minimum are special cases of merging. Because merging copies only the right spines, leftist heaps are a standard persistent priority queue in functional languages.

A lens is a first-class pair of a getter and a setter for one part of a structure, with laws that make them agree: you get back what you set, setting what you got changes nothing, and a second set overwrites the first. Lenses compose, so a path through nested immutable records is one value that can read or update the part at its end. They originated in work on the view-update problem, and in Haskell are usually encoded as functions polymorphic in a functor, which makes composition ordinary function composition.

LL(1) parsing is top-down parsing that decides which grammar rule to apply by looking at a single token of input. It reads the input Left to right and builds a Leftmost derivation, choosing each rule from a table indexed by the nonterminal being expanded and the next token\; the table is computed from the FIRST and FOLLOW sets of the grammar, and a grammar is LL(1) when no entry holds two rules. LL(1) parsers run in linear time with no backtracking, and they correspond directly to recursive-descent parsers, one function per nonterminal. Left-recursive and ambiguous grammars are not LL(1) and must be rewritten.

Bottom-up parsing driven by a table of states: the parser shifts tokens onto a stack, and reduces the top of the stack by a grammar rule when the next token says to. A grammar for which the table cannot be built without a choice has conflicts, reported as shift/reduce or reduce/reduce.

A Merkle tree, or hash tree, is a binary tree in which every leaf holds the cryptographic hash of a data block and every interior node holds the hash of its two children, so that the root hash commits to the whole sequence. Any block can be shown to belong to the sequence with the logarithmically many sibling hashes on its path to the root, and two copies can be compared by descending only into subtrees whose hashes differ. Merkle trees underlie Git, Bitcoin, Certificate Transparency, replicated databases and hash-based signatures.

The modular GCD algorithm computes the greatest common divisor of two polynomials with integer coefficients by computing it modulo many machine-word primes, where coefficients never grow, and reconstructing the integer coefficients with the Chinese remainder theorem once the product of the primes exceeds twice a bound on them. Primes that divide the leading coefficients are skipped, unlucky primes that give an image of too high a degree are detected and discarded, and a final trial division certifies the result. The intermediate numbers are no larger than the answer, which makes it far faster than remainder-sequence methods; it was introduced by Brown in 1971.

In functional programming, a monad is a type constructor m with two operations, return : a -> m a and bind : m a -> (a -> m b) -> m b, satisfying three laws. It lets code with some extra behaviour, such as failure, several results, configuration, state or I/O, be written as a sequence of ordinary steps, with the behaviour defined once in bind. The notion comes from category theory.

A monoid is a set with an associative binary operation and an identity element for it: integers under addition with 0, strings under concatenation with the empty string, functions under composition with the identity. Associativity means a sequence can be combined with any bracketing, so a fold over a monoid can be split into parts and computed in parallel or incrementally. Lists are the free monoid, and every monoid-valued function on elements extends uniquely to lists.

A monomial order is a total order on the monomials of a polynomial ring that is compatible with multiplication and has 1 as its smallest element. It determines the leading term of every polynomial, and with it the result of multivariate division and the shape of Gröbner bases. The standard choices are lexicographic order, which compares exponents variable by variable and is used for eliminating variables; graded lexicographic order; and graded reverse lexicographic order, which usually gives the smallest Gröbner bases and the fastest computations. Dickson's lemma guarantees that every monomial order is a well-order, so that division and Buchberger's algorithm terminate.

The Nelson–Oppen method decides satisfiability of quantifier-free formulas that mix several theories with disjoint signatures, such as linear arithmetic and uninterpreted functions, using only a decision procedure for each theory. The formula is first purified, by naming mixed subterms with fresh variables, so that every literal belongs to one theory; the theory solvers then agree on which of their shared variables are equal, either by propagating the equalities each entails (enough for convex theories) or by searching over all arrangements of the shared variables. It is complete for theories that are stably infinite, and it is how SMT solvers combine their theory solvers.

An orphan instance is a type class instance declared in a module that defines neither the class nor the type. Because instance resolution is global but imports are not, two orphans for the same class and type can coexist in one program, and code compiled against different ones can disagree: a Set built under one ordering and searched under another silently loses elements. GHC warns about orphans, and Rust forbids them outright with its orphan rule. The usual fix is a newtype, which gives the instance a type of its own.

Two type class instances overlap when some type matches both of their heads, as Pretty [a] and Pretty String do at [Char]. Instance resolution in Haskell does not backtrack, so by default GHC reports an error rather than choose. The OVERLAPPING and OVERLAPPABLE pragmas let the most specific matching instance win, which is predictable when the choice is made at a known type and all the instances are in scope, but can make the same expression behave differently in different modules. INCOHERENT lets GHC choose even when the choice depends on a type it does not yet know. Closed type families and newtypes are the usual alternatives.

A pairing heap is a priority queue represented as a heap-ordered tree in which a node can have any number of children. Insertion and merging link two roots in constant time; deleting the minimum removes the root and combines its children in two passes, first merging them in pairs from left to right and then merging the results from right to left. Deletion takes logarithmic amortized time. Pairing heaps are short to write and fast in practice.

A paramorphism is a recursion scheme that generalizes a fold: at each step it receives not only the result of the recursive calls on the substructures but also the substructures themselves. On natural numbers it is primitive recursion. Functions such as factorial, the list of suffixes, or insertion into a sorted list, which need the original tail as well as a result computed from it, are paramorphisms.

A parser combinator is a higher-order function that builds a parser from smaller parsers: a sequence of two parsers, a choice between them, a repetition of one. Parsers are ordinary values in the host language, so a grammar is written as a program that is itself the parser, with no separate generator. Parser combinators produce recursive descent parsers; they cannot use left-recursive rules directly, and with unlimited backtracking can take exponential time, which memoization (packrat parsing) reduces to linear.

A partial fraction decomposition rewrites a rational function n/d as a polynomial plus a sum of simpler fractions, one family for each power of an irreducible factor of the denominator: n/d = q + Σ c_ij / f_i^j with deg c_ij < deg f_i. It exists and is unique once the factorization of d is fixed. Splitting across coprime factors needs only the extended Euclidean algorithm, and the terms for a power f^e are the digits of an f-adic expansion, so computing it costs no more than the factorization of the denominator; with a square-free factorization, no factoring is needed at all. It is the basis of the integration of rational functions and of closed forms for rational generating functions.

A phantom type is a type parameter that appears in a type's declaration but in none of its fields, used to keep otherwise identical representations apart: lengths in metres and in feet, validated and unvalidated strings, read-only and writable handles, SQL expressions of different result types. It carries no data and costs nothing at run time. Combined with an abstract type whose constructors are hidden, it lets a library enforce invariants through the type checker. Unlike a GADT index it tells a pattern match nothing; it constrains what callers may do, not what the compiler can learn.

The pigeonhole formulas PHPⁿ⁺¹ₙ are CNF formulas stating that n + 1 pigeons can be placed in n holes with no two in the same hole. They are unsatisfiable, as the pigeonhole principle says, but Haken proved in 1985 that every resolution refutation of them has exponential size. Since SAT solvers based on DPLL and CDCL produce resolution proofs, they need exponential time on these small formulas, which makes the family the standard example of what resolution cannot do. Proof systems that can count, such as cutting planes and extended resolution, refute them in polynomial size.

A polymorphic variant is a variant whose constructors, called tags and written with a backquote in OCaml, exist independently of any type declaration. Their types are sets of tags with bounds: [> `A] means at least `A, [< `A | `B] means at most those two, and unification works out unions and intersections of those sets using row variables. They let functions share constructors across types, be extended with new cases without editing old code, and encode subtyping, at the cost of longer types and error messages and of typos in open types going unnoticed.

A preprocessor that rewrites the OCaml syntax tree between parsing and type checking. Derivers generate code from type declarations tagged [@@deriving name]; extension points expand nodes written [%name payload]. Neither sees any types.

Pratt parsing, or top-down operator precedence parsing, is a technique for parsing expressions in which every operator has a numeric binding power on each side, and a single recursive function parses an expression by consuming operators for as long as they bind more tightly than a given minimum. Prefix, infix, postfix, mixfix and bracketing operators are handled by attaching to each token a null denotation, its meaning at the start of an expression, and a left denotation, its meaning after one. The method handles any number of precedence levels and both associativities in linear time with one function instead of one grammar rule per level, and new operators can be added by extending a table. Vaughan Pratt introduced it in 1973.

A prism is the counterpart of a lens for sum types: a partial getter, preview, that succeeds only on one case, and a builder, review, that makes a whole value from that case's contents. Two laws make them agree. Prisms compose with each other, and a lens composed with a prism gives an affine traversal, which has at most one focus and no builder. They make deep edits into data like JSON or syntax trees safe when the path does not exist, and they are one of the standard optics, alongside lenses, isos and traversals.

Pseudo-division is division of polynomials over an integral domain that is not a field, such as the integers or a ring of polynomials in other variables. To avoid fractions, the dividend a is first multiplied by lc(b)^(deg a − deg b + 1), the leading coefficient of the divisor raised to one more than the degree difference; then ordinary long division succeeds and yields a pseudo-quotient q and pseudo-remainder r with lc(b)^e a = q b + r and deg r < deg b. It is the basic step of polynomial remainder sequences over the integers, of resultant and gcd computation, and of Wu's method in geometry theorem proving. Iterated naively, it makes coefficients grow exponentially.

Pure literal elimination is a simplification rule for formulas in conjunctive normal form: if a variable occurs in the formula only positively, or only negatively, it can be set so that all its occurrences are true, and every clause containing it can be deleted, without changing whether the formula is satisfiable. It is one of the rules of the DPLL procedure. Modern CDCL solvers do not apply it during search, because detecting pure literals is expensive, but it survives in preprocessing, generalized by autarkies and blocked clause elimination.

A red-black tree is a binary search tree whose nodes are coloured red or black so that no red node has a red child and every path from the root to a leaf passes through the same number of black nodes. The two rules keep the height at most 2 log2(n + 1), so search, insertion and deletion take O(log n) time. Red-black trees are an encoding of 2-3-4 trees as binary trees, and Okasaki's functional version reduces insertion to one rebalancing rule with four cases.

A refinement type is a base type paired with a logical predicate that its values must satisfy, such as {v : Int | v > 0}, the positive integers. Type checking generates verification conditions, implications between predicates, and discharges them with an SMT solver, so a program can be checked against preconditions, postconditions and invariants without the programmer writing proof terms. The predicates are restricted to a decidable logic, typically linear arithmetic with uninterpreted functions, which is what keeps checking automatic. LiquidHaskell, F* and Liquid Types are the best-known systems.

Replace every leaf of a tree by the tree's minimum, in one traversal. The traversal returns the minimum and the rebuilt tree together, and the rebuilt tree's leaves refer to the minimum the same traversal is still computing. It works because the reference is lazy.

Resolution is the inference rule that derives, from two clauses containing a variable with opposite signs, the clause of all their other literals: from C ∨ x and D ∨ ¬x, infer C ∨ D. It is sound and refutation complete for propositional logic, so a set of clauses is unsatisfiable exactly when the empty clause can be derived. Resolution is the proof system behind SAT solvers, whose runs on unsatisfiable formulas are resolution refutations, and behind first-order theorem provers and logic programming. Some formulas, such as the pigeonhole formulas, have only exponentially long resolution refutations.

The Risch algorithm is a decision procedure for integration in finite terms: given an elementary function, it either finds an elementary antiderivative or proves that none exists. It rests on Liouville's theorem, which says that an elementary antiderivative, if one exists, is a function of the same field plus constant multiples of logarithms. The algorithm writes the integrand in a tower of logarithmic, exponential and algebraic extensions of the rational functions and works down it, using Hermite reduction, the Rothstein–Trager resultant and the Risch differential equation y′ + fy = g. Its transcendental case is completely algorithmic; its algebraic case is much harder; and both are decision procedures only relative to deciding whether a constant is zero.

A rope is a binary tree whose leaves are strings and whose internal nodes represent the concatenation of their children, with each node caching the length of its left subtree. Concatenation creates one node instead of copying, and indexing, splitting, insertion and deletion in the middle take time logarithmic in the length for a balanced rope. Ropes are immutable and share structure between versions, which makes them suited to text editors with undo and to programs that build long strings piece by piece.

The Boolean satisfiability problem, SAT, asks whether some assignment of true and false to the variables of a propositional formula makes the formula true. It was the first problem shown to be NP-complete, so every problem in NP reduces to it, and no polynomial-time algorithm is known. In practice SAT solvers based on conflict-driven clause learning decide industrial instances with millions of variables, which has made SAT a general-purpose engine for hardware and software verification, planning, scheduling and combinatorics.

Representing data by its case analysis rather than its fold: a Scott numeral takes what to do for zero and what to do with the predecessor. Pattern matching and the predecessor take one step; iteration needs recursion from outside, such as a fixed-point combinator.

A semigroup is a set with an associative binary operation, with no requirement of an identity element. Maximum and minimum, union of bounding boxes, concatenation of non-empty lists and "keep the first" are semigroups that are not monoids. Associativity alone allows a non-empty sequence to be combined in any bracketing, and n copies of an element to be combined in O(log n) operations by repeated squaring. Adjoining an identity turns any semigroup into a monoid.

The simplex method solves linear programs, maximizing a linear function subject to linear inequalities, by walking along the edges of the feasible polyhedron from vertex to vertex, each step improving the objective, until no neighbouring vertex is better. Each step is a pivot on a tableau. It is fast in practice and in smoothed analysis, but takes exponential time on the Klee-Minty cubes with Dantzig's pivoting rule, and needs a rule such as Bland's to avoid cycling on degenerate problems. Its final tableau also gives a solution of the dual program, certifying optimality.

A skew binomial heap is a priority queue made of a list of heap-ordered trees whose sizes follow the skew binary number system, in which adding one never carries more than one digit. Insertion therefore takes constant time in the worst case, instead of the logarithmic worst case of an ordinary binomial heap, while merging, finding the minimum and deleting it take logarithmic time. Brodal and Okasaki used it as the base of a purely functional priority queue with optimal bounds.

Three combinators, S x y z = x z (y z), K x y = x and I x = x, from which every closed lambda term can be built by application alone, with no variables. I is redundant, since S K K x = x. The translation from lambda terms is called bracket abstraction.

Satisfiability modulo theories (SMT) is the problem of deciding whether a first-order formula is satisfiable when some of its symbols are interpreted by background theories, such as integer or real arithmetic, bit-vectors, arrays and uninterpreted functions. SMT solvers such as Z3 and cvc5 combine a SAT solver, which handles the Boolean structure, with specialized decision procedures for the theories, usually in the DPLL(T) architecture. They read the standard SMT-LIB language and are the reasoning engines of program verifiers, symbolic execution tools, test generators and many other analysis tools.

Memory a program holds longer than it needs to. In a lazy language the usual cause is a chain of unevaluated thunks: a lazy left fold over a list builds one suspended addition per element and only performs them at the end. A heap profile by closure type shows it as a growing THUNK band.

A splay tree is a binary search tree that keeps no balance information and instead moves every node it accesses to the root, by a sequence of rotations called splaying. Single operations can take linear time, but any sequence of m operations on a tree of n nodes takes O((m + n) log n) time, so each operation is logarithmic amortized. Because recently used keys end up near the root, splay trees adapt to the access pattern.

The square-free decomposition of a polynomial writes it as f = f_1 f_2^2 f_3^3 ..., where the f_i are square-free and pairwise coprime, so f_i collects the irreducible factors of multiplicity i. It needs only greatest common divisors with the derivative, not factorization, because gcd(f, f') contains every repeated factor with its multiplicity reduced by one. Yun's algorithm computes it at the cost of about one gcd. In characteristic p a p-th power has zero derivative, and the algorithm must take p-th roots.

The subresultant polynomial remainder sequence is a way of running Euclid's algorithm on polynomials over the integers, or any integral domain, without fractions and without the exponential coefficient growth of plain pseudo-division. After each pseudo-division, the remainder is divided by a factor computed from the previous leading coefficients and degree differences; the division is always exact, and the remainders obtained are the subresultants of the input, determinants of submatrices of the Sylvester matrix, whose size grows only linearly with the degree. The sequence yields the gcd, up to a constant, and the resultant. It was introduced by Collins in 1967 and developed by Brown and Traub.

The Swinnerton-Dyer polynomials are the integer polynomials SD_k(x) = ∏(x ± √p₁ ± √p₂ ± … ± √p_k), taken over all 2^k sign choices, for the first k primes. They are irreducible over the integers but factor into polynomials of degree at most two modulo every prime, because their Galois group (ℤ/2)^k has no element of order greater than two. They are the worst case for the Berlekamp–Zassenhaus factoring algorithm: every prime yields at least 2^(k−1) modular factors, and before concluding that the polynomial is irreducible the algorithm must try exponentially many subsets of them. They motivated the lattice-based factoring algorithms of Lenstra, Lenstra and Lovász and of van Hoeij.

A tail call is a call made as the last action of a function, whose result the caller returns unchanged. Since the caller has nothing left to do, its stack frame can be reused, and the call compiled as a jump; a language that does this for every tail call is properly tail recursive, and loops can be written as recursion without the stack growing. OCaml, Scheme and most functional languages guarantee it; the JVM, Python and most JavaScript engines do not.

In an SMT solver, a theory solver decides whether a conjunction of literals of one theory, such as linear arithmetic or equality with uninterpreted functions, is consistent. The SAT search asserts literals to it incrementally and asks it to check them; on inconsistency it returns an explanation, a small subset of the asserted literals that is already inconsistent, which the SAT search learns as a clause. A theory solver must also undo assertions when the search backtracks, and it may propagate literals that the asserted ones imply. The quality of explanations and propagation largely determines the solver's performance.

Thompson's construction converts a regular expression into a nondeterministic finite automaton with epsilon-transitions by structural recursion: each symbol becomes a two-state automaton, and concatenation, alternation and Kleene star combine the automata of the subexpressions by adding at most two states and a few epsilon-transitions. The resulting automaton has at most 2m states for an expression of size m, and it can be simulated on a string of length n in O(mn) time by tracking the set of states it could be in, which avoids the exponential worst case of backtracking matchers. Ken Thompson described it in 1968; it is the basis of grep, RE2 and most regular expression engines with guaranteed running time.

A three-way merge combines two versions of a document that were derived independently from a common ancestor, the base. Comparing each version with the base shows which side changed each region: a region changed on one side only is taken from that side, a region changed identically on both is taken once, and a region changed differently on both is a conflict left for a person to resolve. The base is what makes the merge possible; with only the two versions, an added line cannot be told from a deleted one. The diff3 algorithm is the standard line-based three-way merge, and it is what version control systems such as Git use to merge files.

Traversable is the abstraction of a container that can be rebuilt while an applicative effect is performed on each element in order: traverse : (a -> f b) -> t a -> f (t b). Validating every element, parsing each string, numbering the nodes of a tree and taking cartesian products are all traversals with different applicative functors. traverse subsumes both map (with the identity functor) and foldMap (with a constant functor into a monoid), and it satisfies laws saying it visits every element exactly once.

A trie, or prefix tree, is a tree for a set of strings in which each edge is labelled with a character and each key is the path from the root to a node; keys with a common prefix share the nodes of that prefix. Lookup and insertion take time proportional to the length of the key, independent of the number of keys, and all keys with a given prefix are found in one subtree, in sorted order. Radix and Patricia trees compress chains of single-child nodes, and the same idea applies to integers, read bit by bit.

The Tseitin transformation converts an arbitrary propositional formula or Boolean circuit into conjunctive normal form in linear time by introducing a new variable for each subformula and adding a few clauses that define it as the result of its operator: g ↔ a ∧ b becomes (¬g ∨ a), (¬g ∨ b) and (g ∨ ¬a ∨ ¬b). The result is not equivalent to the original formula but equisatisfiable, and every model of one extends or restricts to a model of the other. It is how SAT solvers receive circuits and structured formulas; the Plaisted–Greenbaum variant emits only the implications required by each subformula's polarity, roughly halving the clauses.

Type-directed disambiguation is OCaml's rule, since version 4.01, for deciding which record type a field label, or which variant type a constructor, belongs to when several in scope share the name: if the expected type is already known at that point of type inference, it decides; otherwise the most recently defined type with that name wins. It also lets labels and constructors be used without being in scope when the type is known. Because the outcome depends on what inference knows at each point, the -principal flag warns when a choice relied on information that a different inference order might not have had.

Union–find, or a disjoint-set forest, maintains a partition of a set into disjoint classes under two operations: union merges two classes, and find returns a representative of an element's class. Each class is a tree of parent pointers whose root is the representative. With union by rank and path compression, any sequence of m operations on n elements takes O(m α(n)) time, where α is the inverse Ackermann function, which is at most 4 for any practical n.

Unit propagation is the inference rule at the core of SAT solvers: when every literal of a clause is false under the current partial assignment except one unassigned literal, that literal must be true. Applying the rule until nothing changes either extends the assignment or finds a clause with every literal false, a conflict. It decides satisfiability of Horn formulas on its own, it takes most of the running time of a modern CDCL solver, and it is implemented with two watched literals per clause so that only clauses that may have become unit are ever inspected.

The value restriction is the rule, in ML-family languages, that a let-bound expression has its type variables generalized only if it is a syntactic value, such as a function, a constant or a constructor applied to values. An application such as List.map f or ref [] is not a value, so its type variables stay weak and are fixed by their first use. Without the restriction, a reference could be given a polymorphic type and used to store a value at one type and read it at another. OCaml relaxes the rule for type variables that occur only covariantly.

A van Laarhoven lens is a lens represented as a single function polymorphic over functors: forall f. Functor f => (a -> f a) -> s -> f s. Instantiating the functor gives the operations: the constant functor yields the getter and the identity functor the setter. Lenses in this form compose with ordinary function composition, and replacing Functor with Applicative gives traversals, which compose with lenses the same way. The representation is the basis of Haskell's lens library.

VSIDS, Variable State Independent Decaying Sum, is the branching heuristic of conflict-driven SAT solvers. Each variable has an activity score, which is increased whenever the variable takes part in a conflict and decays geometrically over time; when the solver must make a decision, it branches on the unassigned variable with the highest activity. The heuristic is cheap, because it depends on conflicts rather than on the current formula, and it focuses the search on the variables involved in recent conflicts. It was introduced by the Chaff solver in 2001 and, in the exponential form used by MiniSat, remains the default in most solvers.

The two-watched-literal scheme is the data structure SAT solvers use to detect unit and conflicting clauses. Each clause of two or more literals watches two of its literals that are not false; a clause is examined only when one of its watched literals becomes false, and then it either finds a replacement watch, becomes unit, or is a conflict. Because the watches remain valid when assignments are undone, backtracking costs nothing, and a clause with many literals is touched only when its watches are hit. Introduced by the Chaff solver in 2001, it made unit propagation, which dominates solver time, several times faster.

A weak reference is a pointer the garbage collector ignores when deciding reachability, so a cache or registry can refer to a value without keeping it alive; once nothing else refers to the value, it may be collected and the weak reference then reads as empty. Weak references alone do not make a memo table safe, because a cached value that mentions its key keeps the key alive through the table. An ephemeron fixes this: it holds a key weakly and a value that is retained only while the key is reachable from elsewhere.

The Y combinator is a lambda term Y such that Y f = f (Y f) for every f: it finds a fixed point of any function, and so gives recursion to a language with no named definitions. Under call-by-value it loops before f is ever called; the Z combinator delays the self-application behind a lambda and works in strict languages. No fixed-point combinator has a type in the simply typed lambda calculus.

For a functor F and an object a, natural transformations from Hom(a, -) to F correspond one to one with elements of F a. In Haskell, forall b. (a -> b) -> f b is isomorphic to f a, and the left-hand form turns a chain of fmaps into one composed function and a single fmap.

A zipper represents a data structure together with a focus, a position inside it: the substructure at the focus, and the path from the focus back to the root together with everything to either side of that path. Moving the focus one step and editing at the focus take constant time, and the structure is persistent, so edits share everything off the path. The type of paths is the derivative of the structure's type, in the sense of calculus.