Computability beyond Church-Turing via choice sequences

Mark Bickford, Liron Cohen, Robert L. Constable, Vincent Rahli

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

3 Citations (Scopus)
203 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationLICS '18 Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science
PublisherAssociation for Computing Machinery (ACM)
Number of pages10
ISBN (Print)978-1-4503-5583-4
Publication statusPublished - 9 Jul 2018
Event33rd Annual ACM/IEEE Symposium on Logic in Computer Science - Oxford, United Kingdom
Duration: 9 Jul 201812 Jul 2018


Conference33rd Annual ACM/IEEE Symposium on Logic in Computer Science
Country/TerritoryUnited Kingdom


Dive into the research topics of 'Computability beyond Church-Turing via choice sequences'. Together they form a unique fingerprint.

Cite this