EoSA
@J/8&\EtCI*
'PgӌLf]o2$.{6ĘJR?v AShBR.mp,jdgt7Ţͫ##}.@iM
#XmX$F
X)KOP6s/S4
#sFHwH8<>m 4iRg[IEًd+UcpPB tueNC3)4H5Y(M
VP6c#}4y+YCYA>śȺ1KYE˗
R/!&
08,VaT6avU],K7`?FB)Jxpxո
1L+ccq6+lwd2^t/*g%n#A>c?5w>wLŹgSǚAzo)8J& E"_Ҩ
HF87&lalёHdlY@F1n;U<گa2'ɕVPaj$$mK,tUtȆzGUF`ߔ
C]Kٟ!fY5OhuV
.X*i \:gg?jrh8$/ 1c;ft9p]3%U[ĐL#ipe(G{MW몂6aXhVdθIyF6.m\",icXF1Ё^*9jI]ngc[h]7yU2j:c104CiW"v'8bOt=uW~t=k{O?Jwޞo^`:вq첎HL:G^>Wx_??Գ/:gooo;
6U͉₨EFo]'O=r7>ľ~q'J@U✈]1@ڹGўGuu?y+:Ktۿ<{S4M
QR
_\.:uc[oD{{n_>mm/}诺z,m%U;$.`4b:=pc/?מ/h3;C\,2o9u8ç???zzon?b±'W4.k#gIENDB`(mp <
aR>http://www.di.unito.it/~stefano0r.Fotografia Photo Editor MSPhotoEd.30BFotografia di MS Photo Editor 3.0`/0DTimes New Romanث( )0(Y0XDStarBats Romanث( )0(Y0 DSymbols Romanث( )0(Y0X0DCourier Newmanث( )0(Y0X1@DMonotype Corsiva( )0(Y0XBf ."D
@n?" dd@ @@``
+ E6,((*)('$"&%#!
,b$A;Lk3De
A@ A5% 8c8c
?1 d0u0@Ty2 NP'p<'pA)BCDES" f33@Rg4DdDd )0^ppp@<4!d!d0Ĭg4;d;d )0(pO
p:%
ʚ;2Nʚ;<4ddddH04___PPT9~/0b
"
#0$&*((')$ ,%+?$
sefawefgO=Continuations, Backtracking and Limits:a notion of Construction for Classical Logic(Ongoing work)Kyoto, November 2004 Z'$rAbstract of the talkWe describe Classical Principles in term of constructions , of a general kind, learning a value by trialanderror, rather than computing it exactly.
This notion of construction may be described in term of continuations and backtracking, or by Coquand s game interpretation, or by Hayashi s Limit Interpretation. B" dBAL 1. Heyting s notion of construction ' "'rHeyting defined a notion of construction for a formula F.
For Heyting, a construction of F is something computing all informations about F we expect from a proof of F.
We will now introduce Heyting s notion of construction in some details.
Later, we will consider a generalization of it:
Limit Realizability.F%" dZ" dZ%:9An inductive definition of a construction for a formula F:::If F = P(t1, & , tn), with P decidable predicate, then a construction of F is anything, provided F is true.
If F = F1F2, then a construction r of F is any pair <i,s>, with i{1,2}, and s construction of Fi.
If F = F1F2, then a construction r of F is any pair <r1,r2>, with r1 construction of F1, and r2 construction of F2.E" d33333[33333633333+ E9An inductive definition of a construction for a formula F:::If F = "xI.G(x), then a construction r of F is any computable map
f :I{constructions of G(x), for some xI}
such that, for all xI, f(x) is a construction of G(x).
If F = $x.G(x), a construction r of F is a pair <i,s>, with iI, and s construction of G(i).4D" d+" d8" d]" d333$
"&333/9An inductive definition of a construction for a formula F:::If F = F1F2, then a construction r of F is any computable map
f :{constructions of F1}{constructions of F2}
If F = G, a construction of F is anything, provided there is no construction of G.
F@" d/" dT" d" d33333$
333L*0n and 02formulasp N0nformulas are all formulas
A(x1, x2, & ) = $x1N. "x2N. & . P(x1, x2, & )
with n alternating quantifiers, starting with $, and with P decidable.
0nformulas are all formulas
B(x1, x2, & ) = "x1N. $x2N. & . P(x1, x2, & )
with n alternating quantifiers, starting with ", and with P decidable.h" dZ." dZG" dZ" dZ." dZG" dZ3333333333333333333333.3333333333333333333.3( Constructions as programsBy unfolding definitions, a construction r for a closed 02formula B = "xN. $yN. P(x,y) provides some map f, satisfying P(x,f(x)) for all xN.
If we think of B as a specification, a construction for B provides some program f satisfying the specification B.t" d8:v#Intuitionistic and Classical Proofs$$$8EM (Excluded Middle) is the axiom schema
"xN. A(x) A(x)
nEM is the axiom schema EM restricted to 0n formulas.
Intuitionistic proofs are all proofs not using Excluded Middle (in any equivalent form).
Classical proofs are proofs possibly using Excluded Middle (in some form). *" d" d" d*33"L C
(Intuitionistic Proofs are constructions)))We may interpret any intuitionistic proof of F as defining some construction of F, and therefore a program if F is 02formula.
Programs extracted from proofs in this way are usually very naive, but they are a starting point in order to design real programs.
Constructive interpretation of Heyting is a bridge between Mathematical proofs and applications.~d" dS dbClassical Proofs are not Heyting s constructions222There is no construction for Excluded Middle. Let A(x) = $yN.P(x,y) be any 01formula. By unfolding definition, there is some construction for the formula:
"xN. A(x) A(x)
if and only if there is some computable characteristic map in N for A(x) (i.e.: some f:NN such that f(x)=0 if and only if A(x) is true). But for some P, there is no computable characteristic map in N of A(x). " dZ" dZ" dZ233N3X@9Preliminary Conclusion Most Mathematical proofs are Classical. By what we said, apparently, such proofs define no program. Therefore they have no applicative interest.
This preliminary conclusion, however, is false. ." d9*`"Plan of the Talk BWe will define a relaxed notion of construction, obtained from Heyting s by replacing everywhere computable with limit computable .
With this new notion of construction there is a construction for Excluded Middle. Constructions of closed 02formulas still correspond to programs.
Before introducing limit computability, we give a quick account of what is known about extraction of programs from Classical Proofs.v" dZam0 2. A constructive content for Classical Logic11 1Call PA (Peano Arithmetic) Arithmetic with quantification over integers, Induction axiom for all formulas, and Excluded Middle.
Call HA (Heyting Arithmetic) PA without Excluded Middle.
Godel proved 02conservativity of PA w.r.t. HA: If B is a 02formula and PA proves B, then HA proves B. Besides, there is a computable map turning every proof of B in PA into a proof of the same B in HA " dZ
Classical proofs are programs If we interpret proofs in HA by constructions, 02conservativity implies that every proof in PA of a 02formula B = "xN. $yN. P(x,y) may be turned into a program f such that P(x,f(x)).
02conservativity is a bridge between Mathematics and applications.
However, this result has also some limitations, as we will see.E" d/3 7E\Some limitations of 02conservativity resultT/ /No intuitive explanation is given. How can classical proofs of 02statements be programs, if they use Excluded Middle, and there is no construction for Excluded Middle?
As a consequence, we miss a global understanding of the program we extract from a proof. This means that, if the program is naive, as usually is, we have no way of making it better. Therefore we have no real way of using it. " d#P
&,VA refinement of 02conservativity result \, ,xThe first refinement of 02conservativity is due to Griffin (around 1980).
Griffin defined a programming language in which classical proofs could both be written and executed: lambda calculus with Continuations.
Griffin s programming language was simplified by Parigot (lm calculus), and by Berardi (symmetric l calculus). Eventually Curien and Herbelin merged the last two calculus, defining symmetric lm calculus (possibly the best so far)." dZ&]&"Continuations and Classical Logic #! #There is a common idea underlying Griffin s calculus and those who came later: to interpret Excluded Middle by means of Continuations.
Let s be any computation. The continuations of s are some set of computation states M1, & , Mn, stored in the memory of s.
At any moment, s can store the current state E (or part of it) in the set of continuations._" d
%L_#
Backtracking 6At any moment, the computation s can either:
move from the current state E to the next state E (an ordinary step)
move to some state M1, & , Mn in the set of continuation (an exceptional step).
If Mi is some previous state of the computation, we call this second choice backtracking." d" dZ" d!Z3G`Continuations and simply typed lambda l calculus61
1We may add continuations to simply typed lambda l calculus by adding a constant C of type (F F), together with the rewrite rule
(C) E[C(M)] : False M(lx.E[x]) : False
The axiom schema (F F) is intuitionistically equivalent to Excluded Middle. This is the connection between C and Classical Logic.
The rule (C) say that M is a continuation: the computation of E can move to M. A copy of E, in the form lx.E[x], is saved as argument of M. E can added by M to the set of continuations of the computation.b" dZ8" dZS" dZ03 3333# =Y Advantagesof continuations Using continuations, we may describe stepbystep the evaluation of the classical program extracted from a proof.
Continuation are a major advance in extracting programs out of classical proofs." d$Disadvantagesof continuations 0Using continuations, we miss a global and intuitive understanding of the program.
This means we cannot rewrite naive programs in order to obtain efficient programs. In fact, we still cannot use them.
In the rest of the talk, we will outline a semantical constructive interpretations of classical proofs.J1" d#+
21! 3. Semantic of Classical Proofs "! "By a Tarski structure M for a language L we mean a set X, equipped with an equivalence relation ~, and, for each relation R and map f of L, some relation RM and some map fM, both compatible with ~.
A formula F of L is true in M if it is is true the formula obtained by replacing, in F, the symbol = with ~, and all symbols R, f with RM, fM.
A Tarski model of a theory T is a Tarski structure M for the language of T, such that all theorems of T are true in M." dZ y.Interpretation of a theory inside another one /. /A model of a theory T is the usual way of explaining the mathematica concepts of T.
An interpretation of a theory T inside a theory U defines some model M of T using predicates and maps of U, and proving in U that all theorem of T are true in the model.
An interpretation of a theory T inside a theory U is the usual way of explaining the mathematical concepts of T in term of the mathematical concepts of U.0" dZAn example of interpretation ^We may interpre the theory H of Hyperbolic Plane inside the theory E of the Euclidian plane.
The set of elements of H is some set of points of the Euclidean Plane. The equivalence relation is equality on the Euclidean Plane. Any geometrical operation or relation of H is defined through some geometrical operation or relation of the Euclidian Plane. _" d__,02sound models of PAHJA model M of PA is 02sound if all closed 02formula B = "xN. $yN. P(x,y) true in M are true in the usual sense:
for all nN there is some mN such that P(n,m)
If M, B are as above, then any intuitionistic proof that B is true in M provides some program f such that P(x,f(x)) for all xN.Vv" d/" d" d
B6&Interpreting PA inside HA We want to define an interpretation of PA inside HA, in order to interpret Excluded Middle as a construction in some structure.
This is no easy task. There are several impossibility results we have to turn around (see [1]).
We also want to get some intuitive explanation of the programs we extract from classical proofs.
Therefore we only consider 02sound models M of PA.dw" dZ]
wThe main result Let PA",$ be the variant of PA whose set of logical connectives is:
"i{1,& n}.Ai, $i{1,& n}.Ai,
"iP(i), $iN.P(i)
Theorem. There exists a 02sound interpretation M of PA",$ in HA.
We may interpret every step of every classical proof of PA by some construction in some model M, in such a way that a proof of a closed 02formula defines a program.~E" dZ=" dZ" dZ<3333333
f)l&The model M of PA in HA,
lM is the set of all iterated limits of integers, taken over List(N), the set of lists of integers.
Definition of M generalizes Hayashi s Limit Computable Mathematics [4], in which limits are taken over N, and M is defined in PA itself.
Limits over List(N) are intended to give a more accurate descriptions of computations hidden in classical proofs.
M is defined in HA in order to show we may completely describe EM in term of limits." dZ ._
H*Conclusion and Future Work Eventually, we switched to a semantical interpretation of classical proofs, looking for some intuitive understanding of the programs we can extract from them.
This is a work in progress. The model we found looks promising, but it should be checked against some relevant examples. We have also to implement the computations in the model in term of backtracking and continuation.
We are quite confident this is possible. " dZ* 4. Appendix. Intepreting HA +1EM in HA"+ &+We sketch the definition of the interpretation of PA in HA in a simple case: when EM is restricted to 1EM.
We define a structure we call N1 (see [3])
The same construction also produces some model of (n+1)EM out of any model of nEM.
A model of EM is obtained by defining a succession of models of 0EM, 1EM, 2EM, & , then taking the direct limit of them.Lh" d33hA notion of Computation State Let S = List(N) be the set of all finite lists of integers, ordered by prefix. We call the elements of s computation states.
Intuitively, s is a list of (codes of) pairs
<n1,"x.P1(x)>, & , <nk,"x.Pk(x)>
of some integer ni and some 01formulas "x.Pi(x).
If P=Pi and Pi(ni) is false, we know that "x.P(x) is false.
Otherwise we assume that "x.P(x) is true." dZ$" dZ3" dZg" dZ333333333&j(Dynamic Integers We call any L:SN a dynamic integer .
Intuitively, L(s) is an hypothesis about a value, depending on the hypothesis about 01formulas associated to the state
s = <n1,"x.P1(x)>, & , <nk,"x.Pk(x)>
If some hypothesis change, then L(s) can change. L(s) will be a convergent limit if
in any correct computation of L,
eventually L(s) stops changing 2" dZ," dZU" dZC" dZ}"
333333333UCe'A notion of Agent Let Pfin(N) be the set of all finite subsets of N.
We call any F:S Pfin(N) an agent of the computation.
Intuitively, F(s) is a set of elements of the same kind of those which are in the state s:
F(s) = {<n1,"x.P1(x)>, & , <nk,"x.Pk(x)>}
The agent F requires to add the set F(s) above to the state s of the computation." d." dR" d>}
333333333TF)A notion of Computation Let s be any recursive weakly increasing successions s0 s1 s2 & in S
We say that s is a computation of an agent F, or s:F for short, if, eventually, any element a of F(si) either drops out of F(si), or it is added to si.
Formally: s:F if, for all a,nN, there is some mn such that either aF(sm), or asm.
Remark that this definition describes a notion of parallel asyncronous computation." d6n3< 20Convergence and Equivalence of Dynamic Integers 101NLet F:S Pfin(N) be an agent, L, M:SN be dynamic integers. Abbreviate (L is convergent), (L, M are equivalent), with L, (L~M). Then we define:
F is a construction of L, or F:L for short, if for all computations s0 s1 s2 & of F, there is some nN such that L(sn)=L(sn+1).
F is a construction of (L~M) , or F:L~M for short, if for all computations s0 s1 s2 & of F, there is some nN such that L(sn) = M(sn).\" dZ" dZG*O*The Tarski structure N1>Let F:S Pfin(N), and L, M:SN. For any nN, define n:SN by n(s) = n for all sS.
L if F:L for some F
(L~M) if F: (L~M) for some F
N1 is the set of all convergent dynamic integers, with equivalence relation ~. Maps of N1 are all computable maps f:N1 N1 such that
f(L)(s) = f(L(s))(s) for all sS.W" d" d(" d(3333U333F,A construction for 1EM in N1 XfA characteristic map in N1 for a 01formula $yN.P(x,y) is any map f of N1 such that, for all xN1, f(x) ~ True if and only if P(x,y) is true for some yN1.
Maps of N1 are computable, yet they include characteristic maps for all 01formulas, and therefore some construction for 1EM.
Characteristic maps in N of 01formulas, usually, are not computable. This is no contradiction. Characteristic maps in N1 are such only up to ~.J" dZ&
0R3
%Bibliography
l[1] S. Berardi, Intuitionistic Completeness for First Order Classical Logic, J.S.L., vol 63, Number 1, March 1999.
[2] S. Berardi, Classical Logic as Limit Completion, MSCS, 15, 2004 (to appear).
[3] S. Berardi, A Model for D02maps within Intuitionistic Arithmetic, Techical Report, Turin University, 2004.7" dg#
&+`+Bibliography
[4] S. Hayashi and M. Nakata, Towards Limit Computable Mathematics , Types for Proofs and Programs, Springer LNCS, 125144, 2001.
[5] Y. Akama, S. Berardi, S. Hayashi, U. Kohlenbach, An Arithmetical Hierarchy of the Law of Excluded Middle and Related Principles , pp. 192201, 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 1417 July 2004, Turku, Finland, Proceedings." dZX" dZ'?5Pu/8,P9 ` ̙33` ` ff3333f` 333MMM` f` f` 3p?rd,
?"dD EK kE"0EK@E"P v?" dd " @ `@v?" dd " @ `Pe" de d e" d@e d`ed`n" d d " d@@ d``dpe" de d e" d@e d`ede" de d e" d@e d`ed}u(
H) )
k7Cliccate per modificare il formato del testo del titolo8
8
B ) ,)
NCliccate per modificare il formato del testo della struttura
Secondo livello struttura
Terzo livello struttura
Quarto livello struttura
Quinto livello struttura
Sesto livello struttura
Settimo livello struttura
Ottavo livello struttura
Nono livello struttura={
B
s*?rs ? ̙33 *Struttura predefinita0PF(
^
S Y

0y &
0 <
c$9g ? ̙33p@8(
NXJGJG @8
*("!&
NhVJGJG q 8
**"!& "
TVJGJG '@_
*("!& $
TdVJGJG 'q _
**"!& H
09g ? ̙334
0z(
N8
6@ >
n
Stefano Berardi, Semantic of Computation group
C.S. Dept., Turin University, http://www.di.unito.it/~stefanoX"!m"! M$ BF
0On4X
x@
HA??"@VB
s*3?rs ? ̙33
L(
N8V
V
F2X
x@@
C ,
N(, ,V
F2X
x@
N~)?"P
x*4X
x@B
s*?rs ? ̙33
$(
r
ST^V
V
r
S_V,V
H
0?rs ? ̙33
0(
x
c$tV
V
x
c$huV,V
H
0?rs ? ̙33
0(
x
c$ԁV
V
x
c$V,V
H
0?rs ? ̙33
p0(
x
c$[V
V
x
c$[V,V
H
0?rs ? ̙33
`0(
x
c$)
)
x
c$),)
H
0?rs ? ̙33
P0(
x
c$ؿ)
)
x
c$),)
H
0?rs ? ̙33
@0(
x
c$@HV
V
x
c$HV,V
H
0?rs ? ̙33
00(
x
c$=V
V
x
c$>V,V
H
0?rs ? ̙33
0(
x
c$t/V
V
x
c$0V,V
H
0?rs ? ̙33
0(
x
c$V
V
x
c$@VV
H
0?rs ? ̙33
P0(
Px
P c$
V
V
x
P c$VV
H
P0?rs ? ̙33
0(
x
c$V
V
x
c$VCV
H
0?rs ? ̙33
0(
x
c$T
T
x
c$LTCT
H
0?rs ? ̙33
0(
x
c$T
T
x
c$pTCT
H
0?rs ? ̙33
0(
x
c$T
T
x
c$TCT
H
0?rs ? ̙33
0(
x
c$T
T
x
c$TCT
H
0?rs ? ̙33
TF(
Tx
T c$T
T
T c$HTCT
"H
T0?rs ? ̙33
0(
x
c$`T
T
x
c$TCT
H
0?rs ? ̙33
0(
x
c$T
T
x
c$XTpT
H
0?rs ? ̙33
X0(
Xx
X c$,
,
x
X c$,C,
H
X0?rs ? ̙33
p0(
x
c$LT
T
x
c$TCT
H
0?rs ? ̙33
` 0(
x
c$yw蕓Bbo)7o_{7{כVU(5^^__5UR]s%kQߍz)eWp~ԫP?AԫQkQ?auA(P/O[ö㧃ձp5<ŃƯ\ʗGt4g{oV]t!߳m{h7KUo]X;踓'V.fv;&wl#O;hoz)^eU%e,K+V[}ܳ}uMnnc=u_'n͕Vi^o/i??¾!Ά3_Z6`;t=I\,nY6+vw&iNssRsZC ZUSsZQTiݒWlUx9OşVl;֤Iզ[~Sy6;LjR_$w+I%<%뷙'U{Zlvּb[K۲S;RӮm4Jf4؇%s~Y;I^ҥU¶VSո_lHv3ZyZ`6vgk9:d2 h4:<ك57 CDG*V>a&Pz&
A.x7F٨%A^91)E@MMeBP_26z}9%O:'=]7̨<aF3vH#ixI.
6Q]_8lIB WAiڡCO,vjnBL:I&].ϳyҖAxb2!S,
d8:za`=\uy! J3 ÁPϢz\^0ОtTBPvB0X6
fcgM>
%6<#OJғ8+\4}9c2[x10(HJI3&$z#г[r$=S2QXm{`Lr(n5MF"ɧKG^n#gq25+Q(_ΫPxp=
Ecw;#:(%vr"C/6@il5=
B'AF[(bSL}HB XMh9Yp
$'$@JPe")
ENJڶh,{JI/gJI$D8ZNdSIy$
lRc2u%67ciO\^3j4a'#0(]`6WN6bI5}H~ƙ́ht E)lV?#^M8D; Z0M\df
c]^r*"2h`tH@wxo$9BفMd
` U]#gsT&e)Qxu03y>#Q8D/O@HS@9}tNL0l6x*S(&01d9AiO8z#p/;=VH(yLu/mnp.`
0@u.7o/!$cq
ĞN^:zJnY̹槳9,NwC<5ۯ?Gnve7]>'ЉJ2<.dG4=5~ͦuu뾼.ϯnjd՝}lf^H%Kāpc~rw{u]bYf{ns'wt܁t,9 2i\EwmݵuڹMl5Ml}5oݽuǝeQgIK*Sܱv{Yzۥm/weu\"q&շnqp_xmݺO[s~ײf7o[wݺk}y8sJ<~g'FGG?kѣu<趺wY>ͯu؎غkwP].A5;JmL#DpxQ{߾}i߾߭/߰S{dn7p#=P']" Ĳ$Uq=c[WO_s7^][)AJșH6{w?oԲb=
ݵ+QVߺKtwI^>;ǌO}H&z}×0v#ꖏҽwCpKgǄ/7
l
EzY2,`Қĸ.1[fj)v;;XɊy?+4I'Ԝ̏*A+SNܳVTX93ww+62Ejg
hWܭ;1
RE8VT8zvVxknHfVui=݂~,
lvv+ƶ3/(ed#3dKigz:G1kRc\:L_~T
tX$θh14 pȂcc֪r3$xˣC^nXg
l'L_/Ov+6FkBDUŹZU'xiȳ3;J5FKZy1Zbᰝ95fk7XY]tgjk9C]@ ָ؆FZZ8kj:Wl~v0kh̎FǹMIz!F\Kv@'Ių6*Cgx W>hx2ΡZcihCt64]*a=f3xT:GKCc'}1Pq ۂZ#0ivxc`_3fBՀzeJz4CE ,3ItAY:U_]7K(~c'q
vxq="ZѦ_UYzaߐA$$p.ssڽ
poeRcΓyX,G_Y
UHOYgd2kvCsyxUS!a=n92*
3:Z
f\qX7 zY%%)4@Vgm8N`aދ^&gJLqƤ
WC 2<9V6! Їt4o[@+Zm ʰD:Ν*\[yb+,/C'\X,PkD?uj3{8,McԬeV2S1Ec=MoAkib:Eu\=~6l`aІ8Y9
h#s`v2aMX2(&Chad
(X2j76qΆuث&^m=;
]˸/##p')tqР>uy+x06fCqmxV1m*'9SbAk'
3g$)CF2agd1rRo؛{bNvˈE`ZːWj2=eeQieط#!>h]F}eX}# ,>Vr,>']F}&,>˰`D,MebaDXF{˰82jeȪ2h)X˰Eg`,Öe؞ѨDQ+.˰}(ģQcA;vȾF$,6\ 0ha5MؽAe&>2jg!U;˰="w1٭*m'+x4h1al¨m2fx.c6^S6e?EP2?5eؿ˰iah,BU5?Eo]_rPM, _ I"p?r3$p} {@kc[S`KC+#'usC;)1!03
Q5=л(mp <
cR>http://www.di.unito.it/~stefano0roi.Fotograf /Times New Roman StarBatsSymbolCourier NewMonotype CorsivaStruttura predefinita"Fotografia di MS Photo Editor 3.0Continuations, Backtracking and Limits: a notion of ‘‘Construction’’ for Classical Logic (Ongoing work) Kyoto, November 2004Abstract of the talk*§ 1. Heyting’s notion of construction:An inductive definition of a construction for a formula F:An inductive definition of a construction for a formula F:An inductive definition of a construction for a formula F0n and 02formulasConstructions as programs$Intuitionistic and Classical Proofs)Intuitionistic Proofs are constructions4Classical Proofs are not Heyting’s constructionsPreliminary Conclusion Plan of the Talk 2§ 2. A constructive content for Classical LogicClassical proofs are programs1Some limitations of 02conservativity result.A refinement of 02conservativity result #Continuations and Classical Logic Backtracking 5Continuations and simply typed lambda –calculusAdvantages of continuationsDisadvantages of continuations#§ 3. Semantic of Classical Proofs/Interpretation of a theory inside another oneAn example of interpretation02sound models of PAInterpreting PA inside HAThe main resultThe model M of PA in HAConclusion and Future Work,§ 4. Appendix. Intepreting HA +1EM in HAA notion of Computation StateDynamic IntegersA notion of AgentA notion of Computation1Convergence and Equivalence of Dynamic IntegersThe Tarski structure N1A construction for 1EM in N1
Bibliography
BibliographyCaratteri utilizzatiModello strutturaServer OLE incorporatiTitoli diapositive( 8@_PID_HLINKSAx http://www.di.unito.it/~stefano_istefanostefano՜.+,D՜.+,\
Personalizzato( /Times New Roman StarBatsSymbolCourier NewMonotype CorsivaStruttura predefinita"Fotografia di MS Photo Editor 3.0Continuations, Backtracking and Limits: a notion of ‘‘Construction’’ for Classical Logic (Ongoing work) Kyoto, November 2004Abstract of the talk*§ 1. Heyting’s notion of construction:An inductive definition of a construction for a formula F:An inductive definition of a construction for a formula F:An inductive definition of a construction for a formula F0n and 02formulasConstructions as programs$Intuitionistic and Classical Proofs)Intuitionistic Proofs are constructions4Classical Proofs are not Heyting’s constructionsPreliminary Conclusion Plan of the Talk 2§ 2. A constructive content for Classical LogicClassical proofs are programs1Some limitations of 02conservativity result.A refinement of 02conservativity result #Continuations and Classical Logic Backtracking 5Continuations and simply typed lambda –calculusAdvantages of continuationsDisadvantages of continuations#§ 3. Semantic of Classical Proofs/Interpretation of a theory inside another oneAn example of interpretation02sound models of PAInterpreting PA inside HAThe main resultThe model M of PA in HAConclusion and Future Work,§ 4. Appendix. Intepreting HA +1EM in HAA notion of Computation StateDynamic IntegersA notion of AgentA notion of Computation1Convergence and Equivalence of Dynamic IntegersThe Tarski structure N1A construction for 1EM in N1
Bibliography
BibliographyCaratteri utilizzatiModello strutturaServer OLE incorporatiTitoli diapositive( 8@_PID_HLINKSAx http://www.di.unito.it/~stefano_>stefanostefano
!"#$%&'()*+,./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{}~Root EntrydO)%
PicturesCurrent User*5SummaryInformation(PowerPoint Document( DocumentSummaryInformation8` ia Photo Editor MSPhotoEd.30BFotografia di MS Photo Editor 3.0`/0DTimes New Romani`H )0`Y0DStarBats Romani`H )0`Y0 DSymbols Romani`H )0`Y00DCourier Newmani`H )0`Y01@DMonotype Corsivai`H )0`Y0Bf ."D
@n?" dd@ @@``
+ E6((*)('$"%#!
,b$A;Lk3De
A@ A5% 8c8c
?1 d0u0@Ty2 NP'p<'pA)BCDES" f33@g4DdDd )0T^ppp@<4!d!d0ig4;d;d )0T(pO
p:%
ʚ;2Nʚ;<4dddd0lph___PPT9J/0.
"
#*$&*('),%+?$
sefawefgO=Continuations, Backtracking and Limits:a notion of Construction for Classical Logic(Ongoing work)Kyoto, November 2004 Z'$rAbstract of the talkWe describe Classical Principles in term of constructions , of a general kind, learning a value by trialanderror, rather than computing it exactly.
This notion of construction may be described in term of continuations and backtracking, or by Coquand s game interpretation, or by Hayashi s Limit Interpretation. B" dBAL 1. Heyting s notion of construction ' "'rHeyting defined a notion of construction for a formula F.
For Heyting, a construction of F is something computing all informations about F we expect from a proof of F.
We will now introduce Heyting s notion of construction in some details.
Later, we will consider a generalization of it:
Limit Realizability.F%" dZ" dZ%:9An inductive definition of a construction for a formula F:::If F = P(t1, & , tn), with P decidable predicate, then a construction of F is anything, provided F is true.
If F = F1F2, then a construction r of F is any pair <i,s>, with i{1,2}, and s construction of Fi.
If F = F1F2, then a construction r of F is any pair <r1,r2>, with r1 construction of F1, and r2 construction of F2.E" d33333[33333633333+ E9An inductive definition of a construction for a formula F:::If F = "xI.G(x), then a construction r of F is any computable map
f :I{constructions of G(x), for some xI}
such that, for all xI, f(x) is a construction of G(x).
If F = $x.G(x), a construction r of F is a pair <i,s>, with iI, and s construction of G(i).4D" d+" d8" d]" d333$
"&333/9An inductive definition of a construction for a formula F:::If F = F1F2, then a construction r of F is any computable map
f :{constructions of F1}{constructions of F2}
If F = G, a construction of F is anything, provided there is no construction of G.
F@" d/" dT" d" d33333$
333L*0n and 02formulasp N0nformulas are all formulas
A(x1, x2, & ) = $x1N. "x2N. & . P(x1, x2, & )
with n alternating quantifiers, starting with $, and with P decidable.
0nformulas are all formulas
B(x1, x2, & ) = "x1N. $x2N. & . P(x1, x2, & )
with n alternating quantifiers, starting with ", and with P decidable.h" dZ." dZG" dZ" dZ." dZG" dZ3333333333333333333333.3333333333333333333.3( Constructions as programsBy unfolding definitions, a construction r for a closed 02formula B = "xN. $yN. P(x,y) provides some map f, satisfying P(x,f(x)) for all xN.
If we think of B as a specification, a construction for B provides some program f satisfying the specification B.t" d8:v#Intuitionistic and Classical Proofs$$$8EM (Excluded Middle) is the axiom schema
"xN. A(x) A(x)
nEM is the axiom schema EM restricted to 0n formulas.
Intuitionistic proofs are all proofs not using Excluded Middle (in any equivalent form).
Classical proofs are proofs possibly using Excluded Middle (in some form). *" d" d" d*33"L C
(Intuitionistic Proofs are constructions)))We may interpret any intuitionistic proof of F as defining some construction of F, and therefore a program if F is 02formula.
Programs extracted from proofs in this way are usually very naive, but they are a starting point in order to design real programs.
Constructive interpretation of Heyting is a bridge between Mathematical proofs and applications.~d" dS dbClassical Proofs are not Heyting s constructions222There is no construction for Excluded Middle. Let A(x) = $yN.P(x,y) be any 01formula. By unfolding definition, there is some construction for the formula:
"xN. A(x) A(x)
if and only if there is some computable characteristic map in N for A(x) (i.e.: some f:NN such that f(x)=0 if and only if A(x) is true). But for some P, there is no computable characteristic map in N of A(x). " dZ" dZ" dZ233N3X@9Preliminary Conclusion Most Mathematical proofs are Classical. By what we said, apparently, such proofs define no program. Therefore they have no applicative interest.
This preliminary conclusion, however, is false. ." d9*`"Plan of the Talk BWe will define a relaxed notion of construction, obtained from Heyting s by replacing everywhere computable with limit computable .
With this new notion of construction there is a construction for Excluded Middle. Constructions of closed 02formulas still correspond to programs.
Before introducing limit computability, we give a quick account of what is known about extraction of programs from Classical Proofs.v" dZam0 2. A constructive content for Classical Logic11 1Call PA (Peano Arithmetic) Arithmetic with quantification over integers, Induction axiom for all formulas, and Excluded Middle.
Call HA (Heyting Arithmetic) PA without Excluded Middle.
Godel proved 02conservativity of PA w.r.t. HA: If B is a 02formula and PA proves B, then HA proves B. Besides, there is a computable map turning every proof of B in PA into a proof of the same B in HA " dZ
Classical proofs are programs If we interpret proofs in HA by constructions, 02conservativity implies that every proof in PA of a 02formula B = "xN. $yN. P(x,y) may be turned into a program f such that P(x,f(x)).
02conservativity is a bridge between Mathematics and applications.
However, this result has also some limitations, as we will see.E" d/3 7E\Some limitations of 02conservativity resultT/ /No intuitive explanation is given. How can classical proofs of 02statements be programs, if they use Excluded Middle, and there is no construction for Excluded Middle?
As a consequence, we miss a global understanding of the program we extract from a proof. This means that, if the program is naive, as usually is, we have no way of making it better. Therefore we have no real way of using it. " d#P
&,VA refinement of 02conservativity result \, ,xThe first refinement of 02conservativity is due to Griffin (around 1980).
Griffin defined a programming language in which classical proofs could both be written and executed: lambda calculus with Continuations.
Griffin s programming language was simplified by Parigot (lm calculus), and by Berardi (symmetric l calculus). Eventually Curien and Herbelin merged the last two calculus, defining symmetric lm calculus (possibly the best so far)." dZ&]&"Continuations and Classical Logic #! #There is a common idea underlying Griffin s calculus and those who came later: to interpret Excluded Middle by means of Continuations.
Let s be any computation. The continuations of s are some set of computation states M1, & , Mn, stored in the memory of s.
At any moment, s can store the current state E (or part of it) in the set of continuations._" d
%L_#
Backtracking 6At any moment, the computation s can either:
move from the current state E to the next state E (an ordinary step)
move to some state M1, & , Mn in the set of continuation (an exceptional step).
If Mi is some previous state of the computation, we call this second choice backtracking." d" dZ" d!Z3G`Continuations and simply typed lambda l calculus61
1We may add continuations to simply typed lambda l calculus by adding a constant C of type (F F), together with the rewrite rule
(C) E[C(M)] : False M(lx.E[x]) : False
The axiom schema (F F) is intuitionistically equivalent to Excluded Middle. This is the connection between C and Classical Logic.
The rule (C) say that M is a continuation: the computation of E can move to M. A copy of E, in the form lx.E[x], is saved as argument of M. E can added by M to the set of continuations of the computation.b" dZ8" dZS" dZ03 3333# =Y Advantagesof continuations Using continuations, we may describe stepbystep the evaluation of the classical program extracted from a proof.
Continuation are a major advance in extracting programs out of classical proofs." d$Disadvantagesof continuations 0Using continuations, we miss a global and intuitive understanding of the program.
This means we cannot rewrite naive programs in order to obtain efficient programs. In fact, we still cannot use them.
In the rest of the talk, we will outline a semantical constructive interpretations of classical proofs.J1" d#+
21! 3. Semantic of Classical Proofs "! "By a Tarski structure M for a language L we mean a set X, equipped with an equivalence relation ~, and, for each relation R and map f of L, some relation RM and some map fM, both compatible with ~.
A formula F of L is true in M if it is is true the formula obtained by replacing, in F, the symbol = with ~, and all symbols R, f with RM, fM.
A Tarski model of a theory T is a Tarski structure M for the language of T, such that all theorems of T are true in M." dZ y
!"#.Interpretation of a theory inside another one /. /A model of a theory T is the usual way of explaining the mathematica concepts of T.
An interpretation of a theory T inside a theory U defines some model M of T using predicates and maps of U, and proving in U that all theorem of T are true in the model.
An interpretation of a theory T inside a theory U is the usual way of explaining the mathematical concepts of T in term of the mathematical concepts of U.0" dZAn example of interpretation ^We may interpre the theory H of Hyperbolic Plane inside the theory E of the Euclidian plane.
The set of elements of H is some set of points of the Euclidean Plane. The equivalence relation is equality on the Euclidean Plane. Any geometrical operation or relation of H is defined through some geometrical operation or relation of the Euclidian Plane. _" d__,02sound models of PAHJA model M of PA is 02sound if all closed 02formula B = "xN. $yN. P(x,y) true in M are true in the usual sense:
for all nN there is some mN such that P(n,m)
If M, B are as above, then any intuitionistic proof that B is true in M provides some program f such that P(x,f(x)) for all xN.Vv" d/" d" d
B6&Interpreting PA inside HA We want to define an interpretation of PA inside HA, in order to interpret Excluded Middle as a construction in some structure.
This is no easy task. There are several impossibility results we have to turn around (see [1]).
We also want to get some intuitive explanation of the programs we extract from classical proofs.
Therefore we only consider 02sound models M of PA.dw" dZ]
wThe main result Let PA",$ be the variant of PA whose set of logical connectives is:
"i{1,& n}.Ai, $i{1,& n}.Ai,
"iP(i), $iN.P(i)
Theorem. There exists a 02sound interpretation M of PA",$ in HA.
We may interpret every step of every classical proof of PA by some construction in some model M, in such a way that a proof of a closed 02formula defines a program.~E" dZ=" dZ" dZ<3333333
f)l&The model M of PA in HA,
lM is the set of all iterated limits of integers, taken over List(N), the set of lists of integers.
Definition of M generalizes Hayashi s Limit Computable Mathematics [4], in which limits are taken over N, and M is defined in PA itself.
Limits over List(N) are intended to give a more accurate descriptions of computations hidden in classical proofs.
M is defined in HA in order to show we may completely describe EM in term of limits." dZ ._
H*Conclusion and Future Work Eventually, we switched to a semantical interpretation of classical proofs, looking for some intuitive understanding of the programs we can extract from them.
This is a work in progress. The model we found looks promising, but it should be checked against some relevant examples. We have also to implement the computations in the model in term of backtracking and continuation.
We are quite confident this is possible. " dZ* 4. Appendix. Intepreting HA +1EM in HA"+ &+We sketch the definition of the interpretation of PA in HA in a simple case: when EM is restricted to 1EM.
We define a structure we call N1 (see [3])
The same construction also produces some model of (n+1)EM out of any model of nEM.
A model of EM is obtained by defining a succession of models of 0EM, 1EM, 2EM, & , then taking the direct limit of them.Lh" d33hA notion of Computation State Let S = List(N) be the set of all finite lists of integers, ordered by prefix. We call the elements of s computation states.
Intuitively, s is a list of (codes of) pairs
<n1,"x.P1(x)>, & , <nk,"x.Pk(x)>
of some integer ni and some 01formulas "x.Pi(x).
If P=Pi and Pi(ni) is false, we know that "x.P(x) is false.
Otherwise we assume that "x.P(x) is true." dZ$" dZ3" dZg" dZ333333333&j(Dynamic Integers We call any L:SN a dynamic integer .
Intuitively, L(s) is an hypothesis about a value, depending on the hypothesis about 01formulas associated to the state
s = <n1,"x.P1(x)>, & , <nk,"x.Pk(x)>
If some hypothesis change, then L(s) can change. L(s) will be a convergent limit if
in any correct computation of L,
eventually L(s) stops changing 2" dZ," dZU" dZC" dZ}"
333333333UCe'A notion of Agent Let Pfin(N) be the set of all finite subsets of N.
We call any F:S Pfin(N) an agent of the computation.
Intuitively, F(s) is a set of elements of the same kind of those which are in the state s:
F(s) = {<n1,"x.P1(x)>, & , <nk,"x.Pk(x)>}
The agent F requires to add the set F(s) above to the state s of the computation." d." dR" d>}
333333333TF)A notion of Computation Let s be any recursive weakly increasing successions s0 s1 s2 & in S
We say that s is a computation of an agent F, or s:F for short, if, eventually, any element a of F(si) either drops out of F(si), or it is added to si.
Formally: s:F if, for all a,nN, there is some mn such that either aF(sm), or asm.
Remark that this definition describes a notion of parallel asyncronous computation." d6n3< 20Convergence and Equivalence of Dynamic Integers 101NLet F:S Pfin(N) be an agent, L, M:SN be dynamic integers. Abbreviate (L is convergent), (L, M are equivalent), with L, (L~M). Then we define:
F is a construction of L, or F:L for short, if for all computations s0 s1 s2 & of F, there is some nN such that L(sn)=L(sn+1).
F is a construction of (L~M) , or F:L~M for short, if for all computations s0 s1 s2 & of F, there is some nN such that L(sn) = M(sn).\" dZ" dZG*O*The Tarski structure N1>Let F:S Pfin(N), and L, M:SN. For any nN, define n:SN by n(s) = n for all sS.
L if F:L for some F
(L~M) if F: (L~M) for some F
N1 is the set of all convergent dynamic integers, with equivalence relation ~. Maps of N1 are all computable maps f:N1 N1 such that
f(L)(s) = f(L(s))(s) for all sS.W" d" d(" d(3333U333F,A construction for 1EM in N1 XfA characteristic map in N1 for a 01formula $yN.P(x,y) is any map f of N1 such that, for all xN1, f(x) ~ True if and only if P(x,y) is true for some yN1.
Maps of N1 are computable, yet they include characteristic maps for all 01formulas, and therefore some construction for 1EM.
Characteristic maps in N of 01formulas, usually, are not computable. This is no contradiction. Characteristic maps in N1 are such only up to ~.J" dZ&
0R3
%Bibliography
l[1] S. Berardi, Intuitionistic Completeness for First Order Classical Logic, J.S.L., vol 63, Number 1, March 1999.
[2] S. Berardi, Classical Logic as Limit Completion, MSCS, 15, 2004 (to appear).
[3] S. Berardi, A Model for D02maps within Intuitionistic Arithmetic, Techical Report, Turin University, 2004.7" dg#
&+`+Bibliography
[4] S. Hayashi and M. Nakata, Towards Limit Computable Mathematics , Types for Proofs and Programs, Springer LNCS, 125144, 2001.
[5] Y. Akama, S. Berardi, S. Hayashi, U. Kohlenbach, An Arithmetical Hierarchy of the Law of Excluded Middle and Related Principles , pp. 192201, 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 1417 July 2004, Turku, Finland, Proceedings." dZX" dZ'?5Pu/8,Pr?%>
!"#$%&'()Oh+'0HP
%Programming With NonRecursive Mapsestefano505@Z@gf@_
՜.+,D՜.+,\
Personalizzato(