Continuity of Gödelʼs System T Definable Functionals via Effectful Forcing
| Autor: | Martín Hötzel Escardó |
|---|---|
| Rok vydání: | 2013 |
| Předmět: |
Cantor space
General Computer Science Agda Semantics (computer science) Baire space intensional Martin-Löf theory Gödelʼs system T Theoretical Computer Science Interpretation (model theory) Computer Science::Logic in Computer Science semantics uniform continuity Mathematics computer.programming_language Discrete mathematics dialogue Forcing (recursion theory) logical relation continuity Algebra Uniform continuity TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Type theory TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Programming Languages Kripke semantics computer Computer Science(all) |
| Zdroj: | MFPS |
| ISSN: | 1571-0661 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect