Abstract
In this article we study Gödel's functional interpretation from the perspective of learning. We define the notion of a learning algorithm, and show that intuitive realizers of the functional interpretation of both induction and various comprehension schemas can be given in terms of these algorithms. In the case of arithmetical comprehension, we clarify how our learning realizers compare to those obtained traditionally using bar recursion, demonstrating that bar recursive interpretations of comprehension correspond to 'forgetful' learning algorithms. The main purpose of this work is to gain a deeper insight into the semantics of programs extracted using the functional interpretation. However, in doing so we also aim to better understand how it relates to other interpretations of classical logic for which the notion of learning is inbuilt, such as Hilbert's epsilon calculus or the more recent learning-based realizability interpretations of Aschieri and Berardi.
Original language | English |
---|---|
Title of host publication | LICS ’16: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science |
Publisher | Association for Computing Machinery |
Pages | 136-145 |
ISBN (Print) | 9781450343916 |
DOIs | |
Publication status | Published - 2016 |
Event | the 31st Annual ACM/IEEE Symposium - New York, NY, USA Duration: 5 Jul 2016 → 8 Jul 2016 |
Conference
Conference | the 31st Annual ACM/IEEE Symposium |
---|---|
Period | 5/07/16 → 8/07/16 |
Fingerprint
Dive into the research topics of 'Gödel's functional interpretation and the concept of learning'. Together they form a unique fingerprint.Profiles
-
Thomas Powell
- Department of Computer Science - Senior Lecturer
- Mathematical Foundations of Computation
Person: Research & Teaching