1

 Susumu Hayashi, Nov. 23, 2002
 ALT/DS ~{!/~}02, L~{(9~}beck, Germany

2

 The results presented in the talk are join work with the following calibrators:
Y. Akama, S. Berardi, H. Ishihara, U.Kohlenbach, M. Nakata, T.
Yamazaki, M. Yasugi

3

 The paper in the proceedings contain considerable number of typos.
Correction would be on my LCM web page at http://www.shayashi.jp very
soon

4

 Computational Learning Theory is
mathematical investigations of learning.
 In this talk, I will present
LCM: LimitComputable Mathematics
a mathematics based on computational learning theory, more
exactly, based on inductive inference.

5

 MNP (Minimal Number Principle):
Let f be a function form Nat to Nat. Then, there is xÎNat such that
f(x) is the smallest value among
f(0), f(1), f(2),~{!~}
 $xÎNat."yÎNat.f(x)£f(y)
 Nat : the set of natural numbers

6

 Let x,yÎNat and f:Nat®Nat.
 LCMsemantics of $y.A(x,f,y)
is
 There is a machine M taking x and the first n data of f: (0,f(0)),
(1,f(1)),~{!~},
(n1,f(n1)) and outputs its guess y_{n}
 The guesses y_{0}, y_{1},~{!~} converges to a value y_{¥} in Gold~{!/~}s sense
 A(x,f,y_{¥}) holds in
LCMsemantics

7

 Regard the function f as an
input stream
(0,f(0)), (1,f(1)),
(2,f(2)),~{!~} for M
 M is the inductive inference machine taking the first n elements of the
stream and outputs the minimal x_{n} such that "y<n.f(x_{n})£f(y).
 The outputs (guesses) of the machine converges to the right answer of
MNP.

8

 LCM semantics of logical formulas are similarly defined for other cases
by means of inductive inference machines or in another word
limitcomputation. Thus, it is called LimitComputable Math.
 Details of the semantics are in the proceeding paper.

9

 The LCMsemantics of $y.A(x,f,y)
is different from the standard definition of inductive inference (from a
paper by Case and Suraj)
 Inductive inference
 Functions representable finitely, e.g., computable functions, are
infered from their finite segments.

10

 LCM
 Functions such as f in $y.A(x,f,y)
may be arbitrary functions without any finite representations
 The objects to be infered may not be the functions (or languages) to be
fed to the inductive inference machines

11

 LCMsemantics is much generalized from inductive inference
 It is about limitingrecursion (D^{0}_{2}stuffs in
recursion theory), but not all limitingrecursion stuffs are related to
learning
 Is it really useful to think the subject in the relation with learning
theory?
 My answer is YES.

12

 Inductive inference is formulated as the problem of Generalization, but
nongeneralization problem such as Classification (Wiehagen and Smith)
is also considered in COLT

13

 Studies of classification still assume finite representability of
entities, since the data are stored in a DB
 But, Web is now a kind of DB. It might be reasonable to think an entity
as a stream of data obtained from Web
 Isn~{!/~}t it better to modelize a registered customer at an eshop as a
noncomputational stream of interactions

14

 Similarities between the two areas
 The learning for MNP is ~{!0~}Learning by Erasing~{!1~} due to Jain and others.
 Resemblance between ~{!0~}learning of algebraic concepts~{!1~} by Stephan et al.
and LCM algebra.
 A relationship of LCM to Reverse Mathematics has been found, and it can
be explained a ~{!0~}game~{!1~} with a flavor of learning

15

 LCM framework is very general to the existing frameworks in Learning
theory
 However, it does not seem too general, as ~{!0~}thinking in learning theory~{!1~}
has been a great help for developments of LCM
 LCM might provide some ideas to Learning Theory in future

16

 The original motivation was Proof Animation technology, which aims to debug
(partially) formalized proofs with proof checkers.
 By chance, thank to A. Yamamoto, I could related it to learning theory.
 LCM is primarily for Proof Animation.

17

 Formal methods are becoming realistic but still costs of developments of
formal proofs are too huge for almost all commercial applications
 A difficulty is ~{!0~}wrong directed proof plan~{!1~}.
 Proof developments sometimes go into wrong directions due to
illformalized lemmas (subgoals) and definitions.
 An example~{!~}..

18


19

 The theorem holds for group A and B, since they have only n marbles.
All the marbles are of the same color, since they share an.

20

 This kind of situations happen in developments of formal proofs.
 Sometimes, we cannot even the theorem is wrong, when we are not very
familiar with concepts we defined for a particular software and hardware
systems. (Your formal definitions may not represent your informal
concepts!)

21

 We can see goals and definitions are wrong when we find that we cannot
prove the goals.
 However, realizing unprovability of goals after many fruitless trials is
awfully time consuming and exhausting.
 Is~{!/~}nt there any better way to find errors?

22


23

 If a proof is intuitionistic, namely does not use the principle of
excluded middle A or not A, a program which execute the proof is
automatically obtained. Actually, the example of marbles is
intuitionistic and, a skeleton of the applet could be automatically
generated.
 However, not for classical proofs using A or not A~{!~}.

24

 Restricted LEM (Law of Excluded Middle) are valid under LCMsemantics
 Then inductive inference machine could be used as the marble applet
 We cannot compute the final value, but we can debug LCMproofs by
inductive inference
 They do not cover all classical mathematics, but are enough for very
many theorems.

25

 The law of excluded middle and related principle of double negation
elimination can be restricted to S^{0}_{n}and P^{0}_{n}formulas.
They are called semiclassical principles
 Weak semiclassical principles correspond to inductive inference

26

 S^{0}_{n}LEM~{!!~}(Law of Excluded Middle):
A
or not A~{!!~}
for S^{0}_{n}formula A.
 Similarly for P^{0}_{n}LEM
 P^{0}_{1}LEM: "x.A or not "x.A,
 D^{0}_{n}LEM
~{!!~} (A ↔ B) ~{!z~} A or not
A
for S^{0}_{n}formula~{!!~}A and P^{0}_{n}formula~{!!~}B

27

 S^{0}_{n}DNE~{!!~}(Double Negation Elimination):
(not not A) ~{!z~}
A~{!!~}
for S^{0}_{n}formula~{!!~}A.
 S^{0}_{2}DNE:
not not $x."y.A~{!z~} $x."y.A
 P^{0}_{n}DNE is defined similarly

28


29

 Principles correspond to inductive inference:
 P^{0}_{1}LEM, S^{0}_{1}LEM, D^{0}_{2}LEM,
S^{0}_{2}DNE
 The others are strictly weaker or stronger than inductive inference
 Thus these are proper LCMprinciples

30

 The converse of arrows in the hierarchy of semiclassical principles are
conjectured not to be derivable in HA.
 The conjecture have been solved for n=1, 2 levels, which include all
principles corresponding to inductive inference and below.
 It is still open for the higher levels.

31

 We are now classifying mathematical theorems by means of these
principles.
 There are theorems exceeding the scope of LCM, like BolzanoWeierstrass
theorem, but many theorems of standard mathematics are in the scope of
LCM
 E.g. HeineBorel theorem, Completeness theorem of predicate logic,
etc.etc~{!~}.

32

 S. Simpson and his collaborators have shown that WKL is enough to prove
many mathematical theorems, although WKL is very weak from consistency
point of view.
 Weak König Lemma (WKL): any binary branching tree with infinite nodes
has an infinite path

33

 After sending the manuscript of the paper, stuffs on WKL have been much
improved. Even the formulation of LCMWKL has been changed. Now, it is
just as ordinary WKL!
 And the problem of learning theoretic model of WKL is nearly solved as I
will present soon

34

 The low basis theorem: the infinite paths could be of low degree. A
degree is low, if its jump is lower than the degree of halting problem.
 This fact suggests that WKL sits in between of limitingcomputation and
computation
 WKL actually sits in the expected place in our hierarchy

35


36

 Theorems provable constructively from WKL are animated by inductive
inference
 Many theorems in Reverse Mathematics are proved without or with very
weak classical reasoning, and we can transfer their proofs nearly
automatically into LCMproofs.
 An example: Completeness
theorem of the first order predicate logic.

37

 A semantics of intuitionistic WKL by Lifschitz and van Oosten gives a
pradigm of ~{!0~}learning by refutation~{!1~}
 This semantics is based on multivalued computation and developed for a
very different reason in 7090~{!/~}s.

38

 Let p_{1},~{!~},p_{n} be programs and let C_{1},~{!~},C_{n}
be corresponding P^{0}_{1}conditions (formulas)
guaranteeing ~{!0~}correctness~{!1~}
of the programs
 A finite set {(p_{1},C_{1}),~{!~},(p_{n},C_{n})}
represents the following set of values:
 _{ }{v_{i} 
v_{i} is the value of p_{i} and C_{i} holds}

39

 Assume that p_{1},~{!~},p_{n}_{ }are competing
scientists computing a scientific constant based on their own theories
represented by C_{1},~{!~},C_{n}
 Since theories C_{1},~{!~},C_{n} are P^{0}_{1},
they are refutable. If one guy is wrong, he will drop from the race
eventually
 If at most one remains, then we can effectively know who is correct
including none.

40

 A system of this representation of
multivalues gives an intrinsic semantics of WKL
 The proofs by WKL are easy to animate by this system of computation
 An interpretation with a flavor of learning is possible

41

 Since it is strictly below the proper LCM principles, it is not real
inductive inference
 However, the metaphor to Popper style competition by refutation helps
the understanding of proof of ~{!0~}the low basis theorem~{!1~} and proof
animation by the computation system

42

 It must be fruitful to investigate relationship of COLT and LCMlike mathematics
based on ~{!0~}learning~{!1~}.
 There are many interesting open problems. An example:
 Is there mathematics corresponding to other paradigm of learning theory
besides inductive inference? How about PAClearning?

43

 Hearty thanks to
 A.
Yamamoto, H. Arimura, J. Case, E. Martin, F. Stephan,
 I learned about COLT much through discussions with them
 Yamamoto helped me to start the entire field
