Reference
The Applied Higher-Order Functions catalogue
322 modules in src/rainbow/algorithms/proofs/ahof/. All folders
| Module | What it proves | Theorems |
|---|---|---|
| algorithms.proofs.ahof.ac-mcts | AHoF D56 Actor-Critic with MCTS: guide tree search by the critic and select the child with the larger UCB-augmented value; it keeps the larger value: prefers-child-zero? | 3 |
| algorithms.proofs.ahof.accuracy | AHoF Classification Accuracy: the simplest evaluation metric -- the fraction of predictions that are correct, accuracy correct total = correct / total, a value in [0, 1]. | 2 |
| algorithms.proofs.ahof.activity-selection | AHoF Activity Selection (greedy interval scheduling): from a set of activities with start and finish times, select the largest set of mutually compatible (non-overlapping) activities. | 3 |
| algorithms.proofs.ahof.actor-critic | AHoF D53 Actor-Critic: the critic bootstraps a temporal-difference target from the immediate reward plus the discounted value of the next state, and the actor is updated toward it. | 4 |
| algorithms.proofs.ahof.adaboost | AHoF AdaBoost (Adaptive Boosting): combine many weak classifiers into a strong one by a weighted majority vote, where each weak learner's vote weight alpha = (1/2) ln((1 - err)/err) DECREASES with its weighted error err -- more accurate learners get larger votes, and after each round the misclassified examples are up-weighted so the next learner focuses on them. | 3 |
| algorithms.proofs.ahof.adaptive-is | AHoF V28 Adaptive Importance Sampling: iteratively refine the proposal and reweight samples by the ratio of the target density to the current proposal density: reweight target proposal = target / proposal. | 3 |
| algorithms.proofs.ahof.agent-model | AHoF V3 Agent Model Construction: fit a model of another agent's behaviour; the model fits when its prediction error is within the tolerance: model-fits? | 4 |
| algorithms.proofs.ahof.alpha-vector | AHoF D71 Alpha Vector (Exact POMDP value function): the optimal value at a belief b is the maximum over the alpha-vector set of the inner products <alpha, b>. | 3 |
| algorithms.proofs.ahof.articulation-points | AHoF Articulation Points (Tarjan's DFS low-link algorithm): find the cut vertices of an undirected graph -- those whose removal disconnects it -- in O(V + E), the basis of network-reliability and bridge analysis. | 3 |
| algorithms.proofs.ahof.astar | AHoF D37 A* / heuristic search: the priority by which A* expands nodes is the estimated total cost through a node, the path cost so far plus the heuristic estimate of the cost to go: f g h = g + h over exact-rational costs. | 3 |
| algorithms.proofs.ahof.astar-falsification | AHoF V18 A* for Falsification: search the space of system behaviours for a specification violation using A*, ordering the frontier by the f-cost f = g + h (the cost so far plus an admissible heuristic to a likely violation) and always expanding the lowest-f node: priority g h = g + h prefers-lower? | 3 |
| algorithms.proofs.ahof.async-value-iteration | AHoF D23 worked asynchronous (Gauss-Seidel) value-iteration instance. | 8 |
| algorithms.proofs.ahof.backtracking | AHoF O14 Backtracking Line Search: shrink the step until the Armijo sufficient- decrease condition holds -- the new objective is at or below the predicted decrease bound f(x) + c*alpha*slope: sufficient-decrease? | 4 |
| algorithms.proofs.ahof.baseline-subtraction | AHoF D48 Baseline Subtraction: the variance-reduction wrapper for policy-gradient estimators. | 3 |
| algorithms.proofs.ahof.bayes-adaptive-mdp | AHoF D60 Bayes-Adaptive MDP: plan in the belief-MDP over unknown model parameters, where the value of an action is the posterior-belief-weighted average of its value under each candidate model: expected-value b0 v0 b1 v1 = b0 * v0 + b1 * v1 (belief weights b0, b1 summing to one). | 4 |
| algorithms.proofs.ahof.bayes-net | AHoF D1 Bayesian Network Representation: the joint distribution factorizes as a product of conditional-probability factors; the joint mass of two factors is their product joint-factor a b = a * b. | 4 |
| algorithms.proofs.ahof.bayes-theorem | AHoF Bayes' Theorem: invert a conditional probability to obtain the posterior belief in a hypothesis H after observing evidence E, posterior likelihood prior evidence = (likelihood * prior) / evidence i.e. | 2 |
| algorithms.proofs.ahof.bayesian-learning | AHoF D11 worked Bayesian parameter learning over exact rationals. | 3 |
| algorithms.proofs.ahof.bayesian-model-estimation | AHoF D59 Bayesian Model Estimation: score candidate models by their posterior probability, which is proportional to the data likelihood under the model times the model prior: posterior-score likelihood prior = likelihood * prior. | 4 |
| algorithms.proofs.ahof.bayesian-opt | Kochenderfer surrogate-optimization / model-validation cores as higher-order-function compositions, proved axiom-free, extending the 222 AHoF catalog: O19.1 probability of improvement : acquisition prefers candidates beating the best O19.3 SafeOpt : query only within the high-confidence safe set O17.14 0.632 bootstrap : convex combo 0.368*train + 0.632*test error O17.12 bootstrap generalization : | 4 |
| algorithms.proofs.ahof.bayesian-optimization | AHoF O65 Bayesian Optimization Loop: iterate (fit surrogate -> maximize acquisition -> evaluate) and track the best observation seen. | 3 |
| algorithms.proofs.ahof.bayesian-param | AHoF V2 Bayesian Parameter Learning: infer model parameters by their posterior, which is proportional to the data likelihood under the parameter times the parameter prior: posterior-score likelihood prior = likelihood * prior. | 4 |
| algorithms.proofs.ahof.beam-search | AHoF D-family Beam Search: a bounded-breadth heuristic search that, at each level, expands only the K highest-scoring partial solutions (the beam) instead of the full frontier -- trading completeness for tractable memory, as in machine translation decoding and structured prediction. | 3 |
| algorithms.proofs.ahof.behavioral-cloning | AHoF D64 Behavioral Cloning (imitation learning): train a policy by supervised learning to reproduce an expert's actions, minimizing an imitation loss. | 4 |
| algorithms.proofs.ahof.belief-propagation | AHoF D4 Sum-Product (Belief Propagation): approximate marginal inference by passing messages on the factor graph until convergence. | 3 |
| algorithms.proofs.ahof.bellman-ford | AHoF Bellman-Ford single-source shortest paths: unlike Dijkstra, it handles edges of any (including negative) weight by relaxing EVERY edge repeatedly for V-1 passes, and detects a negative-weight cycle if some edge still STRICTLY decreases a distance on a V-th pass. | 3 |
| algorithms.proofs.ahof.bfgs | AHoF O29 BFGS: a quasi-Newton method whose Hessian-approximation update uses the gradient change y = g_{k+1} - g_k: gradient-change g-new g-old = g-new - g-old. | 3 |
| algorithms.proofs.ahof.bfs-reachability | AHoF V48 BFS/DFS Graph Reachability: explore the state graph to decide whether a target is reachable; a state is within the explored frontier when its distance to the frontier representative is within the radius: reachable? | 4 |
| algorithms.proofs.ahof.bin-packing | AHoF Bin Packing (First-Fit approximation): pack items of given sizes into the fewest unit-capacity bins. | 3 |
| algorithms.proofs.ahof.binary-heap | AHoF Binary Heap: the array-backed complete binary tree behind the priority queue and heapsort, maintaining the HEAP PROPERTY -- in a min-heap every parent key is at most its children's keys, so the minimum is always at the root. | 3 |
| algorithms.proofs.ahof.binary-search | AHoF Binary Search: locate a target in a SORTED array in O(log n) by repeatedly halving the search interval -- comparing the target to the middle element and discarding the half that cannot contain it. | 3 |
| algorithms.proofs.ahof.bipartite-matching | AHoF Maximum Bipartite Matching (augmenting-path / Hungarian tree method): find the largest set of edges with no shared endpoints in a bipartite graph -- the model for job/worker assignment, scheduling, and network routing. | 3 |
| algorithms.proofs.ahof.bisection | AHoF O12 worked bisection bracket search over exact rationals. | 4 |
| algorithms.proofs.ahof.bloom-filter | AHoF Bloom Filter: a space-efficient probabilistic set that answers membership with NO FALSE NEGATIVES (if it says absent, the element was never added) but possible false positives. | 3 |
| algorithms.proofs.ahof.boyer-moore | AHoF Boyer-Moore Majority Vote: find the element that appears MORE than n/2 times (if one exists) in O(n) time and O(1) space -- a single streaming pass that keeps just a candidate and a counter, incrementing on a match and decrementing otherwise (replacing the candidate when the counter hits zero). | 3 |
| algorithms.proofs.ahof.branch-and-bound | AHoF D34 worked Branch and Bound pruning step over exact rationals, reusing the shared bounding lemma (rainbow.algorithms.proofs.branch-and-bound, branch-and-bound/*). | 4 |
| algorithms.proofs.ahof.bucket-sort | AHoF Bucket Sort: sort values drawn from a uniform range in EXPECTED linear time by distributing them into ordered buckets by value, sorting each bucket (with any comparison sort), and CONCATENATING the buckets in order. | 3 |
| algorithms.proofs.ahof.ce-falsification | AHoF V15 Cross-Entropy for Falsification: fit the sampling distribution to the failure region by keeping the elite (lowest-cost) samples below the cross-entropy quantile: elite? | 4 |
| algorithms.proofs.ahof.central-difference | AHoF O2 Central Difference: the central finite difference estimates a derivative as (f(x+h) - f(x-h)) / (2h). | 3 |
| algorithms.proofs.ahof.chebyshev-scalarization | AHoF multi-objective method: weighted-Chebyshev (max-norm) scalarization. | 4 |
| algorithms.proofs.ahof.christofides | AHoF Christofides Algorithm: the best-known polynomial APPROXIMATION for the metric Travelling Salesman Problem. | 3 |
| algorithms.proofs.ahof.clamped-surrogate | AHoF D52 Clamped Surrogate Objective (PPO): stabilize policy-gradient updates by clamping the probability ratio r into the trust region [lo, hi] = [1-eps, 1+eps] before forming the surrogate objective: clamp r lo hi = min (max r lo) hi. | 3 |
| algorithms.proofs.ahof.cmaes | AHoF O42 CMA-ES (Covariance Matrix Adaptation Evolution Strategy) -- the mean recombination step. | 3 |
| algorithms.proofs.ahof.cmaes-falsification | AHoF V14 CMA-ES for Falsification: adapt a Gaussian search distribution toward the failure region using the elite (lowest-cost) samples; a sample is elite when its cost is within the elite quantile: elite? | 4 |
| algorithms.proofs.ahof.coin-change | AHoF Coin Change (dynamic programming): the minimum number of coins that sum to a target amount, from unlimited coins of given denominations -- the canonical unbounded-knapsack-style min-DP. | 4 |
| algorithms.proofs.ahof.column-generation | AHoF O-family Column Generation: solve a large linear program with too many variables to enumerate by working with a small RESTRICTED master problem and generating new columns only as needed. | 3 |
| algorithms.proofs.ahof.complex-step | AHoF O3 Complex-Step Derivative (classical method: f'(x) ~ Im f(x + ih) / h, which avoids subtractive cancellation). | 3 |
| algorithms.proofs.ahof.composite-metric | AHoF V5 worked composite metric over exact rationals, combining an accuracy of 3/4 and a precision of 1/4. | 3 |
| algorithms.proofs.ahof.concrete-reachability | AHoF V44 Concrete Reachability: the simplest reachability analysis -- push a finite set of concrete sample states one step forward through the dynamics and collect the images. | 3 |
| algorithms.proofs.ahof.confidence-interval | AHoF Confidence Interval: quantify the uncertainty of a point estimate by an interval that, over repeated sampling, covers the true parameter with a chosen confidence level (e.g. | 4 |
| algorithms.proofs.ahof.conformal | AHoF Conformal Prediction: a distribution-free method that turns any point predictor into set-valued predictions with a finite-sample coverage guarantee. | 3 |
| algorithms.proofs.ahof.conjugate-gradient | AHoF O18 worked conjugate gradient over signed rationals with pair state. | 4 |
| algorithms.proofs.ahof.constrained-ls | Kochenderfer 'Algorithms for Optimization' Ch.11/13 constrained least-squares / distributed cores as higher-order-function compositions, proved axiom-free, extending the 222 AHoF catalog: O13.2 least squares w/ inequalities (LSI) : feasibility test g.x >= h (decidable) O13.3 least distance programming (LDP) : minimum-norm feasible point (min) O11.8 consensus ADMM : consensus variable = weighted av | 4 |
| algorithms.proofs.ahof.coordinate-search | AHoF O32 worked cyclic coordinate search over signed-rational pair state. | 4 |
| algorithms.proofs.ahof.correlated-equilibrium | AHoF D78 Correlated Equilibrium: a distribution over joint action profiles from which no player has an incentive to deviate from the mediator's recommendation; the per-player adherence test compares a deviation payoff against the recommended one: follows-recommendation? | 4 |
| algorithms.proofs.ahof.cosine-similarity | AHoF Cosine Similarity: measure the similarity of two vectors by the cosine of the angle between them -- the dot product normalized by the product of their magnitudes, cosine dot-product magnitude-product = (a . | 2 |
| algorithms.proofs.ahof.counterfactual-cf | AHoF V57 Counterfactual Explanation: explain a model decision by the smallest change to the input that flips the prediction to a desired class. | 4 |
| algorithms.proofs.ahof.counting-sort | AHoF Counting Sort: a stable, NON-comparison, O(n + k) sort for integer keys in a small range [0, k). | 2 |
| algorithms.proofs.ahof.cross-entropy | AHoF O41 Cross-Entropy Method: a model-based stochastic optimizer that, each iteration, samples a population, keeps the top-scoring ELITE, and refits the sampling distribution to the elite. | 3 |
| algorithms.proofs.ahof.cross-entropy-is | AHoF V29 Cross-Entropy Importance Sampling: iteratively fit the sampling distribution to the rare failure region by keeping the elite samples -- those whose cost falls at or below the current elite quantile threshold: elite? | 4 |
| algorithms.proofs.ahof.cross-validation | AHoF V4 worked cross-validation over exact rationals. | 3 |
| algorithms.proofs.ahof.cutting-planes | AHoF O73 Cutting Planes: solve an integer/convex program by iteratively adding linear inequalities (cuts) that remove the current fractional/infeasible LP solution while preserving all true solutions. | 3 |
| algorithms.proofs.ahof.cyk | AHoF CYK Algorithm (Cocke-Younger-Kasami): decide whether a string is generated by a context-free grammar in Chomsky Normal Form, in O(n^3 * |G|), by dynamic programming over substrings. | 3 |
| algorithms.proofs.ahof.dagger | AHoF D65 DAgger (Dataset Aggregation for imitation learning): iteratively run the current policy, query the expert to label the visited states, and aggregate; the expert is queried when the policy's uncertainty reaches a query threshold: query-expert? | 4 |
| algorithms.proofs.ahof.dbscan | AHoF DBSCAN (Density-Based Spatial Clustering of Applications with Noise): find clusters of arbitrary shape as dense regions separated by sparse ones, labelling low-density points as noise -- without needing the number of clusters in advance. | 3 |
| algorithms.proofs.ahof.dcp | AHoF O57 Disciplined Convex Programming: express a convex program from a grammar of convex atoms so feasibility of each convex inequality constraint g(x) <= b reduces to a decidable exact-rational comparison of the constraint value against its bound: constraint-satisfied? | 4 |
| algorithms.proofs.ahof.dec-pomdp-dp | AHoF D82 Dec-POMDP (Dynamic Programming): back up joint-policy values, keeping the larger of two candidate joint-policy values: prefers-joint-zero? | 3 |
| algorithms.proofs.ahof.dec-pomdp-hs | AHoF D83 Dec-POMDP Heuristic Search: search the space of joint policies with heuristic bounds; converged when the bound gap is within precision: converged? | 4 |
| algorithms.proofs.ahof.decision-network | AHoF D18 worked decision network evaluation over exact rationals. | 4 |
| algorithms.proofs.ahof.decision-tree | AHoF D-family Decision Tree learning (greedy top-down induction): at each node, split on the feature that most improves purity -- i.e. | 4 |
| algorithms.proofs.ahof.deterministic-pg | AHoF D55 Deterministic Policy Gradient: the DPG theorem gives the gradient as the chain product of the action-value gradient and the policy Jacobian, grad = ∇_a Q · ∇_θ μ: policy-gradient q-grad mu-grad = q-grad * mu-grad (over signed). | 3 |
| algorithms.proofs.ahof.dfp | AHoF O28 DFP (Davidon-Fletcher-Powell): a quasi-Newton method whose curvature update uses the step vector s = x_{k+1} - x_k: step-vector x-new x-old = x-new - x-old. | 3 |
| algorithms.proofs.ahof.dijkstra | AHoF Dijkstra's Shortest Path: single-source shortest paths on a graph with NON-NEGATIVE edge weights. | 3 |
| algorithms.proofs.ahof.direct | AHoF O37 DIRECT (DIvided RECTangles): a Lipschitzian global optimizer that partitions the domain into rectangles and subdivides the 'potentially optimal' ones. | 3 |
| algorithms.proofs.ahof.direct-sampling | AHoF D5 Direct Sampling: draw a sample from a Bayesian network by ancestral sampling, drawing each variable from its conditional distribution given already sampled parents. | 3 |
| algorithms.proofs.ahof.discrete-filter | AHoF D66 Discrete State Filter (recursive Bayesian filtering over a finite state space): each step multiplies the prior belief in a state by the measurement likelihood to get the unnormalized posterior weight, then renormalizes: posterior-weight likelihood prior = likelihood * prior. | 4 |
| algorithms.proofs.ahof.discrete-search | Kochenderfer discrete-search / sampling / metaheuristic cores as higher-order-function compositions, proved axiom-free, extending the 222 AHoF catalog: O22.7 0-1 knapsack DP : cell = max(exclude value, include value) V5.4 RRT nearest-node : steer toward the nearest existing node (min distance) V5.8 star discrepancy bound : worst-case box discrepancy = max over sub-boxes O22.10 ant colony optimizat | 6 |
| algorithms.proofs.ahof.disturbance-falsification | AHoF V10 Disturbance-Based Falsification: search bounded disturbances to drive the system to a violation; a violation is found when the achieved robustness drops to or below the margin: violation? | 4 |
| algorithms.proofs.ahof.dual-simplex | AHoF O55 Dual Simplex Method: solve a linear program by maintaining DUAL feasibility (reduced costs of the right sign) while iterating toward primal feasibility. | 3 |
| algorithms.proofs.ahof.dutch-flag | AHoF Dutch National Flag (Dijkstra's 3-way partition): partition an array around a pivot into three regions -- less than, equal to, and greater than -- in a single O(n) pass with O(1) extra space. | 3 |
| algorithms.proofs.ahof.edmonds-karp | AHoF Edmonds-Karp Algorithm: compute the maximum flow through a network in O(V*E^2) by repeatedly finding a SHORTEST augmenting path (by BFS) in the residual graph and pushing flow along it, until none remains -- a concrete polynomial realization of Ford-Fulkerson. | 3 |
| algorithms.proofs.ahof.ekf | AHoF D68 Extended Kalman Filter: the EKF linearizes the nonlinear process and measurement models about the current estimate and applies the standard Kalman measurement update, blending the prediction with the observation by the Kalman gain: update wp prior wm measurement = wp * prior + wm * measurement (with wp + wm = 1 the complementary predict/measurement weights). | 4 |
| algorithms.proofs.ahof.eligibility-traces | AHoF D63 worked eligibility traces (TD(lambda)) over exact rationals. | 3 |
| algorithms.proofs.ahof.ellipsoid | AHoF V36 Ellipsoid Propagation: over-approximate a reachable set by an ellipsoid; a point lies inside when its quadratic form (x-c)'P(x-c) is within the ellipsoid limit: in-ellipsoid? | 4 |
| algorithms.proofs.ahof.em | AHoF D13 EM Algorithm: fit latent-variable model parameters by alternating an E-step (compute the expected complete-data log-likelihood under the current parameters) and an M-step (maximize it). | 3 |
| algorithms.proofs.ahof.ensemble-disagreement | AHoF V61 Ensemble Disagreement: quantify predictive uncertainty by the spread of an ensemble's predictions and flag an input as uncertain when the disagreement reaches a threshold: flag-uncertain? | 3 |
| algorithms.proofs.ahof.epsilon-constraint | AHoF O67 Epsilon-Constraint Method (multi-objective): optimize one objective while the others are turned into inequality constraints f_i <= epsilon_i. | 3 |
| algorithms.proofs.ahof.epsilon-greedy | AHoF epsilon-greedy exploration: the canonical explore/exploit rule for bandits and reinforcement learning. | 4 |
| algorithms.proofs.ahof.exact-inference | AHoF D2 worked exact Bayesian inference by enumeration. | 3 |
| algorithms.proofs.ahof.expected-improvement | AHoF O63 Expected Improvement acquisition (Bayesian optimization). | 4 |
| algorithms.proofs.ahof.exploration-strategies | Kochenderfer 'Algorithms for Decision Making' Ch.15 bandit exploration strategies, expressed as higher-order-function compositions and proved axiom-free (core structural property per algorithm), extending the 222 AHoF catalog: D15.3 epsilon-greedy : explore/exploit branch (Bool) over a random bit D15.4 explore-then-commit : two-phase branch on a round>=k threshold (decide-at-most) D15.5 softmax ex | 8 |
| algorithms.proofs.ahof.f1-score | AHoF F1 Score: the standard single-number summary of a classifier's quality on imbalanced data -- the HARMONIC MEAN of precision and recall, f1 precision recall = 2 * precision * recall / (precision + recall). | 2 |
| algorithms.proofs.ahof.failure-mode | AHoF V58 Failure Mode Characterization: cluster observed failures into modes and assign a new failure to a mode when its distance to the mode's centroid is within the mode radius: in-mode? | 4 |
| algorithms.proofs.ahof.failure-probability-monitor | AHoF V64 worked failure-probability monitor over exact rationals with risk threshold 1/2. | 5 |
| algorithms.proofs.ahof.falsification | AHoF V9 Direct Sampling Falsification: the simplest falsification method -- sample inputs, simulate, and return the first whose specification robustness has dropped to the falsification margin. | 3 |
| algorithms.proofs.ahof.falsification-opt | AHoF V12 Falsification as Optimization: cast falsification as minimizing the STL robustness of the specification over inputs; a violation is found when the achieved robustness drops to or below the violation margin: violation-found? | 4 |
| algorithms.proofs.ahof.feasibility | Constraint feasibility checking (the conjunctive dual of the SAT clause and the model-checking companion of V50): a candidate is feasible when ALL of its constraints are satisfied. | 4 |
| algorithms.proofs.ahof.fenwick-tree | AHoF Fenwick Tree (Binary Indexed Tree): maintain prefix sums of an array under point updates, both in O(log n), using a clever low-bit indexing where each index is responsible for a range of size equal to its lowest set bit. | 2 |
| algorithms.proofs.ahof.fibonacci-search | AHoF O8 worked Fibonacci Search reduction step over exact rationals, reusing the shared bracket-reduction lemma (rainbow.algorithms.proofs.golden-section-search, linesearch/*). | 5 |
| algorithms.proofs.ahof.fictitious-play | AHoF D79 Fictitious Play: in a repeated game each player best-responds to the empirical frequency of the opponent's past actions. | 3 |
| algorithms.proofs.ahof.finite-state-controller | AHoF D76 Finite State Controller: a POMDP policy as a finite-state machine; at a controller node it selects the higher-value action; it keeps the larger value: prefers-action-zero? | 3 |
| algorithms.proofs.ahof.fisher-yates | AHoF Fisher-Yates Shuffle (Knuth shuffle): produce a UNIFORMLY RANDOM permutation of an array in O(n) time in place -- every one of the n! | 3 |
| algorithms.proofs.ahof.floyd-cycle | AHoF Floyd's Cycle Detection (tortoise and hare): detect a cycle in a linked list or a functional sequence x_{n+1} = f(x_n) in O(1) extra space, by advancing a SLOW pointer one step and a FAST pointer two steps per iteration. | 3 |
| algorithms.proofs.ahof.forward-difference | AHoF O1 Forward Difference: approximate a derivative by the forward finite difference (f(x+h) - f(x)) / h. | 3 |
| algorithms.proofs.ahof.forward-mode-ad | AHoF O4 Forward-Mode Auto-Diff: propagate derivatives through a computation with dual numbers; the chain rule composes derivatives multiplicatively (f∘g)'=f'(g)·g': dual-derivative outer-deriv inner-deriv = outer-deriv * inner-deriv (over signed). | 3 |
| algorithms.proofs.ahof.forward-reachability | AHoF V33 Forward Reachability: over-approximate the set of states reachable from an initial set by forward-propagating an enclosure; a state is in the forward-reachable over-approximation when its distance to the reachable-set representative is within the enclosure radius: in-reachable-set? | 4 |
| algorithms.proofs.ahof.forward-search | AHoF D33 Forward Search: finite-horizon lookahead planning. | 3 |
| algorithms.proofs.ahof.fractional-knapsack | AHoF Fractional Knapsack: unlike the 0/1 version (which needs DP), when items may be taken in fractional amounts the problem is solved OPTIMALLY by a simple greedy rule -- take items in decreasing order of value density (value / weight), filling the knapsack and splitting the last item that does not fully fit. | 3 |
| algorithms.proofs.ahof.frank-wolfe | AHoF O-family Frank-Wolfe (Conditional Gradient) method: minimize a convex objective over a convex set WITHOUT projections. | 3 |
| algorithms.proofs.ahof.fuzzing | AHoF V11 Fuzzing: generate test inputs by repeatedly mutating a seed input and checking whether any mutant violates the specification. | 4 |
| algorithms.proofs.ahof.ga-policy | AHoF D41 GA for Policy Search: evolve policies under fitness selection, keeping the fitter individual: prefers-fitter? | 3 |
| algorithms.proofs.ahof.gae | AHoF D42 Generalized Advantage Estimation: estimate the advantage function as an exponentially-weighted (by gamma*lambda) sum of temporal-difference errors, A_t = delta_t + (gamma*lambda) delta_{t+1} + (gamma*lambda)^2 delta_{t+2} + ... | 2 |
| algorithms.proofs.ahof.gae54 | AHoF D54 Generalized Advantage Estimation: form a low-variance advantage estimate as an exponentially-weighted sum of one-step TD residuals; the recursive form combines the current residual with the discounted future advantage: gae-advantage delta lambda-gamma next-advantage = delta + lambda-gamma * next-advantage. | 4 |
| algorithms.proofs.ahof.game-ascent | AHoF D80 Gradient Ascent (Games): each player ascends its own payoff gradient, updating ascent-step theta step = theta + step. | 3 |
| algorithms.proofs.ahof.game-equilibria | Kochenderfer 'Algorithms for Decision Making' Ch.24-27 multi-agent equilibrium cores as higher-order-function compositions, proved axiom-free, extending the 222 AHoF catalog. | 4 |
| algorithms.proofs.ahof.gas-station | AHoF Gas Station (greedy circular tour): around a circle of stations, station i provides gas[i] and it costs cost[i] to drive to the next. | 3 |
| algorithms.proofs.ahof.gauss-seidel | Gauss-Seidel coordinate update (Kochenderfer Optimization O24.1), the last of the four signed-cluster algorithms deferred in August. | 2 |
| algorithms.proofs.ahof.gaussian-inference | AHoF D9 Inference in Gaussian Models: exact closed-form conjugate updates. | 3 |
| algorithms.proofs.ahof.gaussian-process | AHoF O62 Gaussian Process (surrogate model / regression): the GP posterior mean at a query point is a kernel-weighted combination of the observed targets, the weights coming from the covariance between the query and the training points: posterior-mean w0 y0 w1 y1 = w0 * y0 + w1 * y1. | 4 |
| algorithms.proofs.ahof.general-descent | AHoF O13 worked general descent, instantiated to gradient descent. | 3 |
| algorithms.proofs.ahof.genetic-programming | AHoF O70 Genetic Programming: evolve programs represented as expression trees under fitness selection; between two candidate programs it keeps the fitter (higher- fitness) one: prefers-fitter? | 3 |
| algorithms.proofs.ahof.gibbs | AHoF D8 Gibbs Sampling: an MCMC method that samples a joint distribution by repeatedly resampling one coordinate at a time from its full conditional given all the others. | 3 |
| algorithms.proofs.ahof.gibbs-failures | AHoF V23 Gibbs Sampling (Failures): reuse the Gibbs structure over the failure region, resampling each variable from its full conditional; the draw is from the conditional when the uniform sample falls under the conditional mass: draws-conditional? | 4 |
| algorithms.proofs.ahof.gini-impurity | AHoF Gini Impurity: the node-purity criterion used by CART decision trees (and a cheaper alternative to entropy). | 3 |
| algorithms.proofs.ahof.golden-section-search | AHoF O9 worked Golden Section Search reduction step over exact rationals. | 5 |
| algorithms.proofs.ahof.gradient-ascent | AHoF D49 worked bounded fixed-rate gradient-ascent instance. | 3 |
| algorithms.proofs.ahof.gradient-boosting | AHoF Gradient Boosting (GBM / the core of XGBoost, LightGBM): build a strong predictor as an additive ensemble, where each stage fits a weak learner (usually a shallow tree) to the negative gradient of the loss (the residuals) and adds a SHRUNKEN version of it to the running model: boost-update current learning-rate weak = current + learning-rate * weak The learning rate (shrinkage) < 1 regularize | 2 |
| algorithms.proofs.ahof.gradient-clipping | AHoF Gradient Clipping (clip-by-norm): stabilize the training of deep and recurrent networks by capping the gradient's magnitude, preventing the exploding-gradient problem where a single huge update destroys the model. | 3 |
| algorithms.proofs.ahof.gradient-descent | AHoF O17 worked bounded gradient descent over signed rationals. | 3 |
| algorithms.proofs.ahof.grammatical-evolution | AHoF O71 Grammatical Evolution: evolve programs by mapping integer genomes through a BNF grammar, then select by fitness; between two individuals it keeps the fitter one: prefers-fitter? | 3 |
| algorithms.proofs.ahof.graph-coloring | AHoF Greedy Graph Coloring: assign colors to vertices so no edge joins two of the same color, using few colors -- the model for register allocation, exam scheduling, and frequency assignment. | 3 |
| algorithms.proofs.ahof.greedy-policy | AHoF greedy policy extraction: given a state-action value function Q(s, .), the greedy policy chooses the action of maximal value, pi(s) = argmax_a Q(s, a), greedy-value(s) = max_a Q(s, a). | 4 |
| algorithms.proofs.ahof.held-karp | AHoF Held-Karp Algorithm: solve the Travelling Salesman Problem EXACTLY in O(2^n * n^2) -- exponential, but far better than the O(n!) brute force -- by dynamic programming over SUBSETS of visited cities. | 3 |
| algorithms.proofs.ahof.hierarchical-clustering | AHoF Agglomerative Hierarchical Clustering: build a hierarchy of clusters (a dendrogram) bottom-up -- start with each point in its own cluster and repeatedly MERGE THE TWO CLOSEST clusters, under a linkage that defines inter-cluster distance (single / complete / average). | 3 |
| algorithms.proofs.ahof.hmc | AHoF V24 Hamiltonian Monte Carlo -- the leapfrog integrator that simulates Hamiltonian dynamics to make distant, high-acceptance proposals. | 3 |
| algorithms.proofs.ahof.hmm-forward | AHoF HMM Forward Algorithm: compute the TOTAL likelihood of an observation sequence under a Hidden Markov Model by summing over all hidden-state paths -- the sum-product companion to Viterbi's max-product decoding. | 2 |
| algorithms.proofs.ahof.hsvi | AHoF D73 HSVI (Heuristic Search Value Iteration for POMDPs): maintain an upper and a lower bound on the optimal value function and search belief points to tighten them; the algorithm has converged at a belief when the bound gap is within the target precision: converged? | 4 |
| algorithms.proofs.ahof.huffman | AHoF Huffman Coding: build an optimal prefix-free binary code by a greedy bottom-up merge. | 3 |
| algorithms.proofs.ahof.hungarian | AHoF Hungarian Algorithm (Kuhn-Munkres): find a minimum-cost perfect assignment of n agents to n tasks in O(n^3) -- the exact solver for the assignment problem (job scheduling, tracking, matching). | 3 |
| algorithms.proofs.ahof.hypergradient-hg | AHoF O25 Hypergradient Descent: adapt the learning rate online by a hypergradient correction, updating rate-update rate adjustment = rate + adjustment. | 3 |
| algorithms.proofs.ahof.hypothesis-test | AHoF Statistical Hypothesis Testing (z-test / critical-value decision): decide whether observed data are inconsistent with a null hypothesis at a chosen significance level. | 3 |
| algorithms.proofs.ahof.imitation-irl | Kochenderfer imitation-learning / inverse-RL / structure-learning cores as higher-order-function compositions, proved axiom-free, extending the 222 AHoF catalog: D18.3 SMILe : stochastic mixture of expert-imitating policies (convex blend) D18.5 max-margin IRL : reward makes the expert beat alternatives by a margin (sound) D18.6 max-entropy IRL : trajectory probability = exp-weight / partition (nor | 4 |
| algorithms.proofs.ahof.importance-sampling | AHoF D7 worked likelihood-weighted (importance) sampling over exact rationals. | 4 |
| algorithms.proofs.ahof.interval-arithmetic | AHoF V40 worked interval arithmetic over exact rationals on the interval [1/2, 3/2]. | 6 |
| algorithms.proofs.ahof.is-falsification | AHoF V27 Importance Sampling: estimate the probability of a rare failure event by sampling from a proposal distribution and reweighting by the importance weight, the ratio of the target density to the proposal density: importance-weight target proposal = target / proposal. | 3 |
| algorithms.proofs.ahof.isotropic-es | AHoF D44 Isotropic Evolutionary Strategies: perturb with isotropic Gaussian noise and keep the fitter offspring; between two fitnesses it keeps the larger value: prefers-fitter? | 3 |
| algorithms.proofs.ahof.ista | AHoF O-family ISTA (Iterative Shrinkage-Thresholding / proximal gradient): the standard first-order method for L1-regularized (LASSO) problems. | 3 |
| algorithms.proofs.ahof.jaccard-similarity | AHoF Jaccard Similarity: measure how alike two SETS are by the size of their intersection over the size of their union, jaccard intersection-size union-size = |A intersect B| / |A union B|, a value in [0, 1] that is 1 for identical sets and 0 for disjoint ones. | 2 |
| algorithms.proofs.ahof.johnson | AHoF Johnson's Algorithm (all-pairs shortest paths): compute shortest paths between EVERY pair of vertices in a sparse, possibly negative-weight (but cycle-free) graph in O(V*E + V^2 log V) -- faster than Floyd-Warshall on sparse graphs. | 3 |
| algorithms.proofs.ahof.k2 | AHoF D15 K2 Graph Search: greedy Bayesian-network structure learning. | 3 |
| algorithms.proofs.ahof.kadane | AHoF Kadane's Algorithm: find the maximum-sum contiguous subarray in a single O(n) pass. | 3 |
| algorithms.proofs.ahof.kalman | AHoF D-family Kalman Filter: the optimal linear estimator for a Gaussian-linear system, alternating a predict step (propagate mean and variance) and an update step that fuses a noisy measurement. | 3 |
| algorithms.proofs.ahof.karger | AHoF Karger's Min-Cut Algorithm (randomized): estimate the minimum cut of an undirected graph -- the fewest edges whose removal disconnects it -- by repeatedly CONTRACTING a uniformly random edge (merging its endpoints, keeping parallel edges) until two supernodes remain; the edges between them form a cut. | 3 |
| algorithms.proofs.ahof.kde | AHoF D12 Nonparametric Learning (Kernel Density Estimation): estimate a density as a sum of kernels centered at the data points, each with bandwidth h. | 3 |
| algorithms.proofs.ahof.kernel-smoothing | AHoF D26 Kernel Smoothing value-function approximation: approximate the value at a query state by a kernel-weighted average of the stored sample values, with weights given by a similarity kernel. | 3 |
| algorithms.proofs.ahof.kkt | AHoF O53 Lagrange Multipliers (KKT): the stationarity condition of the Karush-Kuhn-Tucker system. | 3 |
| algorithms.proofs.ahof.kmeans | AHoF K-Means Clustering (Lloyd's algorithm): partition points into k clusters by alternating an ASSIGNMENT step (assign each point to the nearest cluster centroid) and an UPDATE step (move each centroid to the mean of its assigned points), until assignments stop changing. | 3 |
| algorithms.proofs.ahof.kmp | AHoF Knuth-Morris-Pratt (KMP) string matching: find all occurrences of a pattern in a text in O(n + m) time -- never re-examining a text character -- by precomputing a FAILURE FUNCTION that says, on a mismatch after matching q characters, how far the pattern can shift without missing a match (reusing the longest proper prefix that is also a suffix). | 3 |
| algorithms.proofs.ahof.knapsack | AHoF 0/1 Knapsack (dynamic programming): choose a subset of items maximizing total value under a weight capacity. | 4 |
| algorithms.proofs.ahof.knn | AHoF K-Nearest Neighbors (instance-based classification): classify a query point by a majority vote among its K nearest training examples -- a non-parametric method with no training phase (lazy learning). | 3 |
| algorithms.proofs.ahof.kosaraju | AHoF Kosaraju's Algorithm: find the strongly connected components (SCCs) of a directed graph in O(V + E) via two depth-first passes -- one on the graph (recording finish order) and one on the TRANSPOSE (grouping by reachability in decreasing finish order). | 3 |
| algorithms.proofs.ahof.kruskal | AHoF Kruskal's Minimum Spanning Tree: build an MST by scanning edges in increasing weight order and adding each edge unless it would form a cycle -- i.e. | 2 |
| algorithms.proofs.ahof.lao-star | AHoF D38 Labeled Heuristic Search (LAO*): expand the best (lowest f-cost) node on the frontier of the explicit AND/OR graph; between two f-costs it keeps the smaller value: prefers-lower-f? | 3 |
| algorithms.proofs.ahof.lbfgs | AHoF O30 L-BFGS: limited-memory BFGS storing recent (s, y) pairs; the stored gradient change is y = g_{k+1} - g_k: gradient-change g-new g-old = g-new - g-old. | 3 |
| algorithms.proofs.ahof.lcs | AHoF Longest Common Subsequence (dynamic programming): the length of the longest subsequence common to two sequences -- the basis of diff, version control merges, and bioinformatics alignment. | 3 |
| algorithms.proofs.ahof.levenberg-marquardt | AHoF O31 worked Levenberg-Marquardt: the general descent skeleton with a damped Hessian-inverse step size, on the quadratic f(x) = x^2. | 3 |
| algorithms.proofs.ahof.linear-interpolation | AHoF D27 Linear Interpolation over exact rationals: interpolate between two values a and b with convex weights w0, w1 (summing to one), lerp a b w0 w1 = w0 * a + w1 * b. | 5 |
| algorithms.proofs.ahof.linear-regression-vf | AHoF D29 Linear Regression Value Function: approximate the value function as a linear combination of state features, V(s) = w . | 2 |
| algorithms.proofs.ahof.lis | AHoF Longest Increasing Subsequence (LIS): find the length of the longest strictly-increasing subsequence of a sequence -- underlying diff/patience sorting, box-stacking, and scheduling. | 3 |
| algorithms.proofs.ahof.local-policy-search | AHoF D40 Local Policy Search: hill climbing in policy-parameter space. | 3 |
| algorithms.proofs.ahof.local-search | AHoF D40 worked bounded local (hill-climbing) policy search. | 5 |
| algorithms.proofs.ahof.log-loss | AHoF Cross-Entropy / Log Loss: the standard loss for probabilistic classification and the maximum-likelihood objective for logistic regression and softmax networks. | 3 |
| algorithms.proofs.ahof.logistic-regression | AHoF Logistic Regression: a probabilistic linear classifier that models the class probability as the logistic sigmoid of a linear score, P(y=1|x) = sigmoid(w.x + b), trained by maximizing the log-likelihood (gradient ascent). | 3 |
| algorithms.proofs.ahof.lp-mdp | AHoF D24 LP Formulation of an MDP: the optimal value function is the solution of a linear program that minimizes the total value subject to the Bellman inequality constraints -- for every state-action pair the value must be at least its one-step backup R + gamma * E[V']: satisfies-bellman? | 4 |
| algorithms.proofs.ahof.lp-reachability | AHoF V39 LP-Based Reachability: compute reachable-set bounds by solving linear programs; a candidate is reachable within a facet when the LP objective value stays within the facet bound: lp-reachable? | 4 |
| algorithms.proofs.ahof.lqr | LQR linear feedback control (Kochenderfer Decision Making D7.11), one of the signed-subtraction cluster deferred in August until the signed layer landed. | 2 |
| algorithms.proofs.ahof.ltl-model-checking | AHoF V7 LTL Model Checking: check a Linear Temporal Logic specification against a system; quantitatively the spec is satisfied when the trace robustness meets the required margin: satisfied? | 4 |
| algorithms.proofs.ahof.manacher | AHoF Manacher's Algorithm: find the longest palindromic substring (and all maximal palindrome radii) in LINEAR time, beating the O(n^2) expand-around-center approach by reusing mirror symmetry so each position is examined O(1) amortized. | 3 |
| algorithms.proofs.ahof.matrix-chain | AHoF Matrix Chain Multiplication (dynamic programming): find the parenthesization of a chain of matrix products that minimizes the number of scalar multiplications. | 3 |
| algorithms.proofs.ahof.maximum-likelihood | AHoF D10 worked maximum likelihood estimation over exact rationals. | 4 |
| algorithms.proofs.ahof.mc-dropout | AHoF V62 MC Dropout Uncertainty: estimate predictive uncertainty from the variance of stochastic-dropout forward passes and flag an input uncertain when that variance reaches the threshold: uncertain? | 4 |
| algorithms.proofs.ahof.mc-mean | AHoF O69 Uncertainty Propagation (Monte Carlo): propagate input uncertainty by sampling and averaging the outputs. | 4 |
| algorithms.proofs.ahof.mcts | AHoF D36 Monte Carlo Tree Search: incrementally grow a search tree by selection, expansion, simulation, and backpropagation. | 4 |
| algorithms.proofs.ahof.mcts-falsification | AHoF V19 MCTS for Falsification: Monte Carlo tree search over the space of system behaviours to find a specification violation, selecting child nodes by their UCB score and keeping the higher-scoring child: prefers-child-zero? | 3 |
| algorithms.proofs.ahof.mean-value-inclusion | AHoF V42 Mean-Value Inclusion: a tighter interval extension than the natural inclusion, using the mean-value form to enclose a function's range in [lo, hi]; a value is certified within the enclosure when it lies between the bounds: encloses? | 3 |
| algorithms.proofs.ahof.merge-sort | AHoF Merge Sort: a stable, worst-case O(n log n) comparison sort by divide-and-conquer -- split the list in half, recursively sort each half, then MERGE the two sorted halves. | 3 |
| algorithms.proofs.ahof.mesh-adaptive | AHoF O39 Mesh Adaptive Direct Search (MADS): a derivative-free direct-search method that probes the objective at mesh points around the incumbent. | 3 |
| algorithms.proofs.ahof.min-max-scaling | AHoF Min-Max Scaling (normalization): rescale a feature linearly to the unit interval [0, 1] by mapping the minimum to 0 and the maximum to 1, scaled offset range = (x - min) / (max - min), where offset = x - min and range = max - min. | 2 |
| algorithms.proofs.ahof.mle-system | AHoF V1 MLE for System Models: fit a system model by maximum likelihood, keeping the model with the larger data likelihood: prefers-model-zero? | 3 |
| algorithms.proofs.ahof.momentum | AHoF O19 worked Polyak momentum over signed rationals with pair state. | 4 |
| algorithms.proofs.ahof.monte-carlo | AHoF V26 worked direct Monte Carlo failure-probability estimation. | 3 |
| algorithms.proofs.ahof.mse | AHoF Mean Squared Error: the standard loss for regression and the objective of least-squares fitting -- the average of the squared prediction errors, squared-error e = e * e mse e0 e1 = (e0*e0 + e1*e1) / 2 (a two-sample average). | 3 |
| algorithms.proofs.ahof.multilevel-splitting | AHoF V32 Multilevel Splitting: estimate rare-event probability by splitting particles that cross intermediate levels toward the rare set; a particle reaches a level when its score meets that level: reaches-level? | 4 |
| algorithms.proofs.ahof.multiobjective | Kochenderfer 'Algorithms for Optimization' Ch.15-16 multiobjective / sampling-plan selection rules as higher-order-function compositions, proved axiom-free, extending the 222 AHoF catalog: O15.3 non-dominated sorting : a Pareto-dominates b iff a1>=b1 AND a2>=b2 O15.4 VEGA : per-objective subpopulation selection = max fitness O16.8 greedy subset select : pick the point of minimum distance metric O1 | 7 |
| algorithms.proofs.ahof.mutation-testing | AHoF V-family Mutation Testing: assess a test suite's fault-detection power by seeding many small program mutants and measuring how many the suite KILLS (detects). | 4 |
| algorithms.proofs.ahof.n-queens | AHoF N-Queens (backtracking constraint satisfaction): place N queens on an NxN board so none attacks another -- the textbook example of backtracking search, which extends a partial placement column by column and abandons (backtracks) any branch that violates a constraint. | 3 |
| algorithms.proofs.ahof.naive-bayes | AHoF D-family Naive Bayes classifier: predict a class from features assumed conditionally independent given the class. | 4 |
| algorithms.proofs.ahof.nash-equilibrium | AHoF D77 Nash Equilibrium (support enumeration): a strategy profile is a Nash equilibrium when no player can gain by unilaterally deviating. | 3 |
| algorithms.proofs.ahof.nash-q-learning | AHoF D81 Nash Q-Learning (classical: learn stage-game Q-values and back up the Nash EQUILIBRIUM value of each stage game, Hu-Wellman 2003). | 3 |
| algorithms.proofs.ahof.natural-gradient | AHoF D50 Natural Gradient: the policy update that ascends along the natural gradient -- the ordinary gradient preconditioned by the inverse Fisher information matrix, so the step is invariant to the parameterization of the policy. | 3 |
| algorithms.proofs.ahof.natural-gradient-ng | AHoF D50 Natural Gradient: precondition the gradient by the inverse Fisher metric and step; the parameter update descends update theta step = theta - step. | 3 |
| algorithms.proofs.ahof.natural-inclusion | AHoF V41 Natural Inclusion Function: replace each variable in an expression by its interval and evaluate with interval arithmetic to get a guaranteed enclosure [lo, hi] of the range; the true range is contained, so a candidate value is certified within the enclosure exactly when it lies between the bounds: encloses? | 3 |
| algorithms.proofs.ahof.nearest-neighbor | AHoF D25 worked nearest-neighbor value function approximation over exact rationals. | 3 |
| algorithms.proofs.ahof.nesterov | AHoF O20 worked Nesterov accelerated momentum over signed rationals. | 4 |
| algorithms.proofs.ahof.network-scoring | AHoF D14 worked additive Bayesian-network scoring. | 2 |
| algorithms.proofs.ahof.neural-vf | AHoF D30 Neural Network Value Function: approximate the value function with a trainable neural network. | 3 |
| algorithms.proofs.ahof.newton | AHoF O26 worked Newton's method: the general descent skeleton with a Hessian-inverse step size, on the quadratic f(x) = x^2. | 3 |
| algorithms.proofs.ahof.nn-verification | AHoF V47 Neural Network Verification: certify that a network's output stays within a safety bound over an input region; a concrete output is safe when it is within the safety bound: safe? | 4 |
| algorithms.proofs.ahof.nnls | Nonnegative projection for NNLS (Kochenderfer Optimization O13.4), a signed-cluster algorithm deferred in August: over nonnegative rationals the projection is degenerate, so it needed the signed layer's max(x,0). | 4 |
| algorithms.proofs.ahof.o72-branch-and-bound | AHoF O72 Branch and Bound (optimization form) worked pruning step over exact rationals, reusing the shared bounding lemma (rainbow.algorithms.proofs.branch-and-bound). | 4 |
| algorithms.proofs.ahof.odd-monitor | AHoF V59 worked ODD monitor over the 2-D operating envelope [0,1] x [0,2]. | 4 |
| algorithms.proofs.ahof.ols-regression | AHoF Ordinary Least Squares (simple linear regression): fit a line y = slope*x + intercept minimizing the sum of squared residuals. | 2 |
| algorithms.proofs.ahof.open-loop-planning | AHoF D39 Open-Loop Planning: optimize a fixed open-loop action sequence, keeping the plan with the larger total value; it keeps the larger value: prefers-plan-zero? | 3 |
| algorithms.proofs.ahof.opt-reachability | AHoF V45 Optimization-Based Reach: bound the reachable set by solving an optimization in each direction; a direction's reach is certified when the optimal reach value stays within the bound: reach-bounded? | 4 |
| algorithms.proofs.ahof.order-reduction | AHoF V38 Order Reduction: reduce the generator/complexity order of a set representation while over-approximating; the reduction is sound when the incurred over-approximation error stays within the tolerance: reduction-sound? | 4 |
| algorithms.proofs.ahof.pagerank | AHoF PageRank: rank the nodes of a directed graph by importance -- the stationary distribution of a random surfer who follows out-links with probability d (the damping factor) and teleports to a uniformly random node with probability 1-d. | 2 |
| algorithms.proofs.ahof.pareto | AHoF multiobjective optimization -- Pareto dominance, the partial order that defines the Pareto front. | 4 |
| algorithms.proofs.ahof.particle-filter | AHoF D10 Particle Filter (sequential Monte Carlo): approximate a filtering distribution by a weighted set of particles, propagated and reweighted each step, then RESAMPLED to combat weight degeneracy. | 3 |
| algorithms.proofs.ahof.particle-filter-pf | AHoF D70 Particle Filter: approximate the posterior by a weighted particle set; the state estimate is the weighted mean estimate w0 x0 w1 x1 = w0*x0 + w1*x1. | 4 |
| algorithms.proofs.ahof.partitioning | AHoF V46 Partitioning: recursively split the state/input set into cells so each is small enough for an accurate local over-approximation; a cell is fine enough when its diameter is within the tolerance: fine-enough? | 4 |
| algorithms.proofs.ahof.pattern-search | AHoF O35 worked generalized pattern search over exact rationals, minimizing f(x) = x^2 from x = 2 with step 1. | 3 |
| algorithms.proofs.ahof.pbvi | AHoF D72 PBVI (Point-Based Value Iteration for POMDPs): maintain value at a finite set of belief points, backing up each point's value as the maximum over candidate alpha vectors of the value at that belief. | 3 |
| algorithms.proofs.ahof.pc | AHoF D16 PC Algorithm: constraint-based Bayesian-network structure learning. | 3 |
| algorithms.proofs.ahof.penalty | AHoF O-family Penalty Method: solve a constrained optimization problem by a sequence of UNCONSTRAINED problems whose objective adds a penalty proportional to the constraint violation, penalized f mu violation = f + mu * violation where mu is the penalty coefficient (increased across outer iterations). | 2 |
| algorithms.proofs.ahof.perceptron | AHoF Perceptron (Rosenblatt): the foundational linear classifier and the atom of neural networks. | 3 |
| algorithms.proofs.ahof.policy-evaluation | AHoF D20 specialization of bounded exact-rational policy evaluation. | 5 |
| algorithms.proofs.ahof.policy-evaluation-backup | AHoF D-family Policy Evaluation: the evaluation half of policy iteration. | 2 |
| algorithms.proofs.ahof.policy-gradient | AHoF D49 Gradient Ascent Update (policy gradient): the parameter update at the heart of policy-gradient reinforcement learning. | 3 |
| algorithms.proofs.ahof.policy-iteration | AHoF D21 worked bounded policy-iteration step. | 4 |
| algorithms.proofs.ahof.policy-visualization | AHoF V53 Policy Visualization: render a learned policy by displaying, at each state, the greedy action -- the one with the maximal action value. | 3 |
| algorithms.proofs.ahof.polytope | AHoF V34 Polytope Propagation: represent a reachable set as an intersection of halfspaces (a polytope) and propagate it forward. | 3 |
| algorithms.proofs.ahof.pomcp | AHoF D75 Online POMDP (POMCP): Monte Carlo tree search in belief space, selecting actions at each node by their UCB score and keeping the higher-scoring action. | 3 |
| algorithms.proofs.ahof.pomdp-bounds | Kochenderfer 'Algorithms for Decision Making' Ch.21 offline POMDP value-function bounds, expressed as higher-order-function compositions over belief-weighted alpha-vector values and proved axiom-free, extending the 222 AHoF catalog: D21.2 QMDP : value = max_a sum_s b(s) Q(s,a) (upper bound) D21.3 fast informed bnd : max over observation-corrected action alpha-values D21.5 blind lower bound : value | 5 |
| algorithms.proofs.ahof.pomdp-online | Kochenderfer 'Algorithms for Decision Making' Ch.21-23 online / point-based / controller POMDP cores as higher-order-function compositions, proved axiom-free (each with its most distinctive structural property), extending the 222 AHoF catalog: D21.8 Perseus (randomized PBVI) : backup keeps the better alpha -> value never decreases D22.3 DESPOT (anytime search) : maintains a lower<=upper value brac | 4 |
| algorithms.proofs.ahof.ppo | AHoF D43 Proximal Policy Optimization: a policy-gradient method that keeps updates in a trust region by CLIPPING the probability ratio r = pi_new/pi_old into [1 - eps, 1 + eps] before forming the surrogate objective. | 3 |
| algorithms.proofs.ahof.precision-recall | AHoF Precision and Recall: the two complementary quality metrics of a binary classifier, computed from the confusion-matrix counts (true/false positives and negatives), precision tp fp = tp / (tp + fp) (of predicted positives, how many are right) recall tp fn = tp / (tp + fn) (of actual positives, how many are found). | 3 |
| algorithms.proofs.ahof.prim | AHoF Prim's Minimum Spanning Tree: grow an MST from a start vertex by repeatedly adding the minimum-weight edge that CROSSES THE CUT between the in-tree vertices and the rest. | 3 |
| algorithms.proofs.ahof.prob-programming | AHoF V25 Probabilistic Programming: an observe/factor statement reweights the trace by the observation likelihood; the trace score combines two factors multiplicatively score a b = a * b. | 4 |
| algorithms.proofs.ahof.prob-robust | AHoF O75 Probabilistic Robust Optimization: satisfy constraints with high probability under uncertainty; a design is chance-feasible when its violation probability is within the risk level alpha: chance-feasible? | 4 |
| algorithms.proofs.ahof.probabilistic-reachability | AHoF V51 Probabilistic Reachability: compute the probability of reaching a target set and flag it likely-reachable when that probability meets a confidence threshold: likely-reachable? | 4 |
| algorithms.proofs.ahof.projection-methods | Kochenderfer constrained/rounded update rules as higher-order-function compositions, proved axiom-free, extending the 222 AHoF catalog: O10.1 projected gradient descent : project the updated point onto a box [lo,hi] D12.3 restricted policy gradient : clip the update to a trust region [lo,hi] O22.2 LP-relaxation-and-round : round a fractional LP value by a 1/2 threshold Both projection/clipping rul | 6 |
| algorithms.proofs.ahof.q-learning | AHoF D61 worked temporal-difference (Q-learning) update over signed rationals. | 3 |
| algorithms.proofs.ahof.qmdp | AHoF D22 QMDP (POMDP planning approximation): approximate the value of an action under partial observability by weighting the fully-observable Q-values by the current belief over states, qmdp-value b0 q0 b1 q1 = b0 * Q(s0, a) + b1 * Q(s1, a) (a two-state belief; the general form sums over all states). | 2 |
| algorithms.proofs.ahof.qp | AHoF O56 Quadratic Programming: minimize a convex quadratic objective subject to linear constraints, typically by encoding the KKT stationarity system. | 3 |
| algorithms.proofs.ahof.quadratic-fit | AHoF O10 Quadratic Fit Search: fit a parabola through three sampled points and step toward its vertex, keeping the three lowest-valued points as the bracket shrinks. | 3 |
| algorithms.proofs.ahof.quickselect | AHoF Quickselect (Hoare's selection): find the k-th smallest element of an unsorted array in expected O(n) -- faster than sorting -- by partitioning around a pivot (as in quicksort) but recursing into ONLY the side that contains the target rank. | 3 |
| algorithms.proofs.ahof.quicksort | AHoF Quicksort: an in-place, average-case O(n log n) comparison sort by divide-and-conquer -- pick a pivot, PARTITION the remaining elements into those at most the pivot and those greater, then recursively sort each side. | 3 |
| algorithms.proofs.ahof.r-squared | AHoF R-squared (coefficient of determination): summarize how well a regression fits by the FRACTION of the total variance in the target that the model explains, r-squared explained-variance total-variance = explained-variance / total-variance = SS_regression / SS_total = 1 - SS_residual / SS_total. | 2 |
| algorithms.proofs.ahof.rabin-karp | AHoF Rabin-Karp string matching: find a pattern in a text in expected O(n+m) by comparing a ROLLING HASH of each text window against the pattern's hash -- updating the window hash in O(1) as it slides (remove the leaving character, add the entering one). | 3 |
| algorithms.proofs.ahof.radix-sort | AHoF Radix Sort (LSD): sort fixed-width integer keys in O(n * d) without comparing whole keys -- process the digits from LEAST to most significant, and on each pass STABLY sort by that digit only. | 3 |
| algorithms.proofs.ahof.ratio-normalizing | AHoF V31 Ratio of Normalizing Constants: estimate the ratio of two normalizing constants (partition functions) Z1/Z2, the quantity underlying Bayes factors and bridge/path sampling: ratio z1 z2 = z1 / z2. | 3 |
| algorithms.proofs.ahof.rbf-surrogate | AHoF O61 Radial Basis Function surrogate: an interpolating surrogate model that predicts by a weighted sum of radial basis functions centered at the sampled points. | 3 |
| algorithms.proofs.ahof.reachability-eda | Final Kochenderfer straggler cores (reachability, robustness envelope, adaptive SA, estimation-of-distribution program search) as higher-order-function compositions, proved axiom-free, extending the 222 AHoF catalog: V10.3 backward reachability : a state is back-reachable if SOME successor is (OR) V9.3 conservative linearization : reachable-set upper envelope = center + radius O8.7 adaptive simula | 6 |
| algorithms.proofs.ahof.reachability-spec | AHoF V8 Reachability Specification: a reachability property asks whether the system can reach a target set; concretely a trajectory reaches the target when its distance to the target set falls within the specification tolerance: reaches-target? | 4 |
| algorithms.proofs.ahof.receding-horizon | AHoF D31 Receding Horizon Control (model-predictive control): rather than commit to a whole open-loop plan, the controller solves the finite-horizon problem, applies only the FIRST action of the resulting plan, then re-solves from the new state at the next step. | 3 |
| algorithms.proofs.ahof.regression-gradient | AHoF O6 Regression Gradient: the least-squares gradient is driven by the residual actual - predicted, which the gradient sums over data: residual actual predicted = actual - predicted. | 3 |
| algorithms.proofs.ahof.reinforce | AHoF D46 REINFORCE (likelihood-ratio policy gradient): the Monte-Carlo policy gradient estimator weights each sampled trajectory's score-function by its return. | 3 |
| algorithms.proofs.ahof.rejection | AHoF D6 Rejection Sampling: draw a proposal and a uniform u, accepting the proposal when u falls under the acceptance ratio f(x)/(M g(x)): accepts? | 4 |
| algorithms.proofs.ahof.rejection-sampling | AHoF V21 Rejection Sampling (for failure events): draw samples and keep only those consistent with the evidence / that hit the target event, rejecting the rest. | 3 |
| algorithms.proofs.ahof.reliability | AHoF V-family Series-System Reliability (reliability block diagram): a series system works only if EVERY component works, so with independent components its reliability is the product of the component reliabilities, series-reliability [r0, r1, ...] = r0 * r1 * ... | 4 |
| algorithms.proofs.ahof.reservoir-sampling | AHoF Reservoir Sampling (Algorithm R): draw a uniform random sample of fixed size k from a STREAM of unknown, possibly huge length in a SINGLE PASS and O(k) memory -- used for log sampling, streaming analytics, and dataset subsampling. | 3 |
| algorithms.proofs.ahof.reverse-mode-ad | AHoF O5 Reverse-Mode Auto-Diff: backpropagate adjoints, accumulating each node's adjoint as the sum of its downstream contributions: adjoint-accumulate a b = a + b. | 3 |
| algorithms.proofs.ahof.rl-falsification | AHoF V20 RL for Falsification: train an agent by reinforcement learning to drive the system toward a specification violation, acting greedily on the learned Q-values by keeping the higher-Q action: prefers-action-zero? | 3 |
| algorithms.proofs.ahof.robust-optimization | AHoF O74 Robust Optimization (set-based): optimize against the WORST case over an uncertainty set. | 3 |
| algorithms.proofs.ahof.robustness-objective | AHoF V13 worked robustness-based falsification objective over signed rationals. | 3 |
| algorithms.proofs.ahof.rod-cutting | AHoF Rod Cutting (dynamic programming): given a rod of integer length and a price for each possible piece length, cut it into pieces maximizing total revenue. | 4 |
| algorithms.proofs.ahof.rollout | AHoF D32 Rollout with Heuristic: estimate a state's value by simulating the rollout policy forward and averaging the returns. | 3 |
| algorithms.proofs.ahof.roulette-selection | AHoF genetic-algorithm operator: fitness-proportionate (roulette-wheel) selection. | 3 |
| algorithms.proofs.ahof.sac | AHoF D45 Soft Actor-Critic: an off-policy actor-critic that optimizes a MAXIMUM-ENTROPY objective, augmenting the reward with an entropy bonus so the policy stays as stochastic as possible while succeeding -- improving exploration and robustness. | 2 |
| algorithms.proofs.ahof.sarsa | AHoF D62 worked SARSA on-policy update over signed rationals. | 3 |
| algorithms.proofs.ahof.sarsop | AHoF D74 SARSOP (Successive Approximations of the Reachable Space under Optimal Policies): a point-based POMDP solver that samples beliefs reachable under the optimal policy and tightens value bounds; it has converged when the bound gap is within the target precision: converged? | 4 |
| algorithms.proofs.ahof.sat | AHoF V50 SAT-based Bounded Model Checking: the system is unrolled k steps and encoded as a boolean formula in CNF; a counterexample exists iff the formula is satisfiable. | 4 |
| algorithms.proofs.ahof.secant | AHoF O27 Secant Method: root-find by the secant update x - f(x)*(x-x_prev)/(f-f_prev); the divided-difference denominator is the value change value-change f-new f-old = f-new - f-old. | 3 |
| algorithms.proofs.ahof.segment-tree | AHoF Segment Tree: answer range-aggregate queries (sum / min / max) AND point updates on an array, both in O(log n), by a balanced binary tree over array segments in which every internal node stores the aggregate of its two children. | 2 |
| algorithms.proofs.ahof.sequential-decision | Kochenderfer 'Algorithms for Decision Making' game-theory + model-based-RL cores as higher-order-function compositions, proved axiom-free, extending the 222 AHoF catalog: D24.8 iterated best response : best-response value = max over own actions (dominates) D16.7 R-MAX : optimistic value = max(realistic, Vmax); optimism bound D16.5 prioritized sweeping : sweep the state of maximum Bellman-residual | 5 |
| algorithms.proofs.ahof.set-cover | AHoF Set Cover (greedy approximation): given a universe of elements and a collection of subsets, choose the fewest subsets whose union is the whole universe. | 3 |
| algorithms.proofs.ahof.shap | AHoF V55 SHAP Values: attribute a prediction to features as a weighted sum of feature contributions (Shapley-weighted); attribution w0 c0 w1 c1 = w0*c0 + w1*c1. | 4 |
| algorithms.proofs.ahof.shooting | AHoF V16 Shooting Methods: trajectory-based trajectory optimization / open-loop control. | 3 |
| algorithms.proofs.ahof.shubert | AHoF O11 Shubert-Piyavskii: build a piecewise-linear (sawtooth) lower bound of a Lipschitz objective and sample where the lower bound is smallest; between two candidate lower- bound values it keeps the smaller value: prefers-lower? | 3 |
| algorithms.proofs.ahof.simplex | AHoF O54 Simplex Algorithm -- the minimum-ratio test that chooses the leaving variable (pivot row) each iteration. | 3 |
| algorithms.proofs.ahof.simplex-interpolation | AHoF D28 Simplex Interpolation: interpolate a value function over a simplicial grid using barycentric coordinates. | 3 |
| algorithms.proofs.ahof.simulated-annealing | AHoF Simulated Annealing: a global optimization metaheuristic that escapes local optima by sometimes accepting WORSE solutions -- with a probability that shrinks as a 'temperature' cools -- inspired by the annealing of metals. | 3 |
| algorithms.proofs.ahof.sliding-window | AHoF Sliding Window: solve subarray/substring problems in one O(n) pass by maintaining a window that slides across the data, adding the entering element and removing the leaving one instead of recomputing over each subarray. | 3 |
| algorithms.proofs.ahof.smc | AHoF V30 Sequential Monte Carlo: propagate and resample a weighted particle set over time; the filtered estimate is the normalized weighted mean of the particles, estimate w0 x0 w1 x1 = w0*x0 + w1*x1. | 4 |
| algorithms.proofs.ahof.sobol | AHoF O60 Sobol Sequences: a quasi-random low-discrepancy sequence for uniform space-filling sampling; the sequence meets its uniformity target when the star discrepancy stays within the bound: low-discrepancy? | 4 |
| algorithms.proofs.ahof.softmax | AHoF Softmax: turn a vector of real-valued scores (logits) into a probability distribution over classes -- the standard output layer of multi-class classifiers and the policy head of policy-gradient RL. | 2 |
| algorithms.proofs.ahof.spsa | AHoF O7 SPSA (Simultaneous Perturbation Stochastic Approximation): estimate the gradient from the two-sided perturbation difference (f(x+cD) - f(x-cD))/(2cD); with 2cD=1 the numerator is perturbation-difference f-plus f-minus = f-plus - f-minus. | 3 |
| algorithms.proofs.ahof.state-abstraction | AHoF V52 Discrete State Abstraction (classical: map concrete states to abstract cells of a partition). | 4 |
| algorithms.proofs.ahof.stieltjes | Stieltjes three-term recurrence for orthogonal polynomials (Kochenderfer Optimization O21.3), a signed-cluster algorithm deferred in August until the signed layer landed. | 2 |
| algorithms.proofs.ahof.stl-monitor | AHoF V63 Runtime STL Monitor: online monitoring of a Signal Temporal Logic specification. | 4 |
| algorithms.proofs.ahof.stl-robustness | AHoF V6 worked signal-temporal-logic robustness over signed rationals. | 3 |
| algorithms.proofs.ahof.strong-wolfe | AHoF O15 Strong Wolfe Line Search: accept a step only when it satisfies both the Armijo sufficient-decrease condition and the curvature condition: wolfe-ok? | 3 |
| algorithms.proofs.ahof.subset-sum | AHoF Subset Sum (dynamic programming): decide whether some subset of a set of positive integers sums to a target -- the canonical (weakly) NP-complete decision problem and the kernel of the partition problem and 0/1-knapsack feasibility. | 3 |
| algorithms.proofs.ahof.support-function | AHoF V37 Support Function Method: represent a convex reachable set by its support function; a halfspace in a direction is respected when the set's support value in that direction is within the halfspace bound: within-support? | 4 |
| algorithms.proofs.ahof.surrogate-explanation | AHoF V56 Surrogate Model Explanation: fit an interpretable surrogate to a black-box model and explain via the surrogate; the explanation is faithful when the surrogate's local fidelity error is within the tolerance: faithful? | 4 |
| algorithms.proofs.ahof.svm | AHoF Support Vector Machine (linear, hard-margin classification): find the hyperplane that separates two classes with the MAXIMUM margin, then classify a point by which side it falls on. | 3 |
| algorithms.proofs.ahof.symbolic-reachability | AHoF V49 Symbolic Reachability (BDDs): represent reachable state sets symbolically (e.g. | 4 |
| algorithms.proofs.ahof.tabu-search | AHoF Tabu Search: a local-search metaheuristic that escapes local optima by ALWAYS moving to the best neighbor -- even a worsening one -- while a short-term memory (the TABU LIST) forbids reversing recent moves, preventing cycling. | 2 |
| algorithms.proofs.ahof.taylor-model | AHoF V43 Taylor Model Propagation: represent a function by a polynomial plus a guaranteed remainder interval and propagate it; the model is valid when the remainder magnitude stays within the bound: remainder-bounded? | 4 |
| algorithms.proofs.ahof.thompson | AHoF Thompson Sampling (posterior sampling) for multi-armed bandits: instead of an explicit exploration bonus, draw one sample from each arm's posterior over its mean reward and pull the arm with the largest sample. | 3 |
| algorithms.proofs.ahof.topological-sort | AHoF Topological Sort (Kahn's algorithm): order the vertices of a DAG so every edge points forward -- the canonical dependency/scheduling order. | 3 |
| algorithms.proofs.ahof.tree-search-fal | AHoF V17 Tree Search for Falsification: best-first search over behaviours toward a violation, expanding the node with the lowest cost-to-violation; it keeps the smaller value: prefers-lower-cost? | 3 |
| algorithms.proofs.ahof.trie | AHoF Trie (prefix tree): store a set of strings in a tree keyed by characters, so that insertion and lookup are O(length) regardless of how many words are stored, and every shared prefix is stored once -- the workhorse behind autocomplete, spell-check, IP routing, and dictionary compression. | 3 |
| algorithms.proofs.ahof.trpo | AHoF D51 Trust-Region Policy Optimization: improve a policy by maximizing a surrogate advantage objective subject to a trust-region constraint that the new policy stays close to the old one in KL divergence. | 3 |
| algorithms.proofs.ahof.trust-region | AHoF O16 worked trust region step acceptance over exact rationals. | 5 |
| algorithms.proofs.ahof.tsp-nearest-neighbor | AHoF Nearest-Neighbor TSP heuristic: build a tour of the Travelling Salesman Problem by starting at a city and repeatedly travelling to the NEAREST unvisited city, returning to the start at the end. | 3 |
| algorithms.proofs.ahof.two-pointers | AHoF Two Pointers: solve many array/string problems in a single O(n) pass by maintaining two indices that move toward each other (or in tandem) instead of nesting loops. | 3 |
| algorithms.proofs.ahof.ucb | AHoF O64 Upper Confidence Bound acquisition (Bayesian optimization / bandits): select the next query by optimistically combining the surrogate's predicted mean with an exploration bonus proportional to the predictive uncertainty: ucb mean weight uncertainty = mean + weight * uncertainty over exact nonnegative rationals. | 4 |
| algorithms.proofs.ahof.ucb1 | AHoF D57 UCB1 (bandit arm selection): pull the arm with the largest upper- confidence-bound score UCB_i = mean_i + sqrt(2 ln t / n_i). | 3 |
| algorithms.proofs.ahof.ukf | AHoF D69 Unscented Kalman Filter: propagate a small set of deterministically chosen sigma points through the nonlinear model and recover the posterior mean as their weighted average. | 4 |
| algorithms.proofs.ahof.union-by-rank | AHoF Union by Rank: the balancing optimization that keeps a Union-Find (disjoint set) forest shallow, so find/union run in near-constant amortized time (inverse Ackermann, with path compression). | 3 |
| algorithms.proofs.ahof.union-find | AHoF Union-Find (Disjoint-Set) connectivity: maintain a partition of elements into disjoint sets under union operations, answering connectivity queries by comparing set representatives. | 3 |
| algorithms.proofs.ahof.value-iteration | AHoF D22 worked finite exact-rational value-iteration instance. | 7 |
| algorithms.proofs.ahof.value-of-information | AHoF D19 worked value of information over signed rationals. | 4 |
| algorithms.proofs.ahof.variable-elimination | AHoF D3 Variable Elimination: exact inference by successively eliminating (marginalizing out) variables from the factor graph. | 3 |
| algorithms.proofs.ahof.viterbi | AHoF Viterbi Algorithm: find the single most-likely hidden-state sequence of a Hidden Markov Model given observations -- the standard decoder for HMMs (speech recognition, POS tagging, gene finding). | 3 |
| algorithms.proofs.ahof.weighted-estimators | Kochenderfer weighted-sum / additive estimators (across Optimization and Validation) as higher-order-function compositions, proved axiom-free, extending the 222 AHoF catalog: V7.4 multiple importance sampling : balance-weighted combination of proposals V11.3 integrated gradients : path-sum attribution (completeness: sum = delta) O6.4 Gauss-Newton Hessian : sum of squared Jacobian terms O17.6 ridge | 5 |
| algorithms.proofs.ahof.weighted-interval | AHoF Weighted Interval Scheduling (dynamic programming): given intervals with weights (values), select a mutually-compatible subset of MAXIMUM total weight. | 4 |
| algorithms.proofs.ahof.weighted-sum | AHoF O66 Weighted Sum Method (multi-objective scalarization): collapse several objectives into one scalar by a weighted sum, then optimize the scalar: scalarize w1 f1 w2 f2 = w1 * f1 + w2 * f2. | 4 |
| algorithms.proofs.ahof.word-break | AHoF Word Break (dynamic programming): decide whether a string can be segmented into a sequence of dictionary words -- the core of tokenizers, CJK word segmentation, and URL/identifier splitting. | 3 |
| algorithms.proofs.ahof.z-score | AHoF Z-Score Standardization: rescale a feature to zero mean and unit standard deviation, z = (x - mean) / std-dev -- the standard preprocessing step that puts features on a comparable scale (essential for distance-based methods, gradient descent conditioning, and regularization) and expresses each value as a number of standard deviations from the mean. | 2 |
| algorithms.proofs.ahof.zonotope | AHoF V35 Zonotope Propagation: represent a reachable set as a zonotope (center plus generator vectors) and propagate it; a point lies in the zonotope when each generator coordinate stays within its unit bound: in-zonotope? | 4 |