## Abstract

It is well-known that the Gödel's system T definable functions (N→N)→N are continuous, and that their restrictions from the Baire type (N→N) to the Cantor type (N→2) are uniformly continuous. We offer a new, relatively short and self-contained proof. The main technical idea is a concrete notion of generic element that doesn't rely on forcing, Kripke semantics or sheaves, which seems to be related to generic effects in programming. The proof uses standard techniques from programming language semantics, such as dialogues, monads, and logical relations. We write this proof in intensional Martin-Löf type theory (MLTT) from scratch, in Agda notation. Because MLTT has a computational interpretation and Agda can be seen as a programming language, we can run our proof to compute moduli of (uniform) continuity of T-definable functions.

Original language | English |
---|---|

Pages (from-to) | 119-141 |

Number of pages | 23 |

Journal | Electronic Notes in Theoretical Computer Science |

Volume | 298 |

DOIs | |

Publication status | Published - 4 Nov 2013 |

## Keywords

- Agda
- Baire space
- Cantor space
- continuity
- dialogue
- Gödel's system T
- intensional Martin-Löf theory
- logical relation
- semantics
- uniform continuity

## ASJC Scopus subject areas

- Theoretical Computer Science
- General Computer Science