Computation — flashcards

Propositions correspond to types, proofs to terms, and proof normalisation to evaluation. In a dependently typed proof assistant this is not an analogy but the implementation.

A monic degree-n polynomial needs exactly n roots plus one scale (n+1 numbers) however it's written, but the two standard forms differ in more than notation. Coefficient form is evaluated by Horner's method, a sequential multiply-accumulate whose step k reads step k-1's output by construction — an unavoidable Θ(n) sequential critical path (parallel depth). Root form q∏(x-rᵢ) evaluates its n linear factors independently, then combines them by a parallel product reduction, giving Θ(log n) depth — the standard gap between a linear-recurrence/fold pattern and an associative-reduction pattern, general to computation and not special to polynomials. The mechanism behind the asymmetry: each root-form factor is x read in that root's own private frame (no shared origin across factors), so evaluating in parallel needs no shared reference to compare partial results, only an intrinsic tag (how many factors have deferred to the shared coordinate so far) — a count, not a position. Coefficient form, by contrast, is built by successively converting shared-frame data, which is exactly why extracting it (via Newton's identities, converting power sums to elementary symmetric functions — st/newton-identities) is itself sequential even though it never touches an actual root.

Finding a fair two-thief split of a necklace is PPA-complete already at the simplest case — two thieves, the friendliest group action a proof by Borsuk–Ulam could ask for. Filos-Ratsikas & Goldberg, 2018 (arXiv:1805.12559). This refutes the hypothesis that k-thief difficulty tracks the availability of free ℤ/k actions on spheres: hardness is present at the friendliest case there is, so it is an artefact of the topological proof route rather than an obstruction inherent to the problem.

Haskell Curry, then William Howard, 1934 (Curry), 1969 (Howard).

Aris Filos-Ratsikas and Paul Goldberg, 2018.

Algorithms are often taught as precise logic, after a foundations course.

Computability is a question about formal systems, logically prior to any physical machine.

Propositions ↔ types, proofs ↔ programs, proof normalisation ↔ program evaluation. Logic and computation turn out to be the same subject written twice.

The halting problem's undecidability yields incompleteness directly: if provability were complete, halting would be decidable.

Once a system can encode its own halting, the fate of a process stops being determinable in advance. The cost of enough expressive power is that you can no longer see the end from the beginning.

Optimality elsewhere on this map means an approximation sequence is the best available at its size. A completeness result is the same question asked of a search procedure: PPA-completeness of necklace-splitting says no algorithm can do asymptotically better than the hardest problem in its class, already at the friendliest case (two thieves). The property is the same idea one level up — best-possible, now measured in cost rather than in closeness.

The pre-formal idea of a method you could just follow step by step — the intuition later made rigorous.

Turing's formal model of computation; the basis for algorithmic complexity and the P vs NP question.

Computation as function abstraction and application, with types constraining what may be applied to what.

Not just whether a proof of existence can be turned into a procedure, but what that procedure has to cost — classified by reduction into complexity classes (PPA, PPAD, TFNP and the rest) rather than judged case by case. Turing machines ask whether a method exists at all; this asks what the cheapest one can possibly do, and a completeness result is the sharpest form of that question — it says a whole class of problems is exactly as hard as its hardest member.

Good at — Impossibility and cost. This cannot be decided at all; that needs at least this much time; this problem is secretly the same as that one. It is the only area that routinely proves a method cannot exist.

Bad at — Saying what is true. It reports what is reachable, not what holds. And its own central question about cost has resisted every technique it has produced.