Transcript continuations

Continuations,
Backtracking and Limits:
a notion of ‘‘Construction’’
for Classical Logic
(Ongoing work)
Kyoto, November 2004
Stefano Berardi, Semantic of Computation group
C.S. Dept., Turin University, http://www.di.unito.it/~stefano
Abstract of the talk
• We describe Classical Principles in term of
‘‘constructions’’, of a general kind, learning a
value by trial-and-error, 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.
2
§ 1. Heyting’s notion
of construction
• Heyting 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.
An 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 = F1F2, then a construction r of F is any pair
<i,s>, with i{1,2}, and s construction of Fi.
• If F = F1F2, then a construction r of F is any pair
<r1,r2>, with r1 construction of F1, and r2
construction of F2.
An inductive definition of a
construction for a formula F
• If F = xI.G(x), then a construction r of F is
any computable map
f :I{constructions of G(x), for some xI}
such that, for all xI, f(x) is a construction of G(x).
• If F = x.G(x), a construction r of F is a pair
<i,s>, with iI, and s construction of G(i).
An inductive definition of a
construction for a formula F
• If F = F1F2, 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.
0n- and 02-formulas
• 0n-formulas are all formulas
A(x1, x2, …) = x1N. x2N. … . P(x1, x2, …)
with n alternating quantifiers, starting with , and
with P decidable.
• 0n-formulas are all formulas
B(x1, x2, …) = x1N. x2N. … . P(x1, x2, …)
with n alternating quantifiers, starting with , and
with P decidable.
Constructions as programs
• By unfolding definitions, a construction r for a
closed 02-formula B = xN. yN. P(x,y)
provides some map f, satisfying P(x,f(x)) for all
xN.
• If we think of B as a specification, a construction
for B provides some program f satisfying the
specification B.
Intuitionistic and Classical Proofs
• EM (Excluded Middle) is the axiom schema
xN. A(x)  A(x)
• n-EM is the axiom schema EM restricted to 0nformulas.
• Intuitionistic proofs are all proofs not using
Excluded Middle (in any equivalent form).
• Classical proofs are proofs possibly using
Excluded Middle (in some form).
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 02-formula.
• 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.
Classical Proofs are not
Heyting’s constructions
• There is no construction for Excluded Middle. Let
A(x) = yN.P(x,y) be any 01-formula. By
unfolding definition, there is some construction
for the formula:
xN. A(x)  A(x)
if and only if there is some computable
characteristic map in N for A(x) (i.e.: some
f:NN 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).
Preliminary 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.
Plan of the Talk
• We 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 02-formulas still correspond to
programs.
• Before introducing limit computability, we give a
quick account of what is known about extraction
of programs from Classical Proofs.
§ 2. A constructive content
for Classical Logic
• Call 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 02-conservativity of PA w.r.t. HA:
‘‘If B is a 02-formula 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’’
Classical proofs are programs
• If we interpret proofs in HA by constructions,
02-conservativity implies that every proof in PA
of a 02-formula B = xN. yN. P(x,y) may
be turned into a program f such that P(x,f(x)).
• 02-conservativity is a bridge
Mathematics and applications.
between
• However, this result has also some limitations, as
we will see.
Some limitations of
02-conservativity result
• No intuitive explanation is given. How can
classical proofs of 02-statements 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.
A refinement of
02-conservativity result
• The first refinement of 02-conservativity 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 (–calculus), and by Berardi
(symmetric – calculus). Eventually Curien and
Herbelin merged the last two calculus, defining
symmetric –calculus (possibly the best so far).
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  be any computation. The continuations of 
are some set of computation states M1, …, Mn,
stored in the memory of .
• At any moment,  can store the current state E (or
part of it) in the set of continuations.
Backtracking
•
At any moment, the computation  can either:
1. move from the current state E to the next state
E’ (an ordinary step)
2. 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.
Continuations and simply typed
lambda –calculus
• We may add continuations to simply typed lambda –
calculus by adding a constant C of type (F  F),
together with the rewrite rule
(C)
E[C(M)] : False

M(x.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 x.E[x], is saved as argument of M. E can added by
M to the set of continuations of the computation.
Advantages
of continuations
• Using continuations, we may describe step-bystep the evaluation of the classical program
extracted from a proof.
• Continuation are a major advance in extracting
programs out of classical proofs.
Disadvantages
of continuations
• Using 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.
§ 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.
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.
An 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.
02-sound models of PA
• A model M of PA is 02-sound if all closed 02formula B = xN. yN. P(x,y) true in M are
true in the usual sense:
for all nN there is some mN 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 xN.
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 02-sound models M
of PA.
The main result
• Let PA, be the variant of PA whose set of
logical connectives is:
i{1,…n}.Ai,
iP(i),
i{1,…n}.Ai,
iN.P(i)
• Theorem. There exists a 02-sound 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.
The model M of PA in HA
• M 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.
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.
§ 4. Appendix. Intepreting
HA +1-EM in HA
• We sketch the definition of the interpretation of
PA in HA in a simple case: when EM is restricted
to 1-EM.
• 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 n-EM.
• A model of EM is obtained by defining a
succession of models of 0-EM, 1-EM, 2-EM, …,
then taking the direct limit of them.
A 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 01-formulas x.Pi(x).
1. If P=Pi and Pi(ni) is false, we know that x.P(x)
is false.
2. Otherwise we assume that x.P(x) is true.
Dynamic Integers
• We call any L:SN a “dynamic integer”.
• Intuitively, L(s) is an hypothesis about a value,
depending on the hypothesis about 01-formulas
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”
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.
A notion of Computation
• Let  be any recursive weakly increasing
successions s0  s1  s2  … in S
• We say that  is a computation of an agent F, or
:F for short, if, eventually, any element a of F(si)
either drops out of F(si), or it is added to si.
• Formally: :F if, for all a,nN, there is some
mn such that either aF(sm), or asm.
• Remark that this definition describes a notion of
parallel asyncronous computation.
Convergence and Equivalence
of Dynamic Integers
•
Let F:S  Pfin(N) be an agent, L, M:SN be
dynamic integers. Abbreviate (L is convergent),
(L, M are equivalent), with L, (L~M). Then
we define:
1. F is a construction of L, or F:L for short, if
for all computations s0  s1  s2  … of F, there
is some nN such that L(sn)=L(sn+1).
2. 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 nN such that L(sn) = M(sn).
The Tarski structure N1
•
Let F:S  Pfin(N), and L, M:SN. For any
nN, define nº:SN by nº(s) = n for all sS.
1. L
if
2. (L~M) if
F:L
for some F
F: (L~M)
for some F
3. 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 sS.
A construction for 1-EM in N1
•
A characteristic map in N1 for a 01-formula
yN.P(x,y) is any map f of N1 such that, for
all xN1, f(x) ~ Trueº if and only if Pº(x,y) is
true for some yN1.
•
Maps of N1 are computable, yet they include
characteristic maps for all 01-formulas, and
therefore some construction for 1-EM.
•
Characteristic maps in N of 01-formulas,
usually, are not computable. This is no
contradiction. Characteristic maps in N1 are
such only up to ~.
Bibliography
[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 02-maps within
Intuitionistic Arithmetic, Techical Report, Turin
University, 2004.
Bibliography
[4] S. Hayashi and M. Nakata, “Towards Limit
Computable Mathematics”, Types for Proofs
and Programs, Springer LNCS, 125--144, 2001.
[5] Y. Akama, S. Berardi, S. Hayashi, U.
Kohlenbach, “An Arithmetical Hierarchy of the
Law of Excluded Middle and Related
Principles”, pp. 192-201, 19th IEEE
Symposium on Logic in Computer Science
(LICS 2004), 14-17 July 2004, Turku, Finland,
Proceedings.