Conditional Expression

McCarthy’s (cond ...) primitive: a selector among alternatives evaluated lazily. Its introduction let recursive functions be defined purely, without imperative control flow.

In this vault

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.

Summary

The Lisp paper. McCarthy describes a programming system — LISP, for LISt Processor — developed for the IBM 704 at MIT, originally designed to support the advice taker of Programs with Common Sense by giving it a substrate for manipulating symbolic (declarative and imperative) sentences. The system evolved into a representation of partial recursive functions over a class of symbolic expressions (S-expressions) whose elegance transcended its motivating application. The paper presents S-expressions, a small set of elementary S-functions (atom, eq, car, cdr, cons), conditional expressions (newly introduced here), recursive function definitions via a λ-calculus-flavored notation, and the universal S-function apply that plays the role of a universal Turing machine and the practical role of an interpreter — the now-iconic code-is-data eval/apply kernel.

The paper then translates this formalism into IBM 704 list structures (the famous CAR/CDR naming reflecting the 704’s address and decrement register fields), describes the main features of the LISP system (garbage collection, interpreter, compiler sketch, free storage), and gives a recursive-function interpretation of flow charts — i.e., a semantics for imperative programs via recursive functions, anticipating much later work on denotational semantics. Conditional expressions, submitted by McCarthy as a letter to CACM and “demoted to a letter” by its editor (notes the footnote), were the notation Algol 60 then rejected in favour of if ... then ... else.

Lisp is simultaneously an AI implementation vehicle and a theory of computation — and the paper’s code-is-data property (programs are S-expressions) is what seeded the Lisp extensibility tradition (macros, embedded DSLs) that later runs through The Extensible Language - Graham, Code as Data, Macros as Language Extension, and Creating Languages in Racket. McCarthy closes promising a Part II on symbolic applications and a companion paper applying the recursive-function formalism to mathematical logic and theorem proving — the latter effectively becoming Correctness of a Compiler for Arithmetic Expressions and Towards a Mathematical Science of Computation.

Key Ideas

S-expressions: uniform tree/list data structure for both programs and data (code-is-data).

Five primitive functions (atom, eq, car, cdr, cons) suffice to define all computable functions over S-expressions.

Conditional expressions (p1 → e1, ..., pn → en) as a first-class construct — introduced to computer science here.

Recursive function definitions and λ-notation for anonymous functions.

Universal function apply — a meta-circular evaluator — plays the role of a universal Turing machine and a working interpreter.

Partial functions are inherent to computation (non-termination) and must be handled explicitly.

Flow charts reinterpreted as recursive function applications — an early denotational-style semantics for imperative programs.

Garbage collection (the concept of automatic reclamation of unreferenced list cells) introduced in the implementation notes.

Conceptual Contribution

Claim: Partial recursive functions over symbolic expressions can be defined with five primitive operators (atom, eq, car, cdr, cons) plus conditional expressions and recursion, yielding a language in which programs are themselves symbolic expressions and a single universal function apply serves as both a universal Turing machine and a working interpreter — giving a uniform substrate for AI, programming, and the theory of computation.

Mechanism: S-expressions (atomic symbols + dotted pairs, list sugar); five primitives; conditional expression (p → e, ...); recursive function definitions; λ-notation; universal apply(f, args); IBM 704 list-structure implementation; garbage collection; recursive-function semantics of flow charts.

Concepts introduced/used: Lisp, S-expression, Conditional Expression, Recursive Function, Code as Data, Homoiconicity, eval apply, Garbage Collection, Meta-circular Evaluator.

Stance: foundational

Relates to: The implementation substrate that Programs with Common Sense anticipated. Its code-is-data property seeds the extensibility tradition — The Extensible Language - Graham, Macros as Language Extension, Creating Languages in Racket — and its apply formalism is the ancestor of denotational semantics used in Correctness of a Compiler for Arithmetic Expressions and Towards a Mathematical Science of Computation.

Conditional Expression

In this vault

Backlinks