12 May 2017, Colloquium on Mathematical Logic, Martin Hyland
For its first 40 years the pure Lambda Calculus was studied as a syntactic system. There was no study of semantics in the sense in which e.g. one studies the (evident) semantics of the predicate calculus or possible worlds semantics for modal logic. When the first models were developed around 1970 the community of logicians seems not to have concerned itself much about what was meant. Specialists had esoteric definitions of lambda model and lambda algebra but most were satisfied by Scott's explanation: restricting to continuous functions one can find spaces isomorphic to their space of endofunctions and that gives models. Since then the question of what is a model has been revisited many times: by Barendregt in his magnum opus (with a different account in the two editions), by Meyer and by Scott around 1980 and by Freyd and Selinger in the mid 1990s. Scott does not offer a definition so much as a category theoretic characterisation but in all the other approaches an interpretation of the lambda calculus is an algebraic structure with a cruciall operation of application.
In this talk I shall argue for a quite different view: an interpretation of the lambda calculus is a semi-closed algebraic theory. The link with the older views is given by what I think of as the Fundamental Theorem of the Lambda Calculus: there is a correspondence between such Lambda Theories and models of the initial such Theory. The new view enables direct approaches to Scott's characterisation, to the connection with the combinatory logic and to Lambda Monoids as studied in Koyman's neglected 1984 thesis.