Jonathan Gallagher

Date: August 11, 2017
Time: 12:00 am - 12:00 am
Location: ICT616

Title: Scott, Koymans, and Beyond
Dana Scott, in “Relating theories of the lambda calculus” sought to show that the same techniques for modelling the simply typed lambda calculus can be used to model the untyped lambda calculus. He essentially constructed an adjunction between lambda theories T and cartesian closed categories X with a chosen reflexive object U:
CL(T) —> (X,U)
T —> Th(X,U)
with the property that
Th(CL(T)) \simeq T
In other words, every lambda theory T has a model M, whose theory is equivalent to T. This is now called the Scott-Koymans theorem.
In this talk, we will give a modern presentation of the classifying category of a lambda theory, and the theory of a model, using Turing categories with an extra property called canonical codes (or perhaps latently closed), and use this to reconstruct the Scott-Koymans theorem.
Footnote: Koymans’ contribution was to characterize the difference between lambda-algebras and lambda-models. One can make a subtle mistake about substitutional properties when interpreting into points via a pseudostructure on X(1,U). Koymans’ contribution is vital, but we will steer around issues with points.