Skip to content

Dana Scott

Abstract

Dana Scott (born 1932) is a logician who twice gave computer science a mathematical object it had been missing. In the summer of 1957, as an IBM intern with Michael Rabin, he invented the nondeterministic finite automaton and proved it no more powerful than the deterministic one; the two shared the 1976 Turing Award for it. On a Saturday morning in November 1969, lying on a bed in a rented Oxford flat, he saw how to build a mathematical model of the untyped lambda calculus, which he had spent months arguing could not exist, and with Christopher Strachey turned it into denotational semantics, the standard way of saying what a program means. In between he helped prove the independence of the continuum hypothesis.

Dana Scott 2012
Dana Scott presenting “Lambda Calculus Then and Now” at the ACM Turing Centenary Celebration, 15 June 2012. Image: orcmid, CC BY 2.0, via Wikimedia Commons.

Berkeley and Princeton

Dana Stewart Scott was born in Berkeley, California, on 11 October 1932 and studied at the university there, where a philosophy professor’s course on formal logic led him to Alfred Tarski, and where as a sophomore he taught himself set theory, combinators and the lambda calculus from Paul Rosenbloom’s textbook and Alonzo Church’s short monograph. He took his BA in 1954 and went to Princeton to work with Church, finishing his PhD in 1958 with a dissertation on convergent sequences of complete Boolean algebras.

Princeton’s logic students then included Simon Kochen, Raymond Smullyan and, a year ahead of Scott, Michael Rabin, who became a close friend. In 1957 IBM recruited both of them as summer interns at its research group in Yorktown Heights, which was housed, the new building not being finished, in a vacant estate. “When Rabin and I got to the Lamb estate,” Scott recalled, “we didn’t know what to do.” John Myhill had lectured at Princeton on automata, so they decided to review that work from the point of view of model theory, as algebraic structures. The paper that came out of the summer, “Finite Automata and Their Decision Problems,” appeared in the IBM Journal of Research and Development in April 1959.

Its lasting idea was the nondeterministic automaton: a machine which, on reading a symbol, may have several possible next states rather than one, and which accepts an input if any path through the choices succeeds. “You don’t have to worry about the paths that don’t work out. You only have to find one successful one.” They proved that any such machine can be converted into a deterministic one, at the cost of exponentially more states, so that nondeterminism adds convenience and nothing else. Scott did not remember how they thought of it, “except maybe we kept coming into problems that it was difficult to create the states” for by hand. The construction is in every automata course, and the question of whether the same collapse holds for Turing machines, P versus NP, is the central open problem of the field (Automata Theory and Computability). The ACM gave Rabin and Scott the 1976 Turing Award for the paper.

Set Theory

Scott taught at Chicago (1958–60), Berkeley (1960–63) and Stanford (1963–67). When Paul Cohen proved in 1963 that the continuum hypothesis could not be proved from the axioms of set theory, Scott and Robert Solovay found a way to recast Cohen’s method of forcing in terms of Boolean-valued models, which made the independence proofs look like ordinary model theory; Scott’s account, “A Proof of the Independence of the Continuum Hypothesis,” was published in 1967, and the American Mathematical Society gave him the Steele Prize for it in 1972. Gödel, told of the approach, said he had thought of it years earlier but had never mentioned it, his constructible-sets proof being so much more important. Scott spent 1968–69 on sabbatical in Amsterdam, and in the summer of 1969, at a meeting of IFIP Working Group 2.2 that Patrick Suppes could not attend and sent him to instead, he met Strachey.

Oxford, November 1969

Christopher Strachey ran the Programming Research Group at Oxford and wanted a mathematics of what programs mean. Scott, “very, very much attracted” to the approach, took leave from Princeton and came to Oxford for the autumn of 1969. His first contribution was a critique. Strachey used Church’s untyped lambda calculus, in which a function can be applied to itself, and Scott argued that this had no mathematical model and that the semantics should be built on typed functions instead; he wrote up the typed alternative as a logic of computable functions, LCF, which Robin Milner later turned into the first proof assistant.

Then, one Saturday morning in November, in the guest room of the rented flat, he was thinking about the functions of functions of functionals in the LCF paper, each of which was the limit of finite approximations, and about how Cantor had built the rationals as a limit of finite ordered sets. “Maybe there’s a space of monotone functions that’s the limit of all the spaces at the finite types.” He worked out the details “very shortly”: an infinite tower of domains, each the space of continuous functions on the one before, whose limit, D∞, is isomorphic to its own function space, which is exactly what the untyped lambda calculus requires. “So I had to come to tell Strachey, ‘Oh no, look what happened. After all the criticisms I made of untyped lambda calculus, it turns out that there is a mathematical meaning to the untyped lambda calculus.’” Strachey “was very pleased, and he immediately adopted thinking of things in that way.”

The two monographs that followed, Scott’s “Outline of a Mathematical Theory of Computation” (November 1970) and their joint “Toward a Mathematical Semantics for Computer Languages” (1971), founded denotational semantics: the meaning of a program is a mathematical function, recursion is handled by taking the least fixed point of a continuous function on a domain, and a language is defined by giving such a function for each construct. The domains themselves, partial orders in which every element is the limit of finite pieces of information, are now called Scott domains, and the topology on them the Scott topology. He held the chair of mathematical logic at Oxford from 1972 to 1981.

Carnegie Mellon and After

After a 1978–79 sabbatical from Oxford at Xerox PARC, Scott moved to Carnegie Mellon in 1981 and taught there until 2003. The Royal Swedish Academy gave him the Rolf Schock Prize in Logic and Philosophy in 1997 and the Czech Academy the Bolzano Medal in 2001. He lives in Berkeley. Between November 2020 and February 2021 Gordon Plotkin, himself one of the founders of the semantics Scott made possible, interviewed him over Zoom in four sessions for the ACM’s Turing Award oral history. He still recommends, to anyone who asks what to read, his 1993 paper “A Type-Theoretical Alternative to ISWIM, CUCH, OWHY,” which is the LCF manuscript of 1969 finally published, and his 2000 reflections on Strachey.

Dead End: The Model That Proved Too Much

Scott built D∞ to answer a question about mathematical existence, and it did. It also did something he had not intended: it made the untyped lambda calculus respectable, and with it the dynamically typed, self-applicable style of programming he had argued against. His own preference, stated in the LCF paper and restated in the 1993 title, was for types. The theory he founded went both ways. Domain theory gave the typed functional languages, ML and Haskell among them, their semantics, and it gave the untyped ones theirs as well. Fifty years on, the argument between the two camps is still being conducted in the vocabulary he supplied to both sides, and the man who supplied it is on record, from the guest room in Oxford, saying “Oh no.”

📚 Sources