| Autor: |
Xu, Chuangjie |
| Rok vydání: |
2019 |
| Předmět: |
|
| Zdroj: |
Logical Methods in Computer Science, Volume 16, Issue 1 (February 20, 2020) lmcs:5394 |
| Druh dokumentu: |
Working Paper |
| DOI: |
10.23638/LMCS-16(1:22)2020 |
| Popis: |
We give a new proof of the well-known fact that all functions $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$ which are definable in G\"odel's System T are continuous via a syntactic approach. Differing from the usual syntactic method, we firstly perform a translation of System T into itself in which natural numbers are translated to functions $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$. Then we inductively define a continuity predicate on the translated elements and show that the translation of any term in System T satisfies the continuity predicate. We obtain the desired result by relating terms and their translations via a parametrized logical relation. Our constructions and proofs have been formalized in the Agda proof assistant. Because Agda is also a programming language, we can execute our proof to compute moduli of continuity of T-definable functions. |
| Databáze: |
arXiv |
| Externí odkaz: |
|
