数理解析研究所講究録
1169 巻 2000 年 102-108

102

Formalized Mathematics, Proof Animation,and Limit Computable Mathematics
Susumu Hayashi*
Department of Computer and Systems Engineering,
Faculty of Engineering, Kobe University,
1-1 Rokko-dai, Nada, Kobe, Japan
July 19, 2000

1

Formal Proof Developments

Formalized mathematics or formal proof developments are activities to build
formal proofs checked on computers for applications to formal methods or its
own sake. Formal proof developments by proof-checkers, HOL, Coq, Mizar,
etc are becoIning realistic thanks to accumulation of proof libraries and withhelp of some high-tech efforts.
Bugs in softwares for some safety critical systems, such as traffic control
systems, medical devices, nuclear power stations, are very risky. Even bugsin ordinary commercial softwares and hardwares can cost much for users andfirms. Thus, formal methods, which is a technology for verifying correctnessof such systems, are used. Formal methods use some kind of formal logics
to verify these systems. Since human beings make errors, formal proofs onpapers may be incorrect. Thus, it is recommended to verify via formal proofson computers.
Formal methods are comparable with the activity of traditional appliedmathematics. In applied mathematics, real worlds are “formalized” by dif*Supported by No. 10480063, Monbusyo, Kaken-hi (the aid of Scientific Research, The
Ministry of Education)

103

ferential equations as formal methods describe the world by logical formulasof formal logics. Verifying softwares are comparable with solving differential

equations.

2

Proof Animation

Developments of formal proofs are costly and heavy tasks. We may compare
developments of formal proofs with finding exact solutions of differentialequations. Mathematicians solve differential equations numerically and guess
exact solutions by observing numerical solutions. This way of research isoften easier than guessing exact solutions by bare hands.
We have proposed proof animation [4], a methodology for proof developments, which is analogous to this activity. We “execute” proofs underdevelopments to find bugs in proofs just as programmers execute programs
under developments to find bugs in programs. This technology is expected
to make formal proof developments much easier.
“Executing proofs” means to follow proofs on examples as every mathematician does. Such an execution may be automatically done when proofs
are represented as data on computers. Actually, it is known that executionof proofs are possible, when proofs are constructive. A proof is constructive,
when the law of excluded middle is not used in the proof. The law of excluded
middle is the logical principle that every proposition is true or false: $A\vee\neg A$in symbol. There are some proof checkers which execute proofs. by the principle of “Curry-Howard” isomorphism or related concepts, e.g. realizabilityinterpretations [5].
However, these proof checkers may not be very useful for proof animations, since majority of proofs are non-constructive. In mathematics, classicallogic is freely used. Restricting logic to constructive fragments are not very
natural form the standpoint of ordinary mathematics. For example, it is
not allowed to say that 0123456789 appears in the expansion of or not.
Existence proofs by contradiction is basically non-constructive. Thus, even
if you can prove that it is contradictory that 0123456789 does not appear in
the expansion of , you cannot conclude that 0123456789 appears.
Many mathematical propositions in computer science are constructive.
However, there are some important propositions on concurrent processing
and combinatorics for which non-constructive arguments are much more nat$\pi$$\pi$

104ural.
, an extension of Curry-Howard isomorphism was found by
In the late
Tim Griffin. He extended Curry-Howard isomorphism to classical logic andprograms with continuation, which is a control mechanism used in functional
programming languages.
After his work, number of theories aiming to bridge classical proofs andprograms have been proposed. However, none of them looked fine for proof
animation. Curry-Howard isomorphism is a rather straightforward correspondence. It is not difficult to predict outlines of programs associated toformal proofs. By such a correspondence, we can locate bugs in proofs fromthe location of bugs of programs associated.
However, the new Curry-Howard isomorphisms for classical logic did notprovide such correspondences. The programs associated to standard proofs
their behavior are extremely complicated and difficult to understand.
Since proof animation is a mean to understand proofs via observations of
the behaviors of programs associated, these theories are not good enough for
proof animation.
It should be noted that these theories can be practical for other aims. Forexample, some implementations of -calculus, which is one of such calculi
associated to classical logic, show that it is good for a kernel of functional
languages with continuation.
Although, these works look hopeless for proof animation, Berardi’s theoryof approximation theory was an exception. Unlike to the other theories, it wasaimed to understand computational contents of actual proofs. By his theory,
Berardi gave an interesting computational meaning to a classical proof of thefollowing theorem:$80’ \mathrm{s}$$\mathrm{a}\mathrm{n}\mathrm{d}/\mathrm{o}\mathrm{r}$$\lambda\mu$$\forall f\in Natarrow Nat.\exists n\in.\forall x\in Nat.f(n)\leq f(x)$The “algorithm” which Berardi associated was an algorithmic process“guessing” the solution. It is described as follows:

Regard the function as a stream $f(1),$ $f(2),$ $f(3),$ . Have abox of a Natnumber. Put $f(1)$ in the box. Compare the contentof the box with the next element of the stream. If the new one
is smaller than the number in your box, put the new one in thebox. Repeat it infinitely.
$f$$\cdots$

105

In what sense the algorithm compute the answer? The process does notstop and we will never know when we should stop. However, the box will
eventually contain the correct answer. Once the box contains the correct
answer, then the content will never been changed. In this sense, this nonterminating process computes the right answer in the limit.
This kind of “limit process” is used as a model of learning by Gold [3]and Putnum [?]. The value of a limit $\lim_{t}f(t)$ is defined by the condition“there is $N$ such that $f(N+i)=v$ for all $i\in Nat.$ If $f(x)= \lim_{t}g(x, t)$holds for a recursive function , then is called limiting recursive. We may
think the sequence $g(x, 1),$ $g(x, 2),$is a trace of guessing the value of $f(x)$on a discrete time $t=1,2,$ .
Berardi’s interpretation uses infinitary proof figures and higher orderfunctional etc. and so was not really intuitive. He extracted the algorithm
above from a standard classical proof of the proposition. However, he did notgive an algorithm by which one can extract the algorithm explained above.
The algorithm was obtained by an analysis of his interpretation and was not
given directly from the interpretation.
$v$$f$$g$$\cdots$,$\cdots$

3

Limit Computable Mathematics

We have found that Berardi’s idea of utilizing limiting function as a kindof execution of classical proofs enables direct interpretation of a fragment ofclassical logic. The fragment is obtained by restricting the law of excluded.
middle (LEM) to-LEM, coincides with E. Bishop’s “theThis restricted form of LEM,
limited principle of omni-science.” It is essentially the algorithm explained
above, i.e.
-LEM maintains that we may know if $nf(n)=0$ holds for allor there is a counterexample for $f(n)=0$ . For example, we may conclude
123456789123456789 appears in the decimal expansion of or not byLEM.
E. Bishop wrote in his monograph of constructive analysis [2], if -LEM
(the limited principle of omniscience in his terminology) is allowed, “theoremafter theorem of classical mathematics” can be proved. The examples hegave were the ergodic theorem, the Hahn-Banach theorem, the fixed-pointtheorems, etc. We also found that D. Hilbert’s early work on invariant theoryis also proved by the principle.
$\cdot$$\Sigma_{1^{-}}^{0}\mathrm{f}\mathrm{o}\mathrm{r}\mathrm{m}\mathrm{u}\mathrm{l}\mathrm{a}\mathrm{s}$$\Sigma_{1}^{0}$$\Sigma_{1}^{0}$$n$$\Sigma_{1^{-}}^{0}$$\pi$$\Sigma_{1}^{0}$106

Thus, we conjecture that

Limit Computable Mathematics (LCM) would cover a large partof practical classical mathematics, e.g., mathematics for theoretical computer science (theory of algorithms), applied mathematics, and mathematics before pure abstract mathematics of 20thcentury.
From theoretical point of view, extracting “semi-algorithms” from constructive proofs by -LEM is fairy simple. We simply replace recursivefunctions in Kleene’s realizability interpretation with limit-recursive functions. Then everything works just as it was. This is because of “limiting
computable calculus” is also a “computable calculus”. For example, if a“limit” of computational structure -BRFT is again -BRFT. -BRFT isknown as one of the most general framework for recursion theory [7].
$\Sigma_{1}^{0}$$\omega$

4$\omega$$\omega$

Hilbert’s invariant theory: a target for case
study

There are several interesting targets of case studies of proof animation byLCM. From computer science and related finite mathematics, concurrent
algorithms, e.g. Dekker algorithm, and some combinatorial principles, e.g.
Higman’s lemma, look interesting. From works by Herbelin and Coquand,
we suspect that ordinary classical proof of Higman’s lemma might be beyondof feasible LCM.
From mathematics, Hilbert’s invariant theory in the late 19th century
seems most interesting. In his 1890 paper, Hilbert proved a theorem called“finite basis theorem”. (He called it “general finiteness theorem”.) In hisformulation, it read thatis a stream (sequence) of forms (homogeneous polyIfnomials) with a fixed number of variables, then there is $m$ suchis denoted as $A_{1}F_{1}+A_{2}F_{2}+\cdots+A_{m}F_{m}$ by somethat every.
forms$F_{1},$$F_{2},$$\cdots$$F_{i}$$A_{1},$ $A_{2},$$\cdots,$$A_{m}$, as far as theNote that $m$ is limiting recursive in the stream
theorem holds. We can just “search” such $m$ by try-and-error process. (If$F_{1},$$F_{2},$$\cdots$

107
we find there iswhich cannot be represented in the form, we increment
so that $m\geq i$ . This can be seen as an animation of the statement of thetheorem. However, this is not the thing we should do.
We are planning to animate Hilbert’s proof rather than the statement ofthe theorem. We have analyzed Hilbert’s proof and found that the proof uses
only -LEM. This may be interesting, since the proof is known as one of
the first transcendental proofs in algebra. Hilbert solved the long standing“Gordan’s problem” once and for all by this simple lemma. Then Gordan issaid to reply that “It’s not a mathematics but a theology” [9].
Hilbert proved the theorem by induction on the number of variables. For
the base case, the stream
ispointed outthat the “basis” is given by a single formula, whereis the smallest
number of the degree of the forms. This is the same algorithm as
Berardi’s.
After giving the proof of the base case, he gave an interesting specificproof for the case of two variables, and then proved the general induction
step again by -LEM. These proofs for the cases of two or more variables
contain several applications of -LEM. It is not very difficult to read its
computable contents intuitively from the proofs. Each instance of -LEM
generates its own guessing sequence of a series of algebraic forms or so. Since
our realizability interpretation merge all “local time” in a global time, theextracted term by the interpretation might not be good to understand thecomputable content. The algorithm read intuitively from Hilbert’s proof
suggest that there are some complicated interactions between these instancesof -LEM. Thus, for “legible” proof animaiton, the algorithm would haveto be presented in a network of some basic guessing functions corresponding
to -LEM.
We are now planning to formalize Hilbert’s invariant theory including hisfinite basis theorem via Coq proof checker and extract limiting algorithms
from its proofs.
$F_{i}$$m$$\Sigma_{1}^{0}$$F_{1},$ $F_{2},$$c_{1}x^{i_{1}},$ $c_{2}x^{i_{2}},$$\cdots$$c_{m}x^{i_{m}}$$i_{1},$$i_{2},$$\cdots.\mathrm{H}\mathrm{i}\mathrm{l}\mathrm{b}\mathrm{e}\mathrm{r}\mathrm{t}$$i_{m}$$\cdots$$\Sigma_{1}^{0}$$\Sigma_{1}^{0}$$\Sigma_{1}^{0}$$\Sigma_{1}^{0}$$\Sigma_{1}^{0}$References[1] S. Baratella and S. Berardi, Constructivization via Approximations andExamples, Theories of Types and Proofs, M. Takahashi, M. Okada andM. Dezani-Ciancaglini eds., MSJ Memories Vol. 2, pp.177-205.

108[2] E. Bishop, Foundations of Constructive Mathematics,$\mathrm{M}\mathrm{c}\mathrm{G}\mathrm{r}\mathrm{a}\mathrm{w}$-Hill, 1970.

[3] E. M. Gold, Limiting Recursion, The Journal of Symbolic Logic, 30(1965), pp.28-48.
[4] S. Hayashi, R. Sumitomo and K. Shii, Towards Animation of Proofs
testing proofs by examples-, Theoretical Computer Science, to appear.

-[5] S. Hayashi and H. Nakano, PX: A Computational Logic, (The MIT Press,1988)[6] S. C. Kleene, On the interpretation of intuitionistic number theory, The
Journal of Symbolic Logic, 10 (1945), pp.109-124.

[7] P. G. Odifreddi, Classical Recursion Theory, North-Holland.
[8] H. Putnam, Trial and Error Predicates and the Solution to a Problem ofMostowski, The Journal of Symbolic Logic, 30 (1965), pp.49-57.

[9] C. Reid, Hilbert, Springer-Verlag, New York, 1996
[10] A. S. Troelstra and D. van Dalen, Constructivism In Mathematics, Vol.
I and II, North-Holland.