Continuity of gödel's system T definable functionals via effectful forcing

Research output: Contribution to journalArticlepeer-review

10 Citations (Scopus)

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 languageEnglish
Pages (from-to)119-141
Number of pages23
JournalElectronic Notes in Theoretical Computer Science
Volume298
DOIs
Publication statusPublished - 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
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Continuity of gödel's system T definable functionals via effectful forcing'. Together they form a unique fingerprint.

Cite this