University of Birmingham > Talks@bham > Theoretical computer science seminar > Forcing, effects and continuity

Forcing, effects and continuity

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

  • UserMartin Escardo, University of Birmingham
  • ClockFriday 03 August 2012, 16:00-17:00
  • HouseCS 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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.