Program Semantics

The mathematical definition of what a program means — operational (how it runs), denotational (what value it computes), or axiomatic (what properties it guarantees). Verifiable ACL semantics require programs whose meaning is pinned down precisely enough for conformance to be checked.

In this vault

Language, semantics, and concurrency lineage

graph TD
  CH["Chomsky (1956)<br/>Three Models for the Description of Language"] --> GRAM[Formal grammars]
  MC["McCarthy (1960)<br/>Recursive Functions of Symbolic Expressions"] --> LISP[LISP / λ-calculus lineage]
  MC --> MS["McCarthy (1962)<br/>Towards a Mathematical Science of Computation"]
  MS --> CC["McCarthy & Painter (1966)<br/>Correctness of a Compiler for Arithmetic Expressions"]
  FL["Floyd (1967)<br/>Assigning Meanings to Programs"] --> AX[Axiomatic / inductive assertions]
  NAUR["Naur<br/>Proof Method for Cyclic Programs"] --> AX
  NAUR --> APP[Application of cyclic-program method]
  CC --> AX
  AX --> HOARE["Hoare (1978)<br/>Communicating Sequential Processes"]
  HEW["Hewitt (1973)<br/>Actor Formalism"] --> CONC[Concurrent message-passing]
  HOARE --> CONC
  CONC --> PI[π-calculus / process calculi]
  LISP --> BK["Backus (1978)<br/>Can Programming Be Liberated from the von Neumann Style"]
  BK --> FP[Functional programming]
  AX --> PS((Program Semantics))
  PI --> ACL[[Agent Communication Languages]]
  FP --> ACL

Papers: Three Models for the Description of Language · Recursive Functions of Symbolic Expressions and Their Computation by Machine · Towards a Mathematical Science of Computation · Correctness of a Compiler for Arithmetic Expressions · Assigning Meanings to Programs · A Proof Method for Cyclic Programs · An Application of a Method for Analysis of Cyclic Programs · Communicating Sequential Processes · Can Programming Be Liberated from the von Neumann Style · A Universal Modular Actor Formalism for Artificial Intelligence

Backlinks

concept-map line 145
Verifiable Semantics for ACLs line 32

Linked Pages

A Universal Modular Actor Formalism for Artificial Intelligence

Reference

Hewitt, C., Bishop, P., & Steiger, R. (1973). “A Universal Modular Actor Formalism for Artificial Intelligence.” Proceedings of the 3rd International Joint Conference on Artificial Intelligence (IJCAI), 235-245. URL

Summary

Hewitt, Bishop, and Steiger introduce the Actor — a universal computational primitive that unifies data, procedure, and process under a single kind of object. An actor is an active agent with behavior defined entirely by the messages it sends and receives. All computational structures — numbers, functions, semaphores, cells, queues, interpreters — are modeled uniformly as actors that respond to messages. Control flow and data flow are inseparable; sending a message replaces goto, call-return, interrupt, and semaphore operations with a single mechanism.

The paper grew out of the PLANNER project and explicit dissatisfaction with the von Neumann / stored-program paradigm dominant in AI languages. In place of “program counter + global memory + interrupts,” the actor model offers local state per actor, inherent concurrency via simultaneous message sends, and a coherent account of parallelism that scales from fine-grained numeric computation to large, autonomous agents. The authors emphasize intentions as first-class properties — an actor’s intention is the contract it guarantees to satisfy for its senders, supporting a form of declarative meta-evaluation and debugging.

Hewitt’s framework anticipated and influenced a long arc of subsequent work: Smalltalk’s message-passing object model, Agha’s formalization of actor semantics, Erlang/OTP’s supervised processes and let-it-crash philosophy, the Akka framework, CSP (Hoare) which formalized a closely related but channel-centric style, and contemporary actor-based agentic systems. The paper’s insistence that “creation, control, and communication” are one mechanism remains the defining alternative to shared-memory concurrency.

Key Ideas

Actor = message-receiving agent: a single primitive subsumes data, procedures, processes.
Message passing only: no shared memory, no goto, no interrupt, no semaphore.
Inseparability of control and data: computation is intrinsic — “ask not what you can do to an object; ask what the actor will do for you.”
Inherent concurrency: every message send is potentially parallel.
Intentions / contracts: each actor publishes obligations; meta-evaluators check that behavior satisfies intentions.
Modularity via encapsulation: actors expose only message interfaces; internal state is private.
Universality: the formalism expresses every computational construct needed for AI programming without primitive aggregates.
Hierarchies of scheduling, intention, monitoring, binding, resource management: supervisory structures emerge naturally.

Connections

Actor Model
Programming Erlang Second Edition — the most successful large-scale realization.
Let It Crash
Supervision Tree
A Language-Based Approach To Prevent DDoS
The Society of Mind — Minsky’s agent-of-agents shares the intuition.
Communicating Sequential Processes — Hoare’s contemporary rival formulation.
Hoare Logic

Conceptual Contribution

Can Programming Be Liberated from the von Neumann Style

Can Programming Be Liberated from the von Neumann Style? A Functional Style and Its Algebra of Programs

Reference

Backus, J. (1978). “Can Programming Be Liberated from the von Neumann Style? A Functional Style and Its Algebra of Programs.” 1977 ACM Turing Award Lecture. Communications of the ACM, 21(8), 613-641. URL

Summary

In his Turing Award lecture, Backus — the inventor of Fortran — delivers a startling self-critique of conventional programming languages. He argues that languages from Fortran through Algol to Pascal are all essentially von Neumann languages: they inherit the word-at-a-time, stored-program architecture’s assumptions (variables, assignment, statement sequencing, control flow through a single instruction pointer) and therefore suffer its bottlenecks. Programs written in this style are fat, inelegant, resist composition, and cannot be reasoned about algebraically because their meaning depends on an ever-changing hidden state.

As an alternative, Backus proposes FP — a functional programming language built from a small set of primitive functions and a handful of higher-order combining forms (composition, construction, condition, apply-to-all, insert). Programs are expressions that compose functions without mentioning variables or state. Crucially, FP comes equipped with an algebra of programs: equational laws that let one transform programs by substitution, exactly as one transforms algebraic expressions. A worked inner-product example shows the dramatic size and transparency gains: the FP version is a line of combinators; the Fortran version is a loop with state-manipulating assignments.

The lecture’s impact has been enduring and multifaceted. FP itself did not become mainstream, but its argument animated Haskell, ML, and the broader functional turn; its algebraic equations seeded Bird-Meertens “squiggol” formalism and the point-free programming style; its critique of the von Neumann bottleneck anticipated dataflow, array languages (APL/J/K), and GPU/SIMD programming. Backus’s central thesis — that programming needs a mathematical theory within which programs can be manipulated — is echoed in every modern effort to make software more composable, verifiable, and parallelizable.

Key Ideas

Von Neumann bottleneck: word-at-a-time traffic between CPU and store is inherited by conventional programming languages, making them conceptually as well as physically slow.
State and assignment as original sin: they block algebraic reasoning and force programmers to think like the machine.
FP (Functional Programming): a variable-free, point-free language of functions and combining forms.
Combining forms: composition, construction, condition, apply-to-all (map), insert (fold/reduce), while.
Algebra of programs: equational laws enabling syntactic program transformation and optimization.
Two kinds of functions: ordinary (first-order, operate on values) vs. combining forms (build new functions).
Program = expression: no statements, no mutable variables, no sequencing — just function composition.
Mathematical semantics: each program denotes a function; equivalence is extensional equality.

Connections

The Extensible Language - Graham
Code as Data
Recursive Functions of Symbolic Expressions and Their Computation by Machine — McCarthy’s LISP is the other founding functional work.
Algorithm = Logic + Control — Kowalski’s parallel argument for separating meaning from machinery.
A Universal Modular Actor Formalism for Artificial Intelligence — another push beyond stored-program orthodoxy.

Conceptual Contribution

Communicating Sequential Processes

Reference

Hoare, C. A. R. (1978). “Communicating Sequential Processes.” Communications of the ACM, 21(8), 666-677. URL

Summary

Hoare proposes that input, output, and concurrent composition of processes deserve the same foundational status as assignment, sequencing, and iteration. CSP is a small language in which programs are built from sequential processes that synchronise by unbuffered, typed message exchange over named channels. A send P ! v and a matching receive Q ? x rendezvous: neither proceeds until both are ready. Dijkstra’s guarded commands — with nondeterministic choice — are generalized so that a guard may include a communication action, yielding a clean treatment of external choice, alternation, and fair scheduling.

The paper walks through a progression of examples — coroutines, prime sieve, matrix multiplication, bounded buffer, recursive subroutines implemented as processes, the dining philosophers — demonstrating how seemingly exotic concurrent patterns become compact CSP programs. Hoare’s deliberate methodological stance is that structured concurrency can be as tractable as structured sequential programming, provided the primitives are well-chosen: synchronous rendezvous avoids the subtleties of mailboxes and shared state; named channels make communication explicit in the program text; guarded commands make nondeterminism principled.

CSP seeded a lineage of enormous practical and theoretical impact: occam (the transputer language), the CSP process algebra (Hoare 1985, Roscoe) with refinement-based verification via FDR, the Go programming language’s goroutines and channels, Rust’s std::sync::mpsc, and the modern “structured concurrency” revival. Together with Hewitt’s actors, CSP defines one of the two great alternatives to shared-memory threads.

Key Ideas

Synchronous message passing: unbuffered rendezvous between named processes; no shared memory.
Named channels / named processes: communication is part of program structure, syntactically explicit.
Guarded commands with I/O guards: nondeterministic alternation and repetition over communications.
Parallel composition (||): processes execute concurrently, synchronizing only at matched send/receive.
No implicit buffering: forces designers to reason about liveness and deadlock directly.
Refinement and equivalence: later formalized as a process algebra with bisimulation / failures refinement.
Structured concurrency: parallelism as a first-class program-structuring mechanism, not threads-as-afterthought.

Connections

Actor Model — the other great message-passing tradition; CSP is channel-centric where actors are mailbox-centric.
A Universal Modular Actor Formalism for Artificial Intelligence
Hoare Logic — Hoare’s earlier work on axiomatic reasoning underlies his insistence on structured primitives.
Time Clocks and the Ordering of Events in a Distributed System — rendezvous provides a stronger local synchrony than Lamport’s messages.
Let It Crash

Conceptual Contribution

An Application of a Method for Analysis of Cyclic Programs

Reference: Nissim Francez (1978). IEEE Transactions on Software Engineering SE-4(5): 371-378. URL (DOI: 10.1109/TSE.1978.233857). No open-access PDF located — IEEE paywall, no author preprint on Francez’s Technion page. Cited in McCarthy’s Elephant 2000 - A Programming Language Based on Speech Acts.

Summary

The applied companion to A Proof Method for Cyclic Programs. Francez uses the Francez-Pnueli cyclic-program proof method to prove Dijkstra’s “on-the-fly” garbage collector correct — a paradigmatically hard concurrent, cyclic program in which a mutator and a collector cooperate to manage a shared heap. The paper also compares the Francez-Pnueli approach with an alternative proof of the same algorithm by David Gries using Owicki’s method, discussing what each approach reveals about the algorithm’s invariants and interference structure.

McCarthy cites this paper in Elephant 2000 as concrete evidence that the cyclic-program proof methodology scales to a real concurrent reactive system, supporting his claim that Elephant’s non-terminating speech-act programs admit tractable verification.

Key Ideas

Case study: Dijkstra’s on-the-fly concurrent garbage collector, proved correct in the Francez-Pnueli framework.
Concurrent cyclic behaviour: mutator/collector cooperation analysed via eventual-behaviour invariants.
Comparison with Owicki/Gries: contrasts the Francez-Pnueli cyclic-programs method with Gries’s proof of the same algorithm using the Owicki interference-freedom approach.
Methodological lessons: shows which invariants each proof style makes natural and which it leaves implicit.

Connections

Elephant 2000 - A Programming Language Based on Speech Acts — McCarthy cites this alongside the Francez-Pnueli method paper
A Proof Method for Cyclic Programs — the method applied here
Program Verification
Formal Verification
Hoare Logic
Assigning Meanings to Programs
Verification Condition

Conceptual Contribution

Claim: The Francez-Pnueli cyclic-programs proof method is tractable and perspicuous on a paradigmatically hard concurrent cyclic program — Dijkstra’s on-the-fly garbage collector — and yields a qualitatively different (and in places more natural) account than the Owicki/Gries interference-freedom proof of the same algorithm.
Mechanism: Construct eventual-behaviour invariants describing the mutator/collector cooperation; discharge safety (no live cell is collected) and liveness (garbage is eventually reclaimed) via the cyclic-programs proof rules; juxtapose with Gries’s Owicki-style proof to characterise the methodological difference.
Concepts introduced/used: Program Verification, Formal Verification, Hoare Logic, Verification Condition
Stance: case-study / methodological
Relates to: Pairs with A Proof Method for Cyclic Programs as the empirical leg of the Francez-Pnueli programme on reactive-system verification. McCarthy uses the pair in Elephant 2000 - A Programming Language Based on Speech Acts to argue that the non-terminating, history-referring programs he proposes for speech-act I/O are within reach of contemporary verification techniques — i.e. the “program as logical sentence” stance need not pay a verifiability tax.

Tags

A Proof Method for Cyclic Programs

Reference: Nissim Francez & Amir Pnueli (1978). Acta Informatica 9: 133-157. URL (DOI: 10.1007/BF00289074). No open-access PDF located — Springer paywall, no author preprint on Francez’s Technion page, no Weizmann tech-report copy surfaced. Cited in McCarthy’s Elephant 2000 - A Programming Language Based on Speech Acts.

Summary

Francez and Pnueli propose a proof method for cyclic programs — programs (sequential or concurrent) that are not meant to terminate but to sustain an ongoing, repetitive behaviour: operating systems, reactive processes, garbage collectors. The traditional input-output Hoare-style correctness notion is inapplicable to such programs because there is no terminating output. The paper replaces input-output correctness with a notion of eventual behaviour: properties that must hold infinitely often, eventually, or persistently across the program’s execution, and develops a proof methodology (a precursor of what would become temporal-logic program verification) for discharging these properties.

The paper is an important early step between Floyd-Hoare partial-correctness verification and Pnueli’s subsequent temporal logic of programs (1977). McCarthy cites it in Elephant 2000 as prior art on verifying programs whose specifications are not input-output but ongoing-behaviour — exactly the shape of Elephant programs, whose speech-act semantics concerns sequences of illocutions over time rather than a single terminating output.

Key Ideas

Cyclic programs: non-terminating sequential/concurrent programs whose correctness is about sustained behaviour, not terminal output.
Eventual behaviour: replaces input-output correctness with properties like “infinitely often,” “eventually,” “persistently.”
Proof method: invariant-style reasoning adapted to the cyclic setting, supporting both sequential and concurrent programs.
Precursor to temporal logic: the informal modalities here are systematised in Pnueli’s 1977 temporal logic of programs.
Concurrency: the method handles cooperating concurrent processes, anticipating Owicki/Gries-style proof rules.

Connections

Elephant 2000 - A Programming Language Based on Speech Acts — McCarthy cites this as prior art on verifying non-terminating / reactive programs
An Application of a Method for Analysis of Cyclic Programs — Francez’s 1978 TSE companion paper applying the method to Dijkstra’s on-the-fly garbage collector
Program Verification
Formal Verification
Hoare Logic
Assigning Meanings to Programs
Verification Condition

Conceptual Contribution

Claim: Non-terminating (cyclic) programs admit a rigorous correctness theory if one replaces the input-output correctness paradigm with a proof method over eventual behaviour — properties of the infinite execution — and this method extends to concurrent cyclic programs.
Mechanism: Generalised invariants characterising the sustained behaviour, combined with proof rules that discharge eventual/persistent properties directly rather than deriving them from pre/post pairs. For concurrent programs, the method handles process interaction via cooperation conditions.
Concepts introduced/used: Program Verification, Formal Verification, Hoare Logic, Verification Condition
Stance: methodological / verification-foundations
Relates to: A key transitional work between Floyd-Hoare partial-correctness verification (Assigning Meanings to Programs, Hoare Logic) and Pnueli’s subsequent temporal logic of programs (1977). McCarthy’s Elephant 2000 - A Programming Language Based on Speech Acts positions the paper as evidence that programs whose correctness is an ongoing speech-act record (rather than a terminal output) are already within verification’s reach — the “program as logical sentence” stance just extends this to the speech-act level.

Tags

Assigning Meanings to Programs

Reference: Robert W. Floyd (1967). Proceedings of Symposia in Applied Mathematics, Vol. 19, pp. 19-32 (AMS). Source file: FloydMeaning.pdf. URL

Summary

Floyd’s foundational paper establishes a rigorous, axiomatic basis for proving properties of programs — correctness, termination, equivalence — by attaching propositions (tags) to the edges of a flowchart. A verification condition for each command type guarantees that if the tag on its entrance edge is true when control arrives, then the tag on its exit edge is true when control leaves. Induction over execution then proves global properties like “if initial values satisfy R1, final values satisfy R2”.

The paper defines completeness and consistency of a semantic definition, gives general axioms (axioms 1-4 and corollaries), and derives verification conditions for assignment, conditional branch, join, start, and halt in a simple flowchart language, then extends the approach to fragments of ALGOL. It is a foundational work in axiomatic semantics, directly inspiring Hoare logic.

Key Ideas

Interpretation = mapping from flowchart edges to propositions.
Verification condition per command type enforces local soundness.
Global correctness by induction over execution steps.
Semantic definition should be complete and consistent.
Termination proofs by showing a well-founded quantity strictly decreases.

Connections

Language Workbenches
Agent-Oriented Programming
Verifiable Semantics
Code as Data
Intent Formalization - A Grand Challenge for Reliable Coding — Floyd/Hoare specs as the LLM-era correctness oracle
Making Smart Contracts Smarter — semantic-gap diagnostics in a blockchain setting
Hoare Logic

Conceptual Contribution

Claim: A programming language’s semantics can be defined independently of any implementation by attaching propositions to flowchart edges and constructing per-command verification conditions; global program properties then follow by induction.
Mechanism: Flowchart interpretation as a map from edges to propositions; four general axioms governing verification conditions; derivation of V_c for assignment, branch, join, start, halt; extension to an ALGOL subset (conditional, goto, for, compound, declarations); termination via well-founded decreasing quantities.
Concepts introduced/used: Axiomatic Semantics, Verification Condition, Strongest Verifiable Consequent, Consistency and Completeness, Inductive Assertions, Termination Proof
Stance: foundational / formal-semantic
Relates to: Direct ancestor of Hoare logic and of every verifiable-semantics move in the vault, including Verifiable Semantics for ACLs which transports Floyd/Hoare-style program semantics into the ACL-conformance question. Foundational for Foundations of Logic Programming - Lloyd and reasoning tools in A Modular Approach to Metatheoretic Reasoning for Extensible Languages.

Tags

Correctness of a Compiler for Arithmetic Expressions

Reference: John McCarthy and James Painter (1967). “Correctness of a Compiler for Arithmetic Expressions.” In Mathematical Aspects of Computer Science (Proc. Symposia in Applied Mathematics, vol. 19), American Mathematical Society, pp. 33-41. URL

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.

Tags

Towards a Mathematical Science of Computation

Reference: John McCarthy (1963). “Towards a Mathematical Science of Computation.” In Information Processing 1962: Proceedings of IFIP Congress 62, North-Holland, pp. 21-28. (Version fetched is the 1996 revised reprint.) URL

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
An Unsolvable Problem of Elementary Number Theory — Church 1936, the undecidability bound McCarthy invokes as the horizon of a “practically adequate” theory.
General Recursive Functions of Natural Numbers — Kleene 1936, the recursive-function substrate underpinning McCarthy’s formalism.
Recursively Enumerable Sets of Positive Integers and Their Decision Problems — Post 1944, the unsolvability theory framing termination and decidability limits.

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.

Tags

Recursive Functions of Symbolic Expressions and Their Computation by Machine

Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I

Reference: John McCarthy (1960). “Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I.” Communications of the ACM 3(4): 184-195. (Author-hosted LaTeX reformatting with minor notational changes.) Source file: mccarthy-recursive.pdf. URL

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.

Connections

Programs with Common Sense — Lisp was originally designed to support the advice taker.
Some Philosophical Problems from the Standpoint of Artificial Intelligence
Epistemological Problems of Artificial Intelligence
Towards a Mathematical Science of Computation — continues the theory-of-computation programme.
Correctness of a Compiler for Arithmetic Expressions — first proof of program correctness uses Lisp-like semantics.
First Order Theories of Individual Concepts and Propositions
Ascribing Mental Qualities to Machines
Circumscription - A Form of Nonmonotonic Reasoning
Generality in Artificial Intelligence
Elephant 2000 - A Programming Language Based on Speech Acts
Common Business Communication Language
The Extensible Language - Graham — Graham’s manifesto for the Lisp extensibility culture.
Code as Data — the homoiconicity principle first made concrete here.
Macros as Language Extension — macros exploit the S-expression representation of programs.
Creating Languages in Racket — modern Racket inherits eval/apply as the DSL substrate.
Lisp
Knowledge Representation
Common Sense Reasoning
An Unsolvable Problem of Elementary Number Theory — Church 1936, the λ-calculus whose notation McCarthy adapts for anonymous functions.
General Recursive Functions of Natural Numbers — Kleene 1936, the partial-recursive-function framing Lisp realises over S-expressions.

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.

Three Models for the Description of Language

Reference: Noam Chomsky (1956). IRE Transactions on Information Theory. Source files: 195609-.pdf, chomksy.txt. URL

Summary

Chomsky’s seminal paper comparing three candidate models of linguistic structure — finite-state Markov processes, phrase-structure grammars, and transformational grammars — and showing that each is strictly more powerful than the last. He proves that English cannot be described by any finite-state grammar (via dependencies like “either…or”, “if…then” that require unbounded memory), and argues that even phrase-structure grammars, while formally adequate, yield awkward and complex descriptions of phenomena (auxiliaries, passives, discontinuous elements) that transformational rules handle elegantly.

The paper founded generative linguistics and the Chomsky hierarchy, and established transformational grammar as the preferred formalism for natural-language syntax.

Key Ideas

Finite-state grammars cannot generate English (mirror-image / nested dependencies)
Phrase-structure grammars more powerful but still inadequate for transformations
Transformational grammar operates on phrase markers, not strings
Distinction between grammar as discovery procedure vs. evaluation procedure
Foundations of the Chomsky hierarchy

Connections

Conceptual Contribution

Claim: Natural language (English) is not finitely describable by a finite-state Markov process, nor adequately by a pure phrase-structure grammar; a transformational grammar built on top of phrase structure is materially simpler and exposes genuine linguistic insight.
Mechanism: Three candidate models examined formally — (1) finite-state Markov processes, shown incapable of generating mirror-image / nested-dependency constructions central to English; (2) phrase-structure (context-free) grammars, adequate in principle but producing unwieldy, redundant grammars; (3) transformational grammars, where a kernel of simple sentences plus transformations derives the rest, yielding compact and explanatorily powerful descriptions.
Concepts introduced/used: Finite-state Grammars, Phrase-structure Grammar, Context-Free Grammars, Transformational Grammar, Chomsky Hierarchy, Generative Grammar, Kernel Sentences, Markov Processes, Compositionality
Stance: formal / linguistic-theory
Relates to: Foundational reference point for any discussion of language structure, including emergent-language work (Emergence of Grounded Compositional Language in Multi-Agent Populations, Multi-Agent Cooperation and the Emergence of Natural Language) where “compositionality” is the property Chomsky’s phrase-structure was designed to capture. Complements Algorithmic Information Theory - Grunwald Vitanyi’s description-length view with a structural/syntactic one. Distant ancestor of the parser-design rigour demanded by PKI Layer Cake - Kaminsky Patterson Sassaman.

Tags

Hoare Logic

Axiomatic program-verification system based on Hoare triples {P}C{Q}; direct descendant of Floyd’s edge-assertion method.

In this vault

Operational Semantics

Defining a program’s meaning by the sequence of computation steps it induces on an abstract machine.

In this vault

Verifiable Semantics for ACLs

Verifiable Semantics for Agent Communication Languages

Reference: Michael Wooldridge (1998). ICMAS-98 (International Conference on Multi-Agent Systems). Source file: icmas98.pdf. URL

Summary

Wooldridge tackles a central problem for ACL standardization: how can an external observer verify that an agent conforms to an ACL’s semantics when semantics are expressed in modal BDI logic (beliefs, desires, intentions)? He formalizes an agent communication framework as a tuple containing agent programs, local states, a communication language, a semantic language, and interpretation functions, and defines precisely what it means for a framework to be verifiable: whether one can decide, from program text alone, that the semantic conditions for a sent message are satisfied.

He shows that KQML and FIPA-97 ACL, which define the “sincerity condition” for an inform act using multi-modal quantified logics like SL, are not practically verifiable — deciding whether an agent program really believes what it says requires checking undecidable properties. In contrast, he gives two example frameworks with verifiable (even co-NP-complete) semantics by grounding meaning in program states rather than unobservable mental attitudes. The paper’s upshot: practical ACL conformance testing requires public, state-based semantics.

Key Ideas

Formal agent communication framework as a 2n+4 tuple.
Verifiability = decidability of semantic conformance from program text.
KQML and FIPA-97 semantics (SL modal logic) are not practically verifiable.
Grounding semantics in program states yields co-NP-complete verifiability.
Motivates social/public commitment-based ACL semantics.

Connections

Conceptual Contribution

Claim: An ACL standard is only useful if one can check whether an implementation respects it; existing ACLs (KQML, FIPA-97) whose semantics are given in multi-modal BDI logics are not practically verifiable, so ACL semantics should instead be grounded in program states.
Mechanism: Formalises an agent communication framework as a (2n+4)-tuple of agent programs, local states, communication language L_C, semantic language L_S, and interpretations; defines verifiability as decidability (in polynomial time) of whether an agent program respects a message’s semantic precondition; shows FIPA’s SL semantics undecidable; constructs two verifiable example frameworks (classical propositional logic, grounded propositional epistemic logic) with co-NP-complete verification.
Concepts introduced/used: Verifiable Semantics, Agent Communication Framework, Sincerity Condition, Grounded Semantics, Program Semantics, Model Checking, BDI Logic, Mentalistic Semantics
Stance: formal-semantic / critique
Relates to: Formal companion to ACL Rethinking Principles — Singh’s social-agency argument becomes Wooldridge’s verifiability theorem. Undermines the semantic ambitions of KQML Overview and FIPA-ACL; motivates commitment-based approaches such as Agent Communication And Institutional Reality and the program-grounded framework in Foundations Of Illocutionary Logic.