Computability Beyond Church-Turing via Choice Sequences

Authors: Liron Cohen, Vincent Rahli, Mark Bickford and Robert Constable

Paper Information

Title:Computability Beyond Church-Turing via Choice Sequences
Authors:Liron Cohen, Vincent Rahli, Mark Bickford and Robert Constable
Proceedings:LICS PDF files
Editors: Anuj Dawar and Erich Grädel
Keywords:Choice sequences, Non-lawlike computability, Type theory, Nuprl proof assistant, Beth models, Digital libraries

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 modi cations to the under- lying type theory. 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.

Talk:Jul 11 12:00 (Session 64E)