Computability beyond Church-Turing via choice sequences

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Authors

Colleges, School and Institutes

Abstract

Church-Turing computability was extended by Brouwer who considered non-lawlike computability in the form of free choice sequences. Those are essentially unbounded sequences whose elements are chosen freely, i.e. not subject to any law. In this work we develop a new type theory BITT, which is an extension of the type theory of the Nuprl proof assistant, that embeds the notion of choice sequences. Supporting the evolving, non-deterministic nature of these objects required major modifications to the underlying type theory. Even though the construction of a choice sequence is non-deterministic, once certain choices were made, they must remain consistent. To ensure this, BITT uses the underlying library as state and store choices as they are created. Another salient feature of BITT is that it uses a Beth-like semantics to account for the dynamic nature of choice sequences. We formally define BITT and use it to interpret and validate essential axioms governing choice sequences. These results provide a foundation for a fully intuitionistic version of Nuprl.

Details

Original languageEnglish
Title of host publicationLICS '18 Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science
Publication statusPublished - 9 Jul 2018
Event33rd Annual ACM/IEEE Symposium on Logic in Computer Science - Oxford, United Kingdom
Duration: 9 Jul 201812 Jul 2018

Conference

Conference33rd Annual ACM/IEEE Symposium on Logic in Computer Science
CountryUnited Kingdom
CityOxford
Period9/07/1812/07/18