A basis for a mathematical theory of computation. (John McCarthy, 1961-3) [pdf] (www-formal.stanford.edu)

John McCarthy’s 1961–63 paper "A Basis for a Mathematical Theory of Computation" proposes a concise mathematical framework for describing and reasoning about algorithms and computing systems. Rather than restricting attention to integers or finite-state machines, McCarthy defines a class C{F} of functions computable from a given base collection F by using generalized composition, conditional expressions (notation: (p → e, ...)), and recursive definitions. He extends the formalism to computable functionals (functions that take functions as arguments), non‑computable-looking expressions obtainable via quantifiers that can often be transformed into computable forms, “ambiguous” functions whose values are only partially specified, and mechanisms for building new data spaces from base spaces. Concrete illustrations (e.g., conditional expression syntax, a recursive factorial evaluation) show how these constructs express familiar algorithms without committing to a fixed domain like the integers. The significance is twofold: technically, McCarthy supplies primitive, domain‑independent building blocks (composition, conditionals, recursion) plus a method—recursion induction—for proving equivalence of recursively defined functions, laying groundwork for program transformation and correctness proofs. Conceptually, he outlines an agenda (universal programming language, equivalence theory, symbolic program representation, formal models of machines, and a quantitative theory of computation) that presages functional programming, higher‑order semantics, type/structure constructors, and formal methods. While the paper delivers modest formal results, its formalisms and goals strongly influenced later language design (notably Lisp/functional paradigms) and the mathematical study of programs.