most recent 30 from http://mathoverflow.net 2013-06-19T22:33:57Z http://mathoverflow.net/feeds/question/16752 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/16752/scott-on-the-consistency-of-the-lambda-calculus Charles Stewart 2010-03-01T11:33:22Z 2010-03-01T12:43:59Z

<p>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.</p> <p>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.</p>

http://mathoverflow.net/questions/16752/scott-on-the-consistency-of-the-lambda-calculus/16754#16754 Andrej Bauer 2010-03-01T12:43:59Z 2010-03-01T12:43:59Z

<p>You could ask <a href="http://www.cs.cmu.edu/~scott/" rel="nofollow">him</a> 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.</p> <p>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.</p>