🚀 go-pugleaf

$B!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a(B
$B!!!!!!!!!!!!!!!!5-9fO@M}3X$H>pJs2J3X$N8&5f=82q(B
$B!!!!!!!!!!!!!!!!!!!!!!#S#L#A#C#S!G#9#8(B
$B!!!!!!!!!!!!!!!!!!!!!!!!!!9V1iJg=8(B

$B!!!!!!!!!!!!!!!!#9#8G/#1#07n#1#4F|!A#1#6F|(B
$B!!!!!!!!!!!!!!ElKLBg3X?t3X65<<!J@gBf!&@DMU;3!K(B
$B!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a!a(B

$B!!MhE~$k#1#07n#1#4F|$h$jElKLBg3X$K$*$-$^$7$F!"I85-8&5f=82q$,(B
$B3+:E$5$l$^$9!#5-9fO@M}3X$d>pJs2J3X$N4pACM}O@J,Ln$K4X?4$N$"$k(B
$B3'MMJ}$N8f;22C$r!"?4$h$j$*BT$A$7$F$*$j$^$9!#(B
$B!!>0!"Ev8&5f=82q$K4X$9$k%&%'%VJG$,(B

    http://www.sato.kuis.kyoto-u.ac.jp/SLACS/slacs98.html

$B$K$4$6$$$^$9$N$G$=$A$i$b8fMw2<$5$$!%(B

$B!|>l=j!&F|;~(B

$B!!!!!!!!ElKLBg3X?t3X65<<@n0f%[!<%k(B
$B!!!!!!!!#1#9#9#8G/#1#07n#1#4F|!J?e!K$h$j#1#6F|!J6b!K$^$G(B

$B!|>7BT9V1i!J1Q8l!K(B

$B%&%'%$%J!<@h@8!J%j!<%:Bg3X!K(B 
$B!!!!!V>ZL@O@$HJ#;($5!W(B
$B%P%$%"%^%s@h@8!J%_%e%s%9%?!<Bg3X!K(B
$B!!!!!V%2!<%G%k$NBN7O#T$N7W;;Ns$ND9$5$N87$7$$>e8B!W(B

$B$3$NJ8=q$NKvHx$K!"9V1i$N9<35$rE:IU$7$^$9!#(B

$B!|9V1iJg=8(B

$B!!5-9fO@M}3X$H>pJs2J3X$NNN0h$+$i!"M}O@!"1~MQ$r4^$a!"9-$/9V1i(B
$B$rJg=8CW$7$^$9!#(B
$B!!9V1i$r$44uK>$NJ}$O#97n#1#4F|!J7n!K$^$G$K0J2<$N=q<0$K$F44;v(B
$B$^$G$*Aw$j2<$5$$!#9V1i;~4V$O0l9V1i$"$?$j#3#0J,$+$i#5#0J,$rM=(B
$BDj$7$F$$$^$9!#(B
$B!!9V1i$O35$MF|K\8l$K$F$*4j$$CW$7$^$9!#$^$?!"9V1iBjL\5Z$S9<35(B
$B$O!"=PMh$^$7$?$i!"F|K\8l$N$b$N$H1Q8l$N$b$N$HN>J}$*=q$-2<$5$$!#(B
$B$b$7JRJ}$@$1$r$*=q$-$N>l9g$K$O!"44;v$,E,Ev$KfLLuCW$7$^$9!#(B
$B!!N9HqEy$N1g=u$r4uK>$5$l$kJ}$O!"=PMh$k$@$1Aa$/$4O"Mm2<$5$$!#(B
$B3X@8$NJ}!9$b5$7Z$K44;v$^$G$4AjCL2<$5$$!#(B

$B!|9V1i?=9~Dy@Z!!#97n#1#4F|!J7n!K(B

$B!|=IGq$O$4<+?H$K$F$*<jG[2<$5$$$^$9$h$&$*4j$$CW$7$^$9!#(B

$B!|44;v$NO"Mm@h(B

$B!!EE;R%a!<%k!'(B	slacs-kanji@sato.kuis.kyoto-u.ac.jp

$B!!M9JX!'!!!!!!!!")#6#0#6!]#8#5#0#1!J@lMQM9JXHV9f=;=jITMW!K(B
$B!!!!!!!!!!!!!!!!5~ETBg3X>pJs3X8&5f2J!!!!C]Fb!!@t(B

$B!!#F#A#X!'!!!!!!(B075(753)4954

$B!1!1!1!1!1!1!1!1!1!1!1!1!1!1!1!1!1!1!1!1!1!1!1!1!1!1!1!1!1!1(B
$B!!!!!!!!!!!!!!!!!!!!9V1i?=9~=q<0(B

$B#S#L#A#C#S#9#8$G$N9V1i$r4uK>$7$^$9!%(B

$B;aL>!'(B

$B;aL>!J%m!<%^;zI=5-!K!'(B

$B=jB0!'(B

$B=jB0!J1QLu!K!'(B

$B9V1iBjL\!'(B

$B9<35!J#59T!A#1#09TDxEY!K!'(B

$B4uK>9V1i;~4V!'(B

$B;kD03P@_Hw$N;HMQ!'#O#H#P!"%W%m%8%'%/%?!<(B $B$J$I(B

$BN9Hq$N1g=u$r?=@A!'$9$k!"$7$J$$(B

$B!JFC$K9V1i4uK>F|;~$,$"$l$P$*=q$-E:$(2<$5$$!K(B
$B!2!2!2!2!2!2!2!2!2!2!2!2!2!2!2!2!2!2!2!2!2!2!2!2!2!2!2!2!2!2(B

$B!|4XO"8&5f2q(B

$B!!ElKLBg3X$NEDCf0lG7@h@8$h$j0J2<$N7o$N9-Js$r0MMj$5$l$^$7$?!#(B

$B!V(BWorkshop on Meta-Arithmetic and Computation$B!W(B
	$BF|Dx!'(B1998$BG/(B10$B7n(B13$BF|(B($B2P(B)$B!A(B14$BF|(B($B?e(B)
	$B>l=j!'ElKLBg3XBg3X1!M}3X8&5f2J?t3X@l96(B
	$BFbMF!'(B	S. Wainer $B@h@8!J(B Leeds $BBg3X!K(B
		A. Weiermann $B@h@8!J(B Muenster $BBg3X!K(B
		$BC]Fb30;K@h@8!J(B Illinois $BBg3X!K(B
	$B!!!!!!$N9V1i$,M=Dj$5$l$F$$$^$9!#(B

$B%W%m%0%i%`$J$I>\:Y$O!"#S#L#A#C#S$N%W%m%0%i%`$HF1MM!"#97n2<=\(B
$B$KH/I=$5$l$k$=$&$G$9!#(B

$B!|>7BT9V1i9<35(B
$B!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!](B

Stanley S. Wainer (University of Leeds, UK)

Tilte: Proof Theory and Complexity

This talk will describe some joint work with my student
G. Ostrin, on the proof theory of low subrecursive classes.
The basis is "A new recursion theoretic characterization of
the polytime functions" by Bellantoni and Cook (1992), in 
which it is shown that a natural two-sorted re-interpretation
of the normal primitive recursion schemes characterizes 
polynomially bounded computation. We show that if Peano 
Arithmetic is instead formulated in this two-sorted fashion,
with quantification allowed only over one sort (the "safe"
variables) and induction allowed only over the other ("normal"
variables), then the provably computable functions are exactly
the Kalmar elementary functions E(3). The provably computable 
functions of the $B&2(B_n Inductive fragments of the theory 
turn out to be closely related to the levels of Ritchie's
hierarchy of "Predictably computable functions" (1963), with
$B&2(B_1 Induction corresponding to the linear space functions
E(2). This work is related to other results of Buss, Bellantoni,
Beckmann and Leivant, but in addition it clearly illustrates 
the use of classical ordinal analysis techniques at this low level.
The difference with classical Peano Arithmetic is that it is now 
the Slow Growing Hierarchy which supplies the bounding functions,
rather than the Fast Growing Hierarchy which arises in the classical
case.

$B!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!](B

Andreas Weiermann (Westfaelische Wilhelms-Universitaet Muenster, Deutschland)

Title: Sharp bounds for the lengths of reduction sequences in Goedel's T

Abstract: Using ideas from infinitary proof theory and based on Howard's
weak normalization proof for Goedel's system T we define
a numbertheoretic function f such that for two given terms
a and b of T the following holds:
If a rewrites to b then f(a) is strictly larger than f(b). 
f ensures termination of T and, in addition,
it yields optimal upper bounds for the lengths of
reductions in Goedel's T.

$B!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!](B