> (x/
>
:http://www.shayashi.jp/PALCM/:http://www.shayashi.jp/PALCM/~/0DTimes New Roman0z[ 0D3 00000 Roman0z[ 02 DArial00 Roman0z[ 00DArial Blackman0z[ 0"@DWingdingskman0z[ 0PD3 0fggskman0z[ 0`DSymbolgskman0z[ 0pD3 fggskman0z[ 0DCenturyskman0z[ 0C0.
@n?" dd@ @@``$
)
21aa
()
HH,,33>>
()
_
`
adehijGopqrstvwxz0e0e
A AV 8c8c
?1 d0u0@Ty2 NP'p<'pA)BCDE"0e@ @ABC DEEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abN E5% N E5% N F
5%
!"?N@ABC DEFFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abP33@8ST_5S ʚ; u8ʚ;g4JdJdz[ 0npp@<4dddd@ 0,<4!d!d@ 0,<4BdBd@ 0,___PPT10D3 000000z[ 02DArial000z[ 0
pp___PPT9
L$(?
%p2LimitComputable Mathematics and its Applications 31@%22 Susumu Hayashi & Yohji Akama
Sep, 22, 2002
CSL 02, Edinburgh, Scotland, UK"KZ.@ / "LCM: LimitComputable Mathematics #3 # Constructive mathematics is a mathematics based on D01functions, i.e. recursive functions.
In the same sense, LCM is a mathematics based on D02functions. 3AHH
@6@E3L3L3
D3@H /)The aim of the talk) The talk aims to present basic theoretical ideas of LCM and a little bit of the intended application as the motivation.
Thus, in this talk
THEORY
APPLICATION (Proof Animation)
although the original project was application oriented and still the motto is kept.L %T% K Why D02functions? (1)XG%N%N%F% D02functions are used as models of learning processes, and, in a sense, semicomputable.
The original and ultimate goal of LCM project is materialization of Proof Animation
Proof Animation is debugging of proofs.
See http://www.shayashi.jp/PALCM/ for details of Proof Animation.
" B BCJJGBB1BBB(BABBJ U
00*Why D02functions? (2)XG%N%N%F% 2The D02functions are expected to be useful for Proof Animation as learning theoretic algorithms were useful in E. Shapiro s Algorithmic Debugging of Prolog programs
Shapiro s debugger debugged Prolog programs, i.e. axiom systems in Horn logic.
In a similar vein, an LCM proof animator is expected to debug axiom systems and proofs of LCM logic, which is at least a super set of predicate constructive logic. PCCJJvBBBB.B 2An example of semicomputable learning process (1)3 MNP (Minimal Number Principle):Let f be a function form Nat to Nat. Then, there is n : Nat such that f(n) is the smallest value among f(0), f(1), f(2),& Nat : the set of natural numbersJ ! !!!!!!!!
!!!!!!!!!!!!!!!!!Je 7
2An example of semicomputable learning process (2)3 Such an n is not Turingcomputable from f.
However, the number n is obtained in finite time from f by a mechanical computation .
!!!!!!!!!! !$ A limitcomputation of n (1)$ Regard the function f as a stream f(0), f(1), f(2), &
Have a box of a natural number. We denote the content of the box by x.
$$$$$C$$$$$3 $A limitcomputation of n (2)$ Initialize the box by setting x=0.
Compare f(x) with the next element of the stream, say f(n). If the new one is smaller than f(x), then put n in the box. Otherwise, keep the old value in the box.
Repeat the last step forever.. )
M 3f+ + " b
A limitcomputation of n (3)$ DThe process does not stop. But your box will eventually contain the correct answer and after then the content x will never change.
In this sense, the nonterminating process computes the right answer in finite time.
You will have a right answer, but you will never know when you got it.z# 
7 [ G # A limitcomputation of n (4)$ By regarding the set of natural numbers as a discreate topology space, the process computing x is understood as the limit:
lim n ! " f(n) = x
Thus, E. M. Gold (1965, J.S.L.30) called it
x is computable in the limit >~ ! _''
'*'"''"''# $$$$3$$3$ Z H R )Limit computation as Learning process (1)*** 4In computational learning theory initiated by Gold, the infinite series f(0), f(1), f(2),& is regarded as guesses of a learner to learn the limit value.
b I'# 4.)Limit computation as Learning process (2)*** f is called a guessing function:
The learner is allowed to change his mind. A guessing function represents a history of his mind changes.
When the learner stops mind changes in finite time, it succeeded to learn the right value. Otherwise, it failed to learn.f! iz hz
Limit and recursive hierarchy Shoenfield s Limit Lemma
A function g is defined by g(x)=lim a1 lim a2 & .lim an f(a1,a2,& ,an,x)for a recursive function f, if and only if, g is a D0n+1function.
In this sense, single limit is the jump A : D0n ! D0n+1 in recursion theory.
: lFR
(A
%A A 2 Logic based on limitcomputable functions (1). As the D01functions are the recursive functions, D0nfunctions may be regarded as a generalized domain of computable functions.
For example, they satisfy axioms of some abstract recursion theory, e.g. BRFT by Strong & Wagner.h$A(A Logic based on limitcomputable functions (2). Semantics of constructive mathematics is given by realizability interpretations and type theories based on recursive functions.
Thus, when recursive functions are replaced by D0nfunctions, a new mathematics is created.:A*&2
Logic based on limitcomputable functions (3). For n=2, it is a mathematics based on limitcomputation or computational learning. It is LCM.
Note that limits in LCM are not nested.
We may regard LCM is a mathematics based on the single jump D0n ! D0n+1$H$u0E$E Formal semantics of LCM (1)% Existing formal semantics of LCM are given by limitfunction spaces and realizability interpretations or some interpretations similar.
The first and simplest one is Kleene realizability with limit partial functions with partial recursive guessing functions (Nakata & Hayashi)" ZH
P
[ 2,Formal semantics of LCM (2)% HLearning theoretic limits must be extended to higher order functions to interpret logical implication and etcetras. Some extensions are necessary even for practical application reasons as well.
E.g. Nakata & Hayashi used partial guessing functions , which are rarely used in learning theory.% %&j 3Formal semantics of LCM (3)% :Combinations of different approaches to limitfunctions plus different realizability interpretations (Kleene, modified, etc) make different semantics of LCM, e.g.,
Nakata & Hayashi already mentioned
Akama & Hayashi: limCCC and modified realizability
Berardi: A limit semantics based on limits over directed sets.: ZZ#sH
[
8 What kind of logic hold? Logical axioms and rules of LCM depend on these semantics just as modified realizability and Kleene realizability define different constructive logics.
However, they have common characteristics:
semiclassical principles hold0 #ZK
s '"S0n and P0nformulasvC'
'
''C'
'
' '
' S0nand P0nformulas are defined as the usual prenex normal forms.
Thus, S03formula is Exists x.ForAll y.Exists z.A
A definition not restricted to prenex form is possible but omitted here for simplicity. C!
!
!!!C!
!
!8!C%
%
%
X * , 3 Semiclassical principles (LEM) DS0nLEM0(Law of Excluded Middle): A or not A0for S0nformula0A.
Similarly for P0nLEM
D0nLEM0 (A ! B) ! A or not Afor S0nformula0A and P0nformula0B( C!
!
!&!
!!!C!
!
! !!!!C!
!
!!C!
!
!!!!"!"!"!"!"!
!!C!
!
! !!!!C!
!
! !! < % Semiclassical principles (DNE) PS0nDNE0(Double Negation Elimination): (not not A) ! A0for S0nformula0A.
P0nDNE is defined similarly
Note: S01DNE is Markov s principle for recursive predicates.T C!
!
!'!! !!"!!!C!
!
! !!!C!
!
! !C!
!
!3!2B ] ;4
Some examples' P01LEM ForAll x.A or not ForAll x.A
S01LEM Exists x.A or not Exists x.A
S02DNE not not Exists x.ForAll y.A ! Exists x.ForAll y.A
S03LEM Exists x.ForAll y.Exists z.A or not Exists x.ForAll y.Exists z.AF PC!
!
!C!
!
!C!
!
!4""C!
!
!O *
*Hierarchy of semiclassical principles (1)+ <5Important Remark (1) @If we allow function parameters in recursive formulas, then the hierarchy collapses with the help of the full principle of function definition ForAll x.Exists!y.A(x,y) ! Exists f.Forall x.A(x,f(x))
Because of the combination of these two iterate applications of limits.L!("It K =6Important Remark (2) We keep the function definition principle and forbid function parameters in recursive predicates.
We may introduce function parameters for recursive functions. )$LCM semiclassical principles !In all of the known semantics of LCM, the followings hold: P01LEM, S01LEM, S01DNE, P02DNE
In some semantics the followings also hold: D02LEM, S02DNE
These are LCMprinciples since interpretable by single limits. The principles beyond these need iterated limits, and so nonLCM.
4 ;GGGG+GG"@ 5 *Hierarchy of semiclassical principles (2)* The converse of arrows in the hierarchy of semiclassical principles are conjectured not to be derivable in HA.
If the scheme S0n DNE is not derivable from the scheme P0n LEM, then the conjecture is proved for the nlevel.
The conjecture have been solved for n=1, 2 levels, which include all of the LCM semiclassical principles. It is still open for the higher levels.
r PP~C
&C
,,E'"s "&What theorems are provable in LCM? (1)' Transfers from Reverse Mathematics:
If sets are identified with {0,1}valued function, almost all theorems proved in systems of Reverse Mathematics can be transferred into LCM.
Since Reverse Math. covers large parts of mathematics, we can prove very many classical theorems in LCM almost automatically thanks to e.g. Simpson s book.
h$ ZZ ZZ"N A recent development in LCM P01 LEM is the weakest LCM semiclassical principle considered.
Even below it, there is an interesting semiclassical principle and corresponding theorems.
It s Weak Koenig Lemma (WKL): any binary branching tree with infinite nodes has an infinite path .8 ZA 5/WKL and LLPO
@Bishop s LLPO: not not (A or B) ! A or B for A, B: P01formulas
WKL is constructively equivalent to LLPO plus the bounded countable choice for P01formulas.
AYA
& 70The strength of WKL P01 LEM derives WKL with a help of a function definition principle for P01 graphs.
In contrast, WKL cannot constructively derive P01 LEM.
Thus, WKL is strictly weaker than LCM.
Still WKL is constructively equivalent to many mathematical theorems like Gdel s completeness theorem for classical predicate logic, HeineBorel theorem, etc. etc& V ZC
DC
7C
x"Y&7 81Three underivability proofs& The underivability of P01LEM is proved by three different proofs:
monotone functional interpretation (Kohlenbach)
Standard realizability plus low degree model of WKL0 (Berardi, Hayashi, Yamazaki)
Lifschitz realizability (Hayashi)C Z ZA*c
U
92Open problem
WKL seems to represent a class of nondeterministic or multivalued computation. Monotone functional interpretation and Lifschitz realizability and seem to give their models.
On the other hand, Hayashi s proof uses JockushSoare s the low degree theorem and the usual realizability, i.e., usual computation.
The relationship between these two groups of proofs would be a relationship of forcing and generic construction.
Open problem: Find out exact relationship.D P
tx
H &
:3
Collaborators The results on hierarchy and calibration are obtained in our joint works with the following collaborators: S. Berardi, H. Ishihara, U.Kohlenbach, T. Yamazaki, M. Yasugi Zp > ` ̙3ff3ff` ff723f` ___WW` 3U33ff` f3f` ff33fCK` S vi3f3` LLff3ff` QVV3Y` .]\̙̙B>?" dd@!?lFd@
" @ ` n?" dd@ @@``PT ! @ ` `)p>> J(
6 "P
R000 0000n0f_[
0 "
Z000 0000n0f_[
,{ 2 000
,{ 3 000
,{ 4 000
,{ 5 000~
0Ƌ "
j* 0
04ʋ "@`
j* 0
0Ћ "
j* 0 T j
"j "
BӋGR o"j
@@ hB
s*DԔ"55H
0h ? ̙3ff3ff80___PPT10.
0[ StudioB S B(
"
<UG̙"
@@ "
BXG+̙ "4
@@ "
BLXp"7`
H 0
6X "X
R000 0000n0f_[
6X "Pw
X
V000 000000n0f_[
0X "X
j* 0
0X "@` X
j* 0
0X "X
j* 0 H
0h ? ̙3ff3ff80___PPT10.
0[
(
NFtt B
*
p88pp
NWtt wB
~*
p88pp
T
Wtt .
*
p88pp
T?Utt w.
~*
p88ppH
0rllC ? 3380___PPT10.b'cTK0 0(
x
c$XX
x
c$XPw
X
H
0h ? ̙33___PPT10i.u``SMt+D=' =
@B +
SK000(
x
c$d\P
\
x
c$<\cgIz\
H
0h ? ̙33___PPT10i.u`0}+D=' =
@B +"
S` l0(
lx
l c$\P
\
x
l c$\\
H
l0h ? ̙3ff3ff*"___PPT10.a0+D' =
@B D' =
@BA?%,( <+O%,(
<+D' =%(D' =%(D0' =4@BBBB%(D' =0l9 CCBB*<3<*lD' =%(D' =%(D0' =4@BBBB%(D' =0l9 HBHBBB*<3<*l+
SK0@0(
x
c$\=\P
\
x
c$0>\\
H
0h ? ̙33___PPT10i.w`*+D=' =
@B +
SK0 t<(
t~
t s* H\P
\
~
t s*H\\
H
t0h ? ̙33___PPT10i.w`*+D=' =
@B +}
S$(
r
SZ\P
\
r
S[\\
H
0h ? ̙3ff3ff___PPT10i.}`w+D=' =
@B +
S@0(
x
c$d\P
\
x
c$d\\
H
0h ? ̙3ff3ff___PPT10i.}`w+D=' =
@B +
SP6(
~
s*$m\P
\
x
c$m\@P\
H
0h ? ^WNff3y___PPT10Y+D=' =
@B +
Sp06(
0~
0 s*v\P
\
x
0 c$w\@P\
H
00h ? ^WNff3y___PPT10Y+D=' =
@B +
S6(
~
s*H}\P
\
x
c$~\@P\
H
0h ? ^WNff3y___PPT10Y+D=' =
@B +
S6(
~
s*\P
\
x
c$\@P\
H
0h ? ^WNff3y___PPT10Y+D=' =
@B +}
S$(
r
S\P
\
r
Sl\\
H
0h ? ̙3ff3ff___PPT10i..aл+D=' =
@B +
S 0(
x
c$l\P
\
x
c$d\\
H
0h ? ̙3ff3ff___PPT10i..aл+D=' =
@B +}
S$(
r
S,\P
\
r
S\\
H
0h ? ̙3ff3ff___PPT10i./a@+D=' =
@B +
S :(
r
S4
P
S
"tXHPpH
0h ? ̙3ff3ff___PPT10i.1a5+D=' =
@B +
S0F(
x
c$
P
c$ #
W
"tXHPpH
0h ? ̙3ff3ff___PPT10i.1a5+D=' =
@B +
S@F(
x
c$(
P
c$?
"tXHPpH
0h ? ̙3ff3ff___PPT10i.1a5+D=' =
@B +
Sph`(
r
S$
P
r
S
Z
GHcV?"6@`NNN?NZ
,$D
0
PGood Kripke or forcing style semantics and categorical semantics are longed for.&Q0PQ& F H
0h ? ̙3ff3ff
___PPT10
.3a 4A+\D
' =
@B D ' =
@BA?%,( <+O%,(
<+D{' =%(D#' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =+48?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B
ppt_x<*D' =+48?\CB#ppt_yBCB#ppt_yB*Y3>B
ppt_y<*Dy' =%(D!' =%(D' =A@BBBB0B%(D' =+48?`CB
ppt_xBCB0ppt_w/2B*Y3>B
ppt_x<*D' =+48?`CB
ppt_yBCB1+ppt_h/2B*Y3>B
ppt_y<*D' =1:Bhidden*o3>+B#style.visibility<*%(+p+0+
++0+
+
S 0(
x
c$
P
x
c$
H
0h ? ̙3ff3ff___PPT10i.3a 4A+D=' =
@B +
S 0(
x
c$
P
x
c$t
H
0h ? ̙3ff3ff___PPT10i.3a 4A+D=' =
@B +
S0(
x
c$h
P
x
c$H
H
0h ? ̙3ff3ff___PPT10i.3a 4A+D=' =
@B +}
S<$(
<r
< S
P
r
< S
H
<0h ? ̙3ff3ff___PPT10i.ya+D=' =
@B +}
Sp$(
r
S
P
r
S
H
0h ? ̙3ff3ff___PPT10i.4aĪs+D=' =
@B +
S40(
4x
4 c$T
P
x
4 c$(
H
40h ? ̙3ff3ff___PPT10i.4aĪs+D=' =
@B +
S@
0(
x
c$
P
x
c$
H
0h ? ̙3ff3ff___PPT10i.ya+D=' =
@B +Z
SF$ '(
<0
(
S0n DNE\c J$J$B c
Bd T#(
P0n LEM\c J$J$B c
B"e
:
S0n1 LEM\
c J$J$B c
B)7
$
S0n LEM\c J$J$B c ^B
6D>M "^B
@
6D>& #f
dB
#
<D>pdp
1
<0c(
P0n+1 DNE\
c J$J$B c
XB
3@
0D>xXB
4
0D>we
<
fGPHl&IhJ7)V?"6@`NNN?N"z ,$D
0
B
<8c
(
D0n LEM\c J$J$B c B
C
ND>?"0@NNN?Nc
D
B< P

F
N@V?"0@NNN?N ~
w'The arrows indicate derivability
in HA (0( ( B
s*h ? ̙33E=___PPT10+XD' =
@B D' =
@BA?%,( <+O%,(
<+D' =%(D' =%(DC' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*<%(D' =6B#blinds(vertical)*<3<*<+}
S`
$(
r
SIP
r
StJ
H
0h ? ̙3ff3ff___PPT10i.b0mV+D=' =
@B +
Sp
0(
x
c$QP
x
c$R
H
0h ? ̙3ff3ff___PPT10i.b0mV+D=' =
@B +}
SH$(
Hr
H SYP
r
H SdZ
H
H0h ? ̙3ff3ff___PPT10i.aB5+D=' =
@B +}
S$(
r
S_P
r
S`
H
0h ? ̙3ff3ff___PPT10i.+a@+D=' =
@B +}
S0 $(
r
SpoP
r
SDp
H
0h ? ̙3ff3ff___PPT10i.Pa0+D=' =
@B +}
S$(
r
Sh
P
r
Sd
H
0h ? ̙3ff3ff___PPT10i.DaW+D=' =
@B +
S 0(
x
c$XP
X
x
c$XX
H
0h ? ̙3ff3ff___PPT10i.DaW+D=' =
@B +}
S
$(
r
Sj
P
r
S
H
0h ? ̙3ff3ff___PPT10i.bn5+D=' =
@B +}
S
$(
r
SH
P
r
S
H
0h ? ̙3ff3ff___PPT10i.b8+D=' =
@B +}
S
$(
r
S
P
r
S
H
0h ? ̙3ff3ff___PPT10i.b+D=' =
@B +
S0
0(
x
c$z
P
x
c${
H
0h ? ̙3ff3ff___PPT10i.Cas+D=' =
@B +r`(ѢN
&52
4Jjx<"$ ' )/ zM2@V7R\?
r>Oh+'0hp
PowerPoint Presentationoweowesusumu hayashie206Microsoft PowerPointon@\v@@gbG
g @ !'3ff$EI)D)@*;+62/.2*4'8$;!?CGLPUZafkptx!$'*.26;@DIxtpkfaZUPLGC?;842/+*))I)'$EI5F5B6>7;87:4<1>/@,C*F(I&L%P$S$W#[#$$ %$&'(+*.,1/316487:;<>=B>F>I??>>=<:8631.+'$ [WSPLIFC@><:87655I5'$Emmmoprtvy=AEIMQTWZ]`bceffg(g,f0f4e8c<b?`B]EZHWJTLQNMPIQEQAR=RQQPNLJHEyBv?t<r8p4o0m,m(mm̙%Emmmoprtvy=AEIMQTWZ]`bceffg(g,f0f4e8c<b?`B]EZHWJTLQNMPIQEQAR=RQQPNLJHEyBv?t<r8p4o0m,m(mm'@"Arial Black. 3ff2
Limit&9.System@"Arial Black. 3ff 2
.@"Arial Black. 3ff2
Computable ,&9&&&&&.@"Arial Black. 3ff%2
Mathematics and its 6&&&9&&#&&&#.@"Arial Black. 3ff2
1Applications,&&&&&&#.@Arial. !2
Susumu Hayashi & t
.@Arial. 2
Yohji .@Arial. 2
vAkama.@Arial. 2

Sep, 22, 2002
.@Arial. 2
(CSL.@Arial. 2
(+.@Arial. 02
(302, Edinburgh, Scotland, UK
.
՜.+,D՜.+,p,
ʂɍ킹r%
/Times New Romanlr oSVbNArialArial Black
Wingdingslr oSymbol
lr CenturyStudio3LimitComputable Mathematics and its Applications #LCM: LimitComputable Mathematics The aim of the talkWhy D02functions? (1)Why D02functions? (2)3An example of semicomputable learning process (1)3An example of semicomputable learning process (2)A limitcomputation of n (1)A limitcomputation of n (2)A limitcomputation of n (3)A limitcomputation of n (4)*Limit computation as Learning process (1)*Limit computation as Learning process (2)Limit and recursive hierarchy.Logic based on limitcomputable functions (1).Logic based on limitcomputable functions (2).Logic based on limitcomputable functions (3)Formal semantics of LCM (1)Formal semantics of LCM (2)Formal semantics of LCM (3)What kind of logic hold?S0n and P0nformulas Semiclassical principles (LEM) Semiclassical principles (DNE)Some examples+Hierarchy of semiclassical principles (1)Important Remark (1)Important Remark (2)LCM semiclassical principles+Hierarchy of semiclassical principles (2)'What theorems are provable in LCM? (1)A recent development in LCM
WKL and LLPOThe strength of WKLThree underivability proofs
Open problemCollaboratorsgpĂtHg fUC ev[gXCh ^Cg% 8@_PID_HLINKSAthttp://www.shayashi.jp/PALCM/&_Nsusumu hayashisusumu hayashi
!"#$%&'()*+,./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{}~Root EntrydO)Current UserSummaryInformation(PowerPoint Document(rDocumentSummaryInformation8