*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.) **

- PA/LCM@stands for Proof Animation@and Limit Computable Mathematics

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!".

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."

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

- It is plausible that there is no such a method for full classical proofs.
- An idea from Learning Theory by Gold serves as a good tool of animation for a fragment of classical mathematics, we call it Limit Computable Mathematics.
- A majority of proofs for concrete and pracitical mathematics needs only LCM.

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.

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.

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

- 2001
- Some papers were written and published.

- A talk at The International Workshop on Rewriting in Proof and Computation (RPC'01), October 25-27.
- 2002
- Eric Martin visits Akihiro Yamamoto and LLLL Workshop at Sapporo with
him.
- First meeting with Learning theory circle in colllaboration with Ken Satoh's Kaken-hi project.
- RichProlog is expected to be an implementation language for LCM. A way of implementatin of LCM which we did not expect might be possible by RichProlog.

- Mini workshop with John Case in Kyoto.
- John Case, Akama, Arimura (left to right), Hayashi had discussions on LCM and Learning theory.
- Hayashi and Yasugi visit Kohlenbach at BRICS, Aarhus university, Denmark.
- Calibration of classical principles.
- Various discussions on proof theoretic sides of LCM and related subjects, mainly the ones done by Kohlenbach.
- Brain Storming Workshop at Kobe university (March 4,5,6) schedule for project members (in Japanese)
- S. Berardi visted Kyoto and Kobe in July.
- H. Barendregt visited Kobe in August.
- F. Stephan and E. Martin invited by Yamamoto's project are scheduled to visit Kobe in October.
- U. Kohlenbach invited by Yasugi's project is scheduled to visit Kyoto in December.
- The second LLLL Workshop organized as a part of SIGFAI of Japanese Society of Artificail Intelligence will be held in Hakata in December. http://www.i.kyushu-u.ac.jp/~arim/sigfai02/

- Eric Martin visits Akihiro Yamamoto and LLLL Workshop at Sapporo with
him.
- 2003
- Vasco Brattka visted Kyoto.
- Eric Martin visited Yamamoto at Kyoto University.
- The works by Brattka and Martin are both on Borel hierarchy. Borel hierarchy seems to correspond to LCM.
- I was rather lazy to maitain this page......

- 2004
- The LCM arithmetical hierarchy was finally worked out!!
- Toftdal did the first significant step in the practce of calibration theory in his master thesis work.
- Thierry Coquand, Stefano Berardi, and Hayashi jointly found a game semantics equivalent to LCM realizability. (The game semantics is defined only for prenex normal forms.) It turned out that it's equivalent to simple backtracking game considerd by Coquand before his JSL paper 1995. This must be a significance step for theory of LCM and practice for PA/LCM. A brief description is found in Hayashi's paper for ALT02 special issue of TCS.
- A paper on LCM arithmetical hierarchy by Akama, Berardi, Hayashi, Kohlenbach was accepted by LICS 2004.
- A paper on calibration theory by Toftdal was accepted by ICALP 2004.
- A Kakenhi-grant for "Logic of PAC-Learning" was approved.
- SMART project homepage started. The project is a practical UML-related project, but it is based on the same philosophy as of LCM.
- S. Berardi visited Japan in December. Slides of his talk at Kyoto university.
- The general concept of 1-backtracking game has been established by Berardi. His slides at Types meeting at Paris.

- 2005
- Berardi gave a talk on 1-backtracking semantics by Berardi, Coquand and Hayashi at Galop 05.
- Hayashi gave an invited talk on LCM and games at TLCA '05.

- 2006
- Berardi visited Tokyo and Kyoto in March. He is now working on very natural game semantics of implications. It is fully first-order and applicable to intuitionistic mathematics as well as LCM.

**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.)**Akama, Y.:**, 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/**Limiting Partial Combinatory Algebras Towards Infinitary Lambda-calculi and Classical Logic****Berardi S**.:, 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.*Classical logic as Limit Completion I, a constructive model for non-recursive maps***Berardi,S, Coquand, Th., and Hayashi, S.: Games with 1-backtracking**. GALOP 2005: 210-225**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.**Hayashi S., Sumitomo R., and Shii K.:**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.*Towards Animation of Proofs -testing proofs by examples*-**Hayashi S. and Sumitomo R.;**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*Testing Proofs by Examples*,**Hayashi S, and Nakata M.:**, 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.*Towards Limit Computable Mathematics***Hayashi S, and Nakatogawa K.:**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.*Hilbert and Computation***Hayashi S.:**dvi, ps, pdf: An introduction to LCM and a paradiagm of interactive computation (early draft).*Limit Computable Mathematics and Interactive Computation*,**Hayashi S.:**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*Mathematics based on Learning,***Hayashi, S.:Mathematics based on Incremental Learning -Excluded middle and Inductive inference-**, a preliminary version. submitted to TCS, 2003, revised in 2004.**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**Kohlenbach U**.:, 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.**Unpublished handwritten notes commented and typesetted by Mariko Yasugi****Nakata M. and Hayashi S,:**,*A limiting first order realizability interpretation***Toftdal, M.: A Calibration of Ineffective Theorems of Analysis in a Hierarchy of Semi-Classical Logical Principles**, ICALP 2004: 1188-1200.**Toftdal, M.:****Calibration of Ineffective Theorems of Analysis in a Constructive Context**, Masterfs Thesis at Department of Computer Science, University of Aarhus, 17 May 2004,ps, pdf**Yasugi M, Brattka V. and Washihara M**.:, "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**Computability aspects of some discontinuous functions****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.**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.**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.

- PowerPoint file for Asian98, Dec. 8, 98, Manila.
- PowerPoint file for PA workshop, Jan. 10,11, 00, Kyoto
- goishi.html, pa_example.jar: a HTML file linked from PPT files above and a jar file called from the html file.
- HTML version of PPT presentation for PA workshop
- PowerPoint file for CSL 02, Edinburgh, UK
- PowerPoint (HTML) file for ALT/DS 02, Luebeck, Germany
- PowerPoint (HTML) file for CCA-seminar, Kyoto and SIG-FAI(LLLL), Fukuoka
- PowerPoint file for Berardi's talk at LICS 2004, Truku, Finland
- PowerPoint file for Berardi's talk at Kyoto university, Dec, 2004.
- PowerPoint file for Berardi's talk at GALAP, April, 2005.
- PowerPoint file for Hayashi's talk at TLCA '05, May, 2005

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

- S. Hayashi and R. Sumitomo: Testing Proofs by Examples, invited talk at Asian Computing Science Conference '98, Dec. 8-10, 1998, Manila, Philipin
- S. Hayashi and M. Nakata: Proof Animation and Limit Computable Mathematics, invited talk at TYPES 2000 Annual Meeting, Dec, 2000, Durham, UK,
- Nakata was awarded JSSST Takahashi Award for his talk at JSSST 2000 (Japan Society of Software Science and Technology 2000). His talk is based on the paper and co-authored by Hayashi.
- Limit Computable Mathematics and Interactive Computation, Invited talk at The International Workshop on Rewriting in Proof and Computation (RPC'01), October 25-27, 2001, Itutsubashi-kaikan, Sendai, organized by Research Institute of Electrical Communication Tohoku University.
- S. Hayashi and K. Nakatogawa, Hilbert and Computation, Hilbert Workshop, Jan. 12, 2002, Keio University, Tokyo, organized by Dept. of Philosophy, Keio University, sponsored by Philosophy of Science Society, Japan, and Mita Philosophy Society.
- S. Hayashi and Y. Akama, Limit-Computable Mathematics and its Applications, invited talk at CSL'02 (Computer Science Logic 2002), Edinburgh, UK.
- S. Hayashi, ALT'02 (Algorithmic Learning Theory 2002), Lubeck, Germany, invited talk. (addendum and Errata to the paper)
- S. Hayashi, Can Proof be Animated by Games? at TLCA2005, May, Nara, Japan.

- 98: PA project started by a Kaken-hi grant of Ministry of Education. 1998-2000, Research leader: Susumu Hayashi
- 01: PA/LCM project started by a Kaken-hi grant. 2001-2003, Research leader: Susumu Hayashi
- 03: Awarded by a finacial support from Okawa foudations: 2003-2004, Research leader: Susumu Hayashi
- 04: PA/LCM (2004-2006) and SMART (2004-2005) projects are supported by Kaken-hi grant, Research leader: Susumu Hayashi
- 04: Logic of PAC Learning project by Kaken-hi grant, 2004-2006, Research leader: Susumu Hayashi
- 06: Proof animation by 1-games by Kaken-hi grant, 2006-2007. Research leader: Mariko Yasugi