State Vector

Compiler-correctness abstraction: the entire program state (memory, registers, program counter) packaged as a single value the source- and target-level semantics must correspond over.

In this vault

Summary

The first published machine-checkable-style proof that a compiler is correct. McCarthy and Painter take a trivially small source language — arithmetic expressions over constants, variables, and binary + — and a trivially small target — a single-accumulator machine with li, load, sto, add — and prove by structural induction that compile(e,t) run on the target produces the same accumulator value as the source semantics value(e, xi), while preserving the contents of low-numbered registers that hold the program’s variables.

The paper is methodologically landmark rather than technically deep: it formalises abstract syntax with isconst/isvar/issum predicates and selectors s1/s2; defines source semantics denotationally via a recursive value function; gives the object language both analytic and synthetic syntaxes (so that the compiler can construct code while the interpreter can destructure it); introduces state vectors with c(x,eta) for contents and a(x,alpha,eta) for update; defines outcome as the fold of step over a program; and proves the decisive lemma outcome(p1*p2, eta) = outcome(p2, outcome(p1, eta)). Correctness is then stated as a partial-equality relation zeta1 =_A zeta2 — agreement on all registers except those in the scratch set A — and proved by induction on expression structure.

Key Ideas

Compiler correctness as a theorem provable by structural induction over abstract syntax.

Abstract syntax (predicates + selectors) as the mathematical object, with analytic/synthetic syntaxes mediating between interpreter and compiler.

Denotational source semantics via a value function; operational target semantics via step/outcome.

Partial equality =_A on state vectors — the scratch-register-agnostic equivalence needed to state the theorem.

Proof template transferable to richer compilers and machines — the intended contribution is methodological.

Connections

Towards a Mathematical Science of Computation — the companion manifesto paper; this is its concrete proof-of-concept.

Elephant 2000 - A Programming Language Based on Speech Acts — continues McCarthy’s conviction that programs should have mathematical semantics strong enough to support correctness proofs.

Foundations of Logic Programming - Lloyd — parallel project for declarative languages.

Knowledge Representation

Conceptual Contribution

Claim: Compiler correctness is a rigorous mathematical theorem, provable by structural induction once source and target are given abstract-syntax formalisations and denotational/operational semantics respectively.

Mechanism: Abstract analytic syntax with predicate/selector signatures; denotational value(e,xi); single-accumulator machine with analytic/synthetic syntax pair; state vectors with c (contents) and a (update); outcome(p,eta) defined by fold; decisive concatenation lemma; partial-equality relation =_A on state vectors; structural induction on expressions.

Concepts introduced/used: Abstract Syntax, State Vector, Compiler Correctness, Structural Induction, Program Verification, Denotational Semantics, Operational Semantics.

Stance: foundational

Relates to: Realises the program set out in Towards a Mathematical Science of Computation; template for every subsequent verified-compiler result (CompCert and descendants); the logical-specification-of-programs stance that Elephant 2000 extends to speech-act-embedded programs.

Summary

McCarthy’s IFIP 1962 address sketches what a mathematical science of computation should look like, by analogy with physics: starting from basic assumptions, one should be able to deduce the important properties of the entities the science deals with. He identifies those entities as problems, procedures, data spaces, programs (which are symbolic expressions representing procedures in particular languages), and computers (viewed as finite automata, but from a stored-program-plus-unbounded-storage perspective rather than a finite-state one).

The paper enumerates the kinds of facts one would like to derive — procedure equivalence, termination, compiler correctness, program transformation preserving semantics, lower bounds — and argues that Goedel’s incompleteness precludes a complete theory but a practically adequate one is feasible. McCarthy proposes an integer-free formalism, recursive definitions via conditional expressions (the paper is a locus classicus of if p then a else b as a mathematical notation), and recursion induction as a proof method. He closes by urging that debugging be replaced by machine-checked proofs of program correctness — a foundational statement of the program-verification agenda.

Key Ideas

Computation as a mathematical science with its own entities (problems, procedures, data spaces, programs, computers) distinct from automata theory.

Conditional expressions if p then a else b and recursion as the basis of a formal notation for defining functions.

Recursion induction as a proof technique for program equivalence.

Compiler correctness as a target theorem for the formalism.

Debugging should be supplanted by computer-checked correctness proofs — the founding manifesto of program verification.

Connections

Correctness of a Compiler for Arithmetic Expressions — the paired McCarthy–Painter paper that carries out the compiler-correctness proof sketched here.

Elephant 2000 - A Programming Language Based on Speech Acts — Elephant’s insistence that programs refer directly to past events and future commitments continues McCarthy’s project of giving programs a mathematical semantics amenable to proof.

Foundations of Logic Programming - Lloyd — shares the model-theoretic semantics-for-programs stance.

First Order Theories of Individual Concepts and Propositions

Knowledge Representation

Conceptual Contribution

Claim: Computation admits a mathematical science in the physics sense: basic assumptions from which properties of procedures, programs, and computers can be deduced, with program-correctness proofs replacing debugging.

Mechanism: Abstract syntax of programs; conditional expressions and recursion as a core notation; state vectors for machines; recursion induction; an integer-free formalism avoiding the Mostowski-style reliance on arithmetic coding.

Concepts introduced/used: Conditional Expressions, Recursion Induction, Abstract Syntax, State Vector, Compiler Correctness, Program Verification, Data Spaces.

Stance: foundational

Relates to: Grounds the semantic-correctness agenda that Elephant 2000 later inherits; complements Correctness of a Compiler for Arithmetic Expressions; the appeal to mathematical logic rather than automata foreshadows the logicist program in Ascribing Mental Qualities to Machines and Circumscription - A Form of Nonmonotonic Reasoning.

State Vector

In this vault

Backlinks