1

 Susumu Hayashi
 Dec, 18, 2002
 SIGFAI, Fukuoka

2

 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.

3

 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

4

 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

5

 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.

6

 LCM semantics of logical formulas are similarly defined for other cases
by means of similar inductive inference machines.
 Thus, it is called LimitComputable Math.
 Details of the semantics are in ALT/DS 02 paper and other papers at
PA/LCM home page.

http://www.shayashi.jp/PALCM/

7

 Carl Smith pointed out LCM semantics is similar to ~{!0~}Logic of Discovery~{!1~}
(J. Bardins, R. Freivalds and C. Smith).
 Logic by Smith et al. is based on Tarski~{!/~}s semantics and learning is
involved only at the outmost level of truth definition.
 Ours are based on Kleene~{!/~}s semantics and learning process is involved at
the every level of truth definition.

8

 Ours are based on Kleene~{!/~}s semantics and learning process is involved at
the every level of truth definition.
 However, up to S^{0}_{2}level (the level classical
logic holds in LCM), they are pretty much similar.
 The notion of ~{!0~}expectation level~{!1~} might be helpful to bridge LCM and
computable analysis and numerical analysis.

9

 The LCMsemantics of $y.A(x,f,y)
is different from the standard definition of inductive inference
 Inductive inference
 Functions to be learned are finitely representable
 To be learned is the whole picture (representation etc.) of the
function

10

 LCM
 Functions such as f in $y.A(x,f,y)
may be arbitrary functions without any finite representations
 The object to be learned (infered) is any attribute related to the
function f

11

 According to Carl Smith~{!/~}s definition, our process is not learning but
discovery.
 Mathematics based on Discovery??
 Probably, it is better to call such a task ~{!0~}learning attributes~{!1~}.

12

 LCM have been related to Learning Theory in some nontrivial ways.
 Resemblance between ~{!0~}learning of algebraic concepts~{!1~} by Stephan et al.
and LCM algebra.
 The learning for MNP is ~{!0~}Learning by Erasing~{!1~} due to Jain and others.
 A relationship of LCM to Reverse Mathematics can be explained by a
learning theoretic ~{!0~}Popperian race~{!1~}

13

 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.

14

 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~{!~}..

15


16

 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.

17

 This kind of situations happen in developments of formal proofs.
 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.
 Isn~{!/~}t there any easier way to find errors?

18


19

 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~{!~}.

20

 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.

21

 Logical of LCM depend on realizability semantics used, e.g., modified
realizability and Kleene realizability~{!~}.
 Thus they differ from versions to versions.
 However, they have common characteristics:
 semiclassical principles
hold

22

 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

23

 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

24

 S^{0}_{n}LLPO~{!!~}(Lesser Limited Principles of
Omniscience):
(not (A and B)
)~{!z~} not A or not B
for S^{0}_{n}formula~{!!~}A, B.
 S^{0}_{1}LLPO: P, Q are recurive
 not ($x.not P and $x.not Q)
~{!z~} "x.P or "x.Q
 P^{0}_{n}LLPO is defined similarly

25


26

 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. Maybe~{!~}.
 The exact place of general LLPO is open. However, it is wellknown in
the lowest level, Sublearning Level.

27

 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

28

 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

29

 Bishop~{!/~}s LLPO (=our S^{0}_{1}LLPO) :
not (A and B) ~{!z~} not A
or not B
for A, B: S^{0}_{1}formulas
 WKL is constructively equivalent to LLPO plus the bounded countable
choice for P^{0}_{1}formula (decision making for
effectively refutable conditions).

30


31

 The underivability of P^{0}_{1}LEM is proved by three
different proofs:
 monotone functional interpretation (Kohlenbach)
 Standard realizability plus low degree model of WKL_{0 }(Berardi,
Hayashi, Yamazaki)
 Lifschitz realizability (Hayashi)

32

 Transfers from Reverse Mathematics to LCM
 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.
 This is not an coincidence. Reverse math. and LCM are deeply related.
(Next slide)

33

 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 initiated for a very
different reason in 70~{!/~}s, incidentally by a known AI researcher V.
Lifschitz, and studied by van Oosten in 90~{!/~}s.

34

 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}

35

 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.

36

 A system of this representation of
multivalues gives an intrinsic semantics of logic with WKL
 Existence of entity is interpreted as ~{!0~}an answer is in the multivalued
output, although I do not know which one it is~{!1~}.
 The proofs by WKL are easy to animate by this system of computation

37

 LCMconcepts corresponding to various learning theory concepts:
 What~{!/~}s positive data and negative data in LCM? (Question by Eric
Martin)
 Is there logic for PAClearning?: Probability of PAClearning seems to
corresponds to basis of topological space as expectation level of logic
of discovery.
 Relationship to computable and/or numerical analysis, Kohlenbach~{!/~}s work,
Arikawa et al~{!~}

38

 Relationship to geometry, recursion theory, Lsystem, fractal, etc.
etc~{!~}.
 The thesis
 Many scientific phenomena would be explained in the frame work of computable
generation and refutation, erasing
 Just as development of organic system by cell generation and apotosis

39


40

