PA/LCM Home Page

We no longer look upon a deductive system as one that establishes the truth of its theorems by deducing them from 'axioms' whose truth is quite certain (or self-evident, or beyond doubt); rather, we consider a deductive system as one that allows us to argue its various assumptions rationally and critically, by systematically working out their consequences. Deduction is not used merely for purposes of proving conclusions; rather, it is used as an instrument of rational criticism. (Karl Popper, Realism and the Aim of Science, Part I, Chapter 4.)

what's new

What's PA/LCM

Ideas

To test formalization of proofs by experiments (animation) via Gold's limiting recursive functions. The goal is making proof developments on computers easier, friendly and less costly. Nonetheless, it raises surprisingly many interesting theoretical questions and bridges various areas of computer science and mathematics. It is also expected as a tool of CAI of mathematics to teach students "proofs are graphical and dynamic beings, and fun!".

PA: Proof Animation

Formal proof has been subject to formal inference rules. Or it is the very definition of formal proofs. Proof Animaiton changes this tradition. We propose to utilize Curry-Howard isomorphism to test formal proofs, which may be unfinished incomplete proofs. It is used to find bugs of proofs under development and even of proofs fully checked. In the latter, bugs may exist in formalization (definitions and theorems) itself, even if applications of inference rules are checked to be correct. (Such bugs have been reported in literatures of formal methods, especially, of hardware verification.) Since this resembles the animation of specifications in formal methods, we call it "Proof Animation."

LCM: Limit Computable Mathematics

When the project was started, the main difficulty of PA is that we did not know how to animate classical proofs. After examinations of various theories, we finally arrived the conclusions

The idea of LCM unexpectedly came from a study of history of mathematics. An origin of modern abstract algebra, Hilbert's finite basis theorem in the 1890's, looked similar to an example of proof execution by S. Berardi. A. Yamamoto pointed out that both of them are the same as limiting recurison in the learning theory. Then, Hayashi conceieved the idea. After starting the basic theory of LCM, it turned out that it is related to various areaas of computer scinece, mathematics and logic. See Hayashi S, and Nakata M.: Towards Limit Computable Mathematics below for more detailed discussions.

I tried to put all of my thoughts on LCM obtained so far. However, there remained some ideas still immature to be spelled out in definite words and so not included in it. Some of them are "connection of LCM to methods in applied mathematics in the traditional sense such as numerical analysis" and "computation as an interaction between machine and human being: motto machines compute and human beings decide when the machines stop", and relations to category theory.

The ultimate goal

As UML is emerging as a standard language for OO methods, formal or semi-formal languages and methods are now becoming practical and very important. I guess that, in a near future, formal language would become a very important factor of societies. Then, it becomes very important to understand how and how far we can describe real worlds by such languages. We must understand the gaps between formal entities and informal entities, and how we can relate them. Goedel's incompletness theorem is a mathematical theorem of such a kind. However, what really important is to understand the gaps from practical point of views. We cannot make a space craft traveling beyond the speed of the light by Einstein's theory. Incompletness by Goedel's theorem is a limitation of such a kind. But, real difficulty of building space crafts is not the limitation, since our space crafts are much slower and human-factors are much more important. Space crafts must carry us! Goedel's theorem gives us an undecidable proposition. However, real difficulty of formalization of systems lie elsewhere. We have just started to understand the gaps from realistic point of views.

The ultimate goal of my research is to understand how far and how we can describe the world by man-made languages in pracitical senses. This would be a deep question as philosophers ask. Kripke's "Wittgenstein's paradox" is an example of such questions asked by philosophers. Computer scientists and logicians may attack the problem from more practical sides and I believe that, without such a practice-oriented researches, we will never understand the real nature of the problem. PA is an example of a general framework bridging formal entities and informal entities. Specification animation, algorithm (program) animation, visualization, modelling, simulation, verification, validiation, conformance tests, etc.etc.. are technologies of the similar kinds. LCM not only realizes PA but may hopefully also birdge formalization of discrete systems by formal languages in our sense and more traditional "formalization" of continuous systems by more traditional "formal language" of calculus and classical physics such as differential equations.

What's going on

Here I list our activities. This is for publisizing the project and sharing informations between project members.

Literatures on LCM, PA and related subjects

  1. Akama, Y., Berardi, S., Hayashi, S., Kohlenbach, U.: An arithmetical hierarchy of the law of excluded middle and related principles,LICS 2004: 192-201. pdf (cautions: not the final version, there are some small errors... I do not know if it is legal to put the final verison here.)
  2. Akama, Y.: Limiting Partial Combinatory Algebras Towards Infinitary Lambda-calculi and Classical Logic, to appear In Proc. of Computer Science Logic, Lecture Notes in Computer Science, Springer, 2001, A theory of limiting PCA's. Akama's limit construction is more elaborated than Hayashi-Nakata's, and a fine mathematical theory has been developed. Akama tries to make limit-models as a semantics of concurrent processes, Available at http://www.math.tohoku.ac.jp/~akama/lcm/
  3. Berardi S.: Classical logic as Limit Completion I, a constructive model for non-recursive maps, Manuscript, Jan. 2001,Berardi introduced a new version of his approximation theory based on limit-idea. It utilizes limits over directed sets. He tries to make his theory as a sematics of concurrent processes. Available at http://www.di.unito.it/~stefano/Berardi-ClassicalLogicAsLimit-I.rtf: updated on May 24, 2001, section 1 and appendix are still drafts.
  4. Berardi,S, Coquand, Th., and Hayashi, S.: Games with 1-backtracking. GALOP 2005: 210-225
  5. Brattka, V.: Effective Borel Measurability and Reducibility of Functions, A talk at Kyoto Sangyo University, October 2003. Supported by LCM project. This talk give an interesting developments of discontinuous function theory in computable analysis. This would be a good target for calibration. A full paper version. The final version will appear in MLQ.
  6. Hayashi S., Sumitomo R., and Shii K.:Towards Animation of Proofs -testing proofs by examples- ps , dvi :, Theoretical Computer Science, 272, pp.177--195: The position paper of PA, It discusses the idea of PA. This is a papter written before the idea of LCM, but published after the idea of LCM. It took 3 years or so to be published! Thus, it is somehow "old-fashinoned", but still it is the best paper to know the idea of Proof Animation.
  7. Hayashi S. and Sumitomo R.; Testing Proofs by Examples, in Advances in Computing Science, Asian '98 : 4th Asian Computing Science Conference, Manila, the Philippines, December 1998, J. Xiang and A. Ohori, eds., Lecture notes in Computer Sciences No. 1538, pp.1-3, 1998, ps, pdf
  8. Hayashi S, and Nakata M.: Towards Limit Computable Mathematics, in Types for Proofs and Programs, International Workshop, TYPES 2000, Durham, UK, December 2000, Selected Paper, P. Challanghan, Z. Luo, J. McKinna, R. Pollack, eds., Springer Lecture Notes in Computer Science 2277, pp.125-144 : The position paper of LCM. It contains a plenty of open problems. Contents: The notion of PA and LCM. Illustrations of PA constructive or non-constructive by some examples. Shoratge of existing theory of classical proof execution for PA. LCM serves as a good foundation. A formalization of LCM by realizability and semi-classical principles. Relationships to various fields of computer science, mathematics and logic, including recursive degree, learning theory, computability of discontinuous functions, BSS theory of computational complexity over reals, Hilbert invariant theory, and a kind of reverse mathematics, etc.etc.. Some practical issues, e.g., a good calculus of limiting computable processes, and formal languages for proof checker-proof executor for LCM.
  9. Hayashi S, and Nakatogawa K.: Hilbert and Computation pdf (an early version of the first chapter of a paper in preparation), It was a handout for a talk at Hilbert workshop Jan. 2002 at Keio Universtiy, (html, pdf versions of PPT slides for the talk). Although the subject is history of science on Hilbert's early conception of computation, the LCM research was initiated by the the investigation of history. The relationships between classical logic, learning theory, proof animation, algebra were conceived through Hilbert's proof method used in his finite basis theorem, which was accused as "theology" by Paul Gordan. History of science is a great source of ideas of our research, as old mathematical articles are sources of algorithms for the computer algebra circle. Hibert invariant theory is our main target of PA/LCM case study. The research mainly foucuses on pre-1920's. Since Mancosu and Zach have studied Hilbert's and his pupils' notions of computation, e.g., Zach has shown that they were already beyond RCA_0 even in early 1920's, Mancosu suggested that their researches and our research complementary to each other and would have serve a complete picture of Hilbert's notion of computation.
  10. Hayashi S.: Limit Computable Mathematics and Interactive Computation, dvi, ps, pdf: An introduction to LCM and a paradiagm of interactive computation (early draft).
  11. Hayashi S.: Mathematics based on Learning, Algorithmic Learning Theory, LNAI 2533, Springer, pp.7-21: Largely introductory account of LCM for learning theory audiences. Addendum and Errata to the paper. 2002
  12. Hayashi, S.:Mathematics based on Incremental Learning -Excluded middle and Inductive inference-, a preliminary version. submitted to TCS, 2003, revised in 2004.
  13. Hayashi, S.:Can Poofs be Animated by Games?,inTyped Lambda Calculi and Applications: 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005. Proceedings, Editors: P. Urzyczyn, Springer LNCS No.3461, pp.11-22. pdf
  14. Kohlenbach U.: Unpublished handwritten notes commented and typesetted by Mariko Yasugi, Nov., 2000, Existence of hierarchy of semi-classical principles was proved for some constructive formal systems of arithemetics, HA, HA^omega, etc... dvi, ps, pdf.
  15. Nakata M. and Hayashi S,: A limiting first order realizability interpretation, Scientificae Mathematicae Japonicae http://www.jams.or.jp/scmjol/5.html, paper number 5-49: dvi, ps, pdf (caution, these are not the final version): This paper introduces realizability intepretation of a first order LCM-arithmetic by limiting computable functions and shows applications to proof animation. It also discuess some examples in details and speculations.
  16. Toftdal, M.: A Calibration of Ineffective Theorems of Analysis in a Hierarchy of Semi-Classical Logical Principles, ICALP 2004: 1188-1200.
  17. Toftdal, M.: Calibration of Ineffective Theorems of Analysis in a Constructive Context, Masterfs Thesis at Department of Computer Science, University of Aarhus, 17 May 2004,ps, pdf
  18. Yasugi M, Brattka V. and Washihara M.: Computability aspects of some discontinuous functions, "Computability of discontinuous functions over reals is considered from some point of views. Among them, they show that some typical discontinuous functions as Gasussian function are functions in the sense of LCM. Available at http://www.kyoto-su.ac.jp/~yasugi/recent.html
  19. M. Yasugi and M. Washihara, A note on Rademacher functions and computability, Words, Languages and Combinatorics III, World Scientific, 466-475, Computation by limit of the Rademacher function system.
  20. M. Yasugi and Y. Tsujii, Computability of a function with jumps-- Effective uniformity and limiting recursion-- to appear in Special Issue of "Topology and its Applications", Equivalence of limit computation and effective uniform space under certain condition.
  21. M. Yasugi and Y. Tsujii, Two notions of sequential computability of a function with jumps, Electronic Notes in Theoretical Computer Science 66 No.1 (2002), Preliminary version of 16.

Slides

Invited talks and an award

only invited talks at international meetings are listed. sorry for domestic meetings...

Finacial supports