10
$\begingroup$

I have twice heard it attributed to Dana Scott that he said something to the effect that the consistency of the lambda-calculus was an accident.

Does anyone have a reasonable-sounding source for this? I find it hard to believe that Scott would talk about the Church-Rosser theorem in this way; I guess that this a mangling of something else he said, or some context is hidden.

Improve this question
$\endgroup$

2 Answers 2

Reset to default
19
$\begingroup$

You could ask him directly, but the story he told me was that he was working on domain theory because he wanted to give a denotational semantics of typed lambda calculus, or more generally typed programming languages. (He had been telling people they should design typed languages, rather than untyped ones, and so he wanted to show how a mathematical theory of typed programming languages would work.) But it turned out that his theory of domains also provides a model of the untyped lambda calculus. In this sense it was an accident.

I also asked him once why he thought it was important to give a model of the untyped lambda calculus when it had been known by the Church-Rosser theorem the calculus was consistent. I cannot reporoduce the exact answer, but in effect he said that it was important to understand what models of a theory looked like, not just that it was consistent. I think this reveals a certain "semantic" view of mathematics.

Improve this answer
$\endgroup$
4
  • $\begingroup$ Which suggests "domain-model-ability" is the property in question, and not "consistency". I think your suggestion is sound, and I probably should ask directly. The obvious advantage of domain models over, say, Böhm-tree models is that they allow you to solve fixpoint equations, and so are useful in the semantics of programming languages. Which might point to the concrete influence of Strachey in his choice of research goals, rather than a high-level matter of perspective. $\endgroup$
    – Charles Stewart
    Commented Mar 1, 2010 at 14:53
  • 1
    $\begingroup$ There's also the philosophical angle, in that the asymmetry of observability of termination induces the Sierpinski topology on the 2-point space. A great deal of basic domain theory can be derived from that intuition. $\endgroup$
    – Neel Krishnaswami
    Commented Mar 1, 2010 at 15:19
  • 3
    $\begingroup$ Professor Scott always mentions Strachey when he speaks about the history of domain theory. $\endgroup$
    – Andrej Bauer
    Commented Mar 1, 2010 at 22:15
  • $\begingroup$ At 35:49 in LogicLounge with Dana S. Scott, there is an interesting comment about the story behind denotational semantics for the lambda calculus: youtu.be/nhc94A829qI?t=35m49s $\endgroup$
    – Anton Salikhmetov
    Commented Jun 21, 2018 at 14:07
6
$\begingroup$

Not exactly λ-calculus, but untyped formalisms in general. Here is an excerpt from the introduction of A type-theoretical alternative to ISWIM, CUCH, OWHY (bold emphasis is mine):

No matter how much wishful thinking we do, the theory of types is here to stay. There is no other way to make sense of the foundations of mathematics. Russell (with the help of Ramsey) had the right idea, and Curry and Quine are very lucky that their unmotivated formalistic systems are not inconsistent. <...> My point is that formalism without eventual interpretation is in the end useless. Now, it may turn out that a system such as the λ-calculus will have an interpretation along standard lines (and I have spent more days than I care to remember trying to find one), but until it is produced I would like to argue that its purposes can just as well be fulfilled by a system involving types. <...>

Both the introduction and the preface to this paper are very interesting to read as they somewhat explain Scott’s feelings towards typed vs. untyped systems and contain some nice bits of history.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .