Outline of a Mathematical Theory of Computation

Preview

I’ll present Dana Scott’s Outline of a Mathematical Theory of Computation.

Summary

We don’t want to just blindly trust that whatever the compiler spits out is the semantics of the input program—we need a mathematical system of semantics! This paper provides the abstractions to start building up mathematical definitions of languages.

Does self-application make sense in a mathematical semantics setting? That is, can we faithfully represent a term p such that p(p) is an okay thing to do? The answer of this paper is yes—it involves a lattice of approximations of values, and this gives us the ability to create the first mathematical model for the lambda calculus.

To make that model, we need to create a domain D such that D ≅ D → D. We need this so that every term can be applied to every other term (e.g., (λx.x x)(λx.x x)) ! We can approximate this by taking the limit of the equations D₀ = D, Dₙ₊₁ = Dₙ → Dₙ. This limit D∞ = D∞ → D∞ exists (and isn’t vacuous) by the machinery in the paper, and we have our first mathematical model!