Topic domain
Computation Theory
Models of computation and the limits they impose.
- Articles
- 80
- Clusters
- 8
- Foundational
- 24
- Intermediate
- 32
- Advanced
- 24
Automata
10Finite machines, regular languages, and state minimization.
- How a DFA Decides Membership: Transition Tables and the Extended Transition Function
- Simulating an NFA Without Determinizing It: State Sets, Epsilon Closure, and Bitsets
- Thompson Construction: Turning a Regular Expression into an Epsilon NFA
- Where the 2^n Comes From: Subset Construction and the Limits of Determinization
- Partition Refinement: Minimizing a DFA by Splitting Blocks
- Distinguishing Strings and the Myhill-Nerode Theorem
Grammars, derivations, and the Chomsky hierarchy.
- Alphabets, Strings, and the Closure Properties That Define a Language Class
- Derivations, Sentential Forms, and What a Parse Tree Actually Records
- Right-Linear Grammars and the Limits of One-Way Derivation
- The Chomsky Hierarchy as a Ladder of Memory
- Chomsky Normal Form and the CYK Table
- Closure Gaps in Context-Free Languages
Decidability
10Turing machines, reductions, and undecidable problems.
- Encoding Turing Machines and the Undecidability of Acceptance
- Recognizers, Dovetailing, and Complement Asymmetry
- Mapping Reductions and the Halting Problem
- Rice’s Theorem and the Collapse of Semantic Properties
- Presburger Arithmetic and the Decidable Side of Number Theory
- Trakhtenbrot’s Theorem and the Finite Model Boundary
P, NP, and the landscape of hardness.
- Polynomial Time and the Machine-Independence of P
- Certificates and the Two Definitions of NP
- Many-One Reductions and What Completeness Requires
- The Cook–Levin Tableau: Encoding a Computation as a Formula
- Why Three Literals Is the Pivot for Satisfiability
- Configuration Graphs and Savitch's Reachability Argument
Boolean circuits, lower bounds, and depth.
- Circuit Families and the Non-Uniform Model of Computation
- Gate Basis, Fan-In, and What Circuit Size Actually Counts
- The Counting Argument for Circuit Size Lower Bounds
- Formula Size and the Tree-Shaped Restriction on Circuits
- The Switching Lemma and Why Parity Needs Depth to Compute
- The Depth Hierarchy: NC, AC, and the Cost of Wide Gates
Entropy, coding, and channel capacity.
- Shannon Entropy as the Expected Cost of an Outcome
- Mutual Information and the Capacity of a Noisy Channel
- Prefix Codes, the Kraft Inequality, and Why Huffman Is Optimal
- Arithmetic Coding by Interval Subdivision
- LZ77, LZ78, and the Shift from Symbols to Substrings
- Entropy Rate of a Markov Source and the Value of Context
Substitution, reduction, and encodings.
- Alpha-Equivalence and de Bruijn Indices in the Lambda Calculus
- Capture-Avoiding Substitution and the Substitution Lemma
- Beta Reduction and the Consequences of Evaluation Order
- Confluence and the Church-Rosser Theorem for Beta Reduction
- Church Encodings and the Cost of Representing Data as Functions
- Fixed-Point Combinators and How Recursion Enters a Nameless Calculus
Curry-Howard, proof assistants, and typed computation.
- Natural Deduction: Why Implication Is Defined by Two Rules
- Proof Terms: Reading a Derivation as a Program
- The Sequent Calculus and Why Its Rules Are Invertible
- Cut Elimination and the Subformula Property
- Dependent Types: Pi and Sigma as Generalised Function and Pair
- Definitional and Propositional Equality
All Computation Theory articles
- Oct 24, 2026 How a DFA Decides Membership: Transition Tables and the Extended Transition Function The five-tuple, the recursive lift of the transition function to whole strings, and the table layouts that make each input symbol cost one dependent load.
- Oct 23, 2026 Testing DFA Equivalence with Union-Find Instead of a Product Table Why two machines accept the same language exactly when no reachable pair is split by acceptance, and how merging pairs in a disjoint-set structure avoids building the product.
- Oct 19, 2026 Ambiguity, Equivalence, and Other Undecidable Grammar Questions Membership in a context-free language is decidable, but asking whether two grammars denote the same language is not, and neither is asking whether one is ambiguous.
- Oct 12, 2026 The Cook–Levin Tableau: Encoding a Computation as a Formula How a nondeterministic polynomial-time computation becomes a boolean formula whose satisfying assignments correspond exactly to accepting runs, and what the encoding costs in variables and clauses.
- Sep 24, 2026 Rate-Distortion Theory and the Shape of Lossy Compression Why lossy coding is governed by a curve rather than a single number, how the Gaussian bound is derived, and why vector quantization beats scalar quantization at the same rate.
- Sep 23, 2026 Elaboration: Filling in What the Program Did Not Say How metavariables, unification, and implicit arguments turn surface syntax into a fully explicit core term, and why the process can fail in ways the source does not explain.
- Sep 5, 2026 The Arithmetical Hierarchy and the Turing Jump How undecidable problems are graded by the number of quantifiers needed to express them, why the halting set generates every level, and what Post’s theorem says about the resulting ladder.
- Aug 29, 2026 Trakhtenbrot’s Theorem and the Finite Model Boundary Why first-order validity over all structures and over finite structures are both undecidable but for opposite reasons, and how a sentence can encode an entire halting computation in one finite domain.
- Aug 16, 2026 Closure Gaps in Context-Free Languages Context-free languages are closed under union and star but not under intersection or complement, and the two failures are the same failure seen from two sides.
- Aug 6, 2026 Abstract Machines: The CEK, the Krivine Machine, and Closure Conversion How an evaluator becomes an explicit state machine with a control string, an environment, and a continuation, and what each of the three registers costs.
- Aug 3, 2026 Definitional and Propositional Equality Why a type checker can only decide equality by computation, what must be proved as a proposition instead, and how equality reflection changes the boundary between the two.
- Aug 2, 2026 Right-Linear Grammars and the Limits of One-Way Derivation Why a grammar whose rules can only consume input left to right generates exactly the regular languages, and what happens to the language when left-linear rules are mixed in.
- Aug 1, 2026 Pumping Lemmas, Marked Positions, and the Limits of Counting Arguments Why the pumping lemma is a necessary condition for regularity and never a sufficient one, and how marking positions in the input strengthens the argument for both regular and context-free languages.
- Jun 27, 2026 Arithmetic Coding by Interval Subdivision How a message becomes a single rational interval, why the decoder needs no codeword boundaries, and what finite-precision renormalization must do to keep the arithmetic exact.
- Jun 25, 2026 The Sequent Calculus and Why Its Rules Are Invertible How Gentzen's sequent presentation differs from natural deduction, why left and right rules can be read backwards for proof search, and what the cut rule adds.
- Jun 22, 2026 Normalisation by Evaluation for Conversion Checking How to decide equality of terms by evaluating them into a semantic domain of closures and neutral values, and why this avoids the quadratic cost of substitution.
- Jun 18, 2026 Simulating an NFA Without Determinizing It: State Sets, Epsilon Closure, and Bitsets How a nondeterministic automaton runs on a single pass by carrying a set of live states, why the closure step dominates the cost, and how bitsets make it cheap.
- Jun 14, 2026 Context-Sensitive Rules and Why Non-Contracting Rewriting Is Decidable A rule may rewrite a symbol in the context of its neighbours as long as it never shortens the string, and that single restriction turns an unbounded search into a finite one.
- Apr 30, 2026 Böhm Trees, Separability, and What Normal Forms Cannot Distinguish Why beta-eta equivalence fails to identify terms that agree on every argument, how Böhm trees record the observable behaviour of a term, and where the separability theorem stops.
- Apr 22, 2026 Alpha-Equivalence and de Bruijn Indices in the Lambda Calculus Why the names of bound variables carry no information, how alpha-equivalence is defined, and how nameless indices turn it into structural equality with a shift operation.
- Mar 30, 2026 Natural Deduction: Why Implication Is Defined by Two Rules How introduction and elimination rules fix the meaning of implication, why the pair must be in harmony, and what a local reduction step removes from a derivation.
- Mar 17, 2026 Kolmogorov Complexity and the Two-Part MDL Code Why the shortest program describing an object is uncomputable yet still useful, how the two-part minimum description length principle turns that idea into a model selection criterion, and where the criterion misleads.
- Mar 12, 2026 Rice’s Theorem and the Collapse of Semantic Properties Why every nontrivial property of the language a program computes is undecidable, how the proof smuggles a halting question into an arbitrary property, and which program properties escape the theorem.
- Mar 9, 2026 Counting Derivations: Algebraic Generating Functions and the Growth of Parse Trees A grammar can be compiled into a polynomial system whose power-series coefficients count parse trees, and the resulting algebraic function explains why ambiguity grows exponentially.
- Feb 25, 2026 The Counting Argument for Circuit Size Lower Bounds Why almost every Boolean function on n bits needs about 2^n/n gates, how Lupanov matched that bound from above, and why the argument cannot name a single hard function.
- Jan 28, 2026 Ladner's Theorem: Building Languages Between P and NP How to construct an NP language that is neither in P nor NP-complete assuming P differs from NP, using a slow diagonalization that delays each requirement until the padding is large enough.
- Jan 26, 2026 Razborov-Smolensky and the Limits of Modulo Gates How low-degree polynomials over a finite field stand in for constant-depth circuits, and why AC0 with MOD-p gates cannot compute MOD-q for a different prime.
- Jan 21, 2026 Encoding Turing Machines and the Undecidability of Acceptance How a machine becomes a finite string, what a configuration record contains, and why diagonalization over that encoding rules out any decider for acceptance.
- Jan 5, 2026 Alternating Automata: Universal Branching and the Cost of Free Complementation What happens when a state may demand that all successors accept rather than one, how the acceptance game is played, and why one-way alternation shrinks descriptions without changing the exponential determinization bound.
- Dec 10, 2025 Certificates and the Two Definitions of NP Why "solved quickly" and "checked quickly" describe the same class, how the verifier definition is proved equivalent to nondeterministic machines, and what the certificate length bound actually constrains.
- Nov 29, 2025 The De Bruijn Criterion and What a Proof Kernel May Assume Why a proof assistant separates a small trusted checker from large automation, what the kernel must implement, and which shortcuts quietly enlarge what must be trusted.
- Nov 18, 2025 Distinguishing Strings and the Myhill-Nerode Theorem How the set of right contexts partitions a language into classes, why that partition is exactly the minimal DFA, and how to use it as an upper bound in proofs.
- Nov 10, 2025 The Post Correspondence Problem as a Reduction Source How a set of domino pairs encodes a computation through matched strings, why no algorithm can decide whether a match exists, and why this formulation is the convenient origin for other undecidability proofs.
- Nov 6, 2025 Monotone Circuits and the Approximation Method Why negations make lower bounds hard, how Razborov and Alon-Boppana proved exponential monotone size for clique, and what the method cannot say about matching.
- Nov 2, 2025 The Natural Proofs Barrier and Why Circuit Lower Bounds Stall What makes a lower-bound argument natural, why such arguments cannot separate P from NP unless factoring is easy, and which techniques escape the barrier.
- Sep 19, 2025 Recognizers, Dovetailing, and Complement Asymmetry Why a machine that halts on every yes-instance but may loop on no-instances cannot be closed under complement, and how interleaved simulation converts a recognizer into one for a different set.
- Sep 2, 2025 Alphabets, Strings, and the Closure Properties That Define a Language Class Why formal languages are studied as sets of strings, how closure under composition operations determines what a class can express, and why descriptions rather than sets carry the theory.
- Aug 20, 2025 Circuit Families and the Non-Uniform Model of Computation How a Boolean circuit encodes one fixed input length, why decision problems need whole families of them, and what the missing uniformity assumption costs.
- Aug 18, 2025 The Switching Lemma and Why Parity Needs Depth to Compute How random restrictions collapse constant-depth circuits, why the lemma proves AC0 cannot compute parity, and where the argument runs out of room.
- Aug 4, 2025 Entropy Rate of a Markov Source and the Value of Context Why the per-symbol cost of a source with memory is not its order-0 entropy, how the entropy rate is computed from a transition matrix, and what context models capture that frequency tables cannot.
- May 27, 2025 Bracket Abstraction: Compiling Lambda Terms into Combinators How the lambda-free basis S and K can express every abstraction, the translation that removes binders one at a time, and why the naive translation explodes in size.
- May 21, 2025 Many-One Reductions and What Completeness Requires The mechanics of Karp reductions, why hardness and completeness are different properties, and the closure conditions a class must satisfy for a complete problem to exist.
- May 6, 2025 Where the 2^n Comes From: Subset Construction and the Limits of Determinization Why determinizing an n-state NFA can require exponentially many states, how to exhibit a language that forces the blow-up, and which partial determinization schemes keep it bounded in practice.
- Mar 30, 2025 Fixed-Point Combinators and How Recursion Enters a Nameless Calculus Why a finite lambda term cannot refer to itself, how the Y and Turing combinators manufacture self-reference through duplication, and what the Z variant fixes about call-by-value.
- Mar 18, 2025 Differentiating a Regular Expression: Residual Languages as Automaton States How the Brzozowski derivative turns matching into repeated symbolic differentiation, why the residual languages are already DFA states, and where the construction blows up.
- Mar 2, 2025 Gate Basis, Fan-In, and What Circuit Size Actually Counts Why the de Morgan basis, NAND alone, and unbounded fan-in bases give different gate counts, and how the conversions between them are constructed.
- Jan 28, 2025 Capture-Avoiding Substitution and the Substitution Lemma Why naive textual replacement of a variable silently changes the meaning of a term, how renaming repairs it, and what the substitution lemma guarantees about the interaction with reduction.
- Jan 24, 2025 Thompson Construction: Turning a Regular Expression into an Epsilon NFA Why the construction inserts empty transitions between fragments, how each operator rewires two boundary states, and where the 2n state bound comes from.
- Jan 22, 2025 Diagonalization and the Time Hierarchy Theorem How a machine that runs itself on its own description separates two time bounds, why the constructibility condition cannot be dropped, and what the theorem does not prove.
- Jan 17, 2025 Formula Size and the Tree-Shaped Restriction on Circuits What is lost when every gate may feed only one consumer, why parity needs a quadratic formula, and how circuit size converts to formula size at a quadratic cost.
- Dec 9, 2024 Mapping Reductions and the Halting Problem How a computable function that maps one language into another transfers undecidability, why the halting problem follows from acceptance by a reduction in the opposite direction, and where the construction breaks.
- Dec 4, 2024 Eta Conversion, Extensionality, and When Two Functions Are the Same What the eta rule asserts about functions that differ only in an unused argument, why it is unsound under call-by-value, and how eta-expansion survives in compilers as an arity fix.
- Nov 27, 2024 Chomsky Normal Form and the CYK Table How rewriting a grammar so every rule is A to BC or A to a makes cubic-time recognition possible, and why the table is indexed by substrings rather than by derivation prefixes.
- Nov 21, 2024 Proof Terms: Reading a Derivation as a Program The correspondence between natural-deduction proofs and typed lambda terms, why normalisation is evaluation, and which logical principles correspond to which programming constructs.
- Nov 20, 2024 Polynomial Time and the Machine-Independence of P How P is defined by counting steps on a Turing machine, why the class survives a change of machine model, and where the definition stops matching the idea of tractability.
- Nov 18, 2024 Configuration Graphs and Savitch's Reachability Argument How a nondeterministic space-bounded computation becomes a path problem in a configuration graph, and why reachability composes into a quadratic blowup in space rather than an exponential one.
- Nov 5, 2024 Prefix Codes, the Kraft Inequality, and Why Huffman Is Optimal How decodability without separators constrains code lengths, what the Kraft sum measures, and the exchange argument that makes Huffman coding the best prefix code for a known distribution.
- Nov 1, 2024 Oracles, Relativization, and the Limits of Diagonalization How adding an oracle changes what a proof can see, why there are oracles that collapse P and NP and oracles that separate them, and what that implies for any argument that treats machines as black boxes.
- Oct 29, 2024 Range Coding and rANS as Practical Entropy Coders How byte-oriented range coders and asymmetric numeral systems implement the arithmetic-coding ideal with integer state, and why interleaving makes the rANS variant parallelizable.
- Sep 17, 2024 Decision Procedures for Word Equations and Unification How Makanin’s algorithm decides whether two words with variables can be made equal, why the bound on solution length is enormous, and what unification gains from restricting to free function symbols.
- Sep 14, 2024 Dependent Types: Pi and Sigma as Generalised Function and Pair How quantifying over a type lets the result type mention the argument, why checking such types needs conversion, and where the dependent eliminators differ from the simply typed ones.
- Aug 22, 2024 Sparse Parity-Check Codes and Iterative Decoding How a low-density parity-check matrix defines a code, why belief propagation on its Tanner graph approaches capacity, and where trapping sets produce an error floor.
- Jun 5, 2024 Size-Depth Tradeoffs and the Block-Respecting Model How restricting a circuit to communicate only between fixed blocks of inputs turns depth into a measurable resource, and what the resulting bounds say about parity.
- May 4, 2024 Partition Refinement: Minimizing a DFA by Splitting Blocks How Hopcroft-style minimization refines an initial partition into equivalence classes of states, why splitting the smaller half gives O(n log n), and where the implementation gets it wrong.
- Apr 22, 2024 Combining Decision Procedures with the Nelson–Oppen Method How separate decision procedures for arithmetic, arrays, and uninterpreted functions are made to agree on shared variables, why stable infiniteness is required, and where non-convex theories force case splits.
- Mar 6, 2024 Shannon Entropy as the Expected Cost of an Outcome Why information is measured as the logarithm of reciprocal probability, how entropy averages that quantity over a source, and where the number stops describing anything real.
- Feb 2, 2024 The Depth Hierarchy: NC, AC, and the Cost of Wide Gates How NCi and ACi interleave, why the hierarchy collapses if NC1 equals NC, and what the known separations at the bottom actually prove.
- Jan 28, 2024 Church Encodings and the Cost of Representing Data as Functions How numerals, booleans, and pairs are built from nothing but abstractions, why predecessor is the hard case, and what unary representation costs in reduction steps.
- Dec 12, 2023 Mutual Information and the Capacity of a Noisy Channel How the largest reliable transmission rate is defined as a maximum of mutual information, why the binary symmetric channel peaks at an interior input distribution, and what the capacity formula does not promise.
- Nov 7, 2023 Beta Reduction and the Consequences of Evaluation Order How the single rewrite rule of the lambda calculus produces drastically different programs depending on where it is applied, and why normal order finds a value whenever one exists.
- Apr 13, 2023 Presburger Arithmetic and the Decidable Side of Number Theory Why the first-order theory of addition alone admits quantifier elimination and always terminates, and how the single operation of multiplication moves the same language across the undecidability line.
- Mar 10, 2023 Product Constructions: Intersection, Union, and Complement Without Rebuilding How pairing states from two machines computes a boolean operation on their languages, why complement needs a total transition function, and what the product costs in states.
- Feb 27, 2023 The Chomsky Hierarchy as a Ladder of Memory Each level of the hierarchy corresponds to a kind of store a machine may use: none, a stack, a bounded tape, an unbounded tape. What the grammar restrictions encode about that store.
- Sep 26, 2022 Cut Elimination and the Subformula Property Why removing the cut rule from a derivation bounds proof search to subformulas of the goal, what the elimination procedure costs, and where the bound fails to be useful.
- Jun 15, 2022 Confluence and the Church-Rosser Theorem for Beta Reduction Why the order of beta reductions cannot change the final answer, how the diamond property is proved by parallel reduction, and what the standardisation theorem adds.
- Jun 10, 2022 Why Three Literals Is the Pivot for Satisfiability The reduction from general CNF to 3-SAT, why 2-SAT is solvable in linear time while 3-SAT is complete, and how clause length controls the shape of the search space.
- Apr 29, 2022 Termination Checking and the Price of Consistency Why a total language cannot have a general fixpoint, how structural and size-change checks approximate termination, and what each approximation rejects.
- Apr 24, 2022 Derivations, Sentential Forms, and What a Parse Tree Actually Records How a grammar rewrites strings step by step, why leftmost derivations and parse trees are two views of one object, and where the correspondence breaks when a grammar is ambiguous.
- Jan 5, 2022 LZ77, LZ78, and the Shift from Symbols to Substrings How dictionary coders replace repeated substrings with back-references, why their output is not bounded by the source entropy, and how the parser design determines the compression actually obtained.
- Jan 3, 2022 Alternation and the Structure of the Polynomial Hierarchy How stacking existential and universal quantifiers over polynomial-length certificates produces a hierarchy of classes, why it collapses if any two levels coincide, and what complete problems look like at each level.