Limit Computable Mathematics and Interactive Computation

Abstract

We are now investigating an "executable" fragment of classical mathematics for testing formal proofs to make formal proof developments less laborious. Several theories of execution of full classical proofs are known. In these theories, some kind of abstract values such as continuations, are necessary. It makes them illegible from computational point of view, although they are mathematically interesting. In contrast, we consider only a fragment of classical mathematics and give a simple and natural "computational" contents without such abstract values. The fragment appears to cover a rather large domain of practical mathematics. The point is that codes associated to proof by our method is not computable in Turing's sense, i.e., \Delta 0 1 , but "executable " in the sense of Gold's theory of machine learning, i.e., \Delta 0 2 . I will give a survey of this new executable mathematics LCM. I will also discuss a possible framework of "interactive computation" emerged from LCM research. ...