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!".
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
- 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
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
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.
- Some papers were written and published.
- Eric Martin visits Akihiro Yamamoto and LLLL Workshop at Sapporo with
- 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
- Mini workshop with John Case in Kyoto.
- John Case, Akama,
Arimura (left to right), Hayashi had discussions on LCM and Learning
- Hayashi and Yasugi visit Kohlenbach at BRICS, Aarhus university, Denmark.
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
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/
- Calibration of classical principles.
- Various discussions on proof theoretic sides of LCM and related subjects,
mainly the ones done by Kohlenbach.
- 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......
- 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
- 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.
slides at Types meeting at Paris.
- Berardi gave a talk on 1-backtracking semantics by Berardi, Coquand
and Hayashi at Galop
- Hayashi gave an invited talk on LCM and games at TLCA '05.
- 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.
Literatures on LCM, PA and related subjects
- 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
- 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/
- 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.
- 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.
full paper version. The final version will appear in MLQ.
- 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.
- 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,
- 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.
- 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
- Hayashi S.: Limit Computable Mathematics and Interactive Computation,
dvi, ps, pdf:
An introduction to LCM and a paradiagm of interactive computation (early draft).
- 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
- 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.: 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,
- 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
- 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 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
- 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,
- PowerPoint file for PA workshop, Jan. 10,11, 00,
- goishi.html, pa_example.jar:
a HTML file linked from PPT files above and a jar file called from the html
- 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
file for Berardi's talk at LICS 2004, Truku, Finland
file for Berardi's talk at Kyoto university, Dec, 2004.
file for Berardi's talk at GALAP, April, 2005.
- PowerPoint file for Hayashi's talk at TLCA '05, May,
Invited talks and an award
only invited talks at international meetings are listed. sorry for domestic
- 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,
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
- 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