Forcing, effects and continuity

Add to your list(s) Download to your calendar using vCal

• Martin Escardo, University of Birmingham
• Friday 03 August 2012, 16:00-17:00
• CS 217.

If you have a question about this talk, please contact Paul Levy.

A natural model of Gödel’s system T (simply typed lambda calculus with natural numbers and primitive recursion) is the full type hierarchy. The type of natural numbers is interpreted as the set N of natural numbers, function types are interpreted as sets of all functions. Every T-definable function f:(N->N)->N is continuous. Moreover, from any T-definition of f, one can algorithmically extract a T-definable function m:(N->N)->N such that the value of f at a sequence x:N->N depends only on the first m(x) positions of x. Such a function m is a so-called modulus of continuity of f.

One way of proving this is to use constructive “forcing” with a “generic” sequence N->N. I will develop this from the point of view of denotational semantics. With a Moggi-style semantics of system T for a suitable “dialogue” monad, the generic sequence amounts to a so-called generic effect. A logical relation between the “intended” set-theoretical model and the auxiliary monadic model gives the continuity result. I also implemented the construction and short proof in Agda.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• CS 217
• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.