Constructive Algebra and Verification
Thierry Coquand Henri Lombardi
Marie-Françoise Roy
5-10 january, 2003
Place
The meeting took place in the
Schloss Dagstuhl. It was the seminar Nš03021, and it has a web page in Dagstuhl.
You'll find there a complete list of participants and a group
picture.
General Presentation
The meeting was an attempt to bring together people from different
communities: constructive algebra, computer algebra, designers and
users of proof systems. Though the goals and interests are distinct,
the meeting revealed that there is a strong core of common interests,
the main one maybe the shared desire to understand in depth
mathematics concepts in connections with algorithms and proofs. An
interaction appears thus to be possible and fruitful. One outcome of
this week was the decision to create a European group under the
acronym MAP for "Mathematics, Algorithms, Proofs". As we said in
our proposal: "If there is enough common interests and good
interactions during the week, the Dagstuhl seminar could be the
starting point of a european proposal on the same topic, with more
ambitious goals." This is indeed what happened.
We would like at this point to thank the team of Schloss Dagtuhl. The
exceptional working conditions we enjoyed there played an important
rôle in the success of the meeting.
Summary of the meeting
Here are some common themes that emerged in the meeting on
constructive algebra and verifications. There is no attempt
to be exhaustive.
Certificates
A first common theme that emerged can be captured by the notion of
"certificate", and was exposed clearly by the talk of Arjeh Cohen.
This notion unifies some attempts to connect proof systems and
computer algebra systems, that were the topic of the talks of Loic Pottier and David Delahaye. The idea
is roughly that computer algebra should communicate mathematical data
together with a certificate, which represents the information
needed to complete a proof of correctness of the mathematical
data. This notion is reminiscent of the difference NP/P: it may
be hard to check that a formula is a tautology but it is easy to check
a proof. A simple example is provided by the gcd of two polynomials
P and Q. The computer system should communicate not only
the answer G, but also a certificate, that may be four
polynomials A,B,C,D such that AP+BQ = G, P=CG, Q=DG. To
find G may be hard, but to check these equalities is easy. A
more sophiscated example was the topic of the talk of Loic Pottier
(special cases of quantifier eliminations for reals), who had to
program in CAML his own version of a computer algebra algorithm in
order to get the desired certificates.
This notion of certificate is also closely connected to the talk of Helmut Schwichtenberg (common
to all interactive proof systems with explicit proof objects): a
starting point of such work is that while it is undecidable in general
whether a given program meets its specification. In contrast, it can
be checked easily by a machine whether a formal proof is correct. The
proof object itself can thus then be used as a certificate.
It is curious that a similar notion of certificate was used in the
talk of Dmitrii
Pasechnik. There, of course, the goal is completely different,
which is to provide interesting strong propositional proof systems
with lower bound results. Finally, the talk of Laureano Gonzalez-Vega
was concerned on the difficulty of computing algebraic certificates in
some geometrical statements in Real Algebraic Geometry.
Algorithms in Mathematics, via Proof Theory
A second theme is what one may call the relevance of classical
mathematics to algorithms. The talks of Henri Lombardi, Marie-Francoise Roy and Ulrich Kohlenbach showed, in very
different ways, that mathematical proofs that use a priori highly non
computational concepts, such as Zorn lemma, or compactness principles,
contain implicitely very interesting computational informations. The
talk of Ulrich Kohlenbach presented a way to extract implicit
informations in proofs, in such a way that one can even obtain new
theorems, surprising to the expert, from these informations (here in
the field of metric fixed point theory). One interesting topic is to
compare the two approaches: in Lombardi and Roy's talks, to use
techniques from geometric logic, and in Kohlenbach's talk, a
modification of Gödel's dialectica interpretation, that is
especially well suited to extract bounds from classical proofs. Ulrich
Kohlenbach said for instance that it should be interesting to use his
methods also for examples on algebra, where the dynamical method of
Lombardi-Roy has been used so far.
A general feeling, emerging from some talks and discussions, was that
the algorithms extracted by the dynamical method from a priori non
effective proofs, may give algorithms that are better (even feasible)
than the algorithms one can extract more straightforwardly from usual
constructive arguments. For instance, in usual constructive
mathematics, one requires to have a test of irreducibility for
polynomials. While such a test exists in some cases, there are usually
quite inefficient. The algorithm corresponding to a proof using this
test is thus a priori also inefficient. By contrast the algorithm
extracted from dynamical methods does not rely on such tests. It was
suggested by Henri Lombardi that some efficient algorithms may be
obtained in this way in number theory (dynamical theory of Dedekind
domains). Such claims, if they happen to be verified, are of
fundamental importance.
Progress on basics
Another theme is best expressed by one sentence taken from the
presentation of the seminar: "It is remarkable that in constructive
and computer algebra, progress in sophisticated algorithms often
implies progress on basics". This point was stressed in the talk of
Peter Paule on symbolic summation
for instance, who provided basic examples that would be welcome
additions to basic courses on calculus, and several time in
discussions, for instance for algebraic topology. Another example was
provided by the talk of Gilles
Dowek, who, motivated by a quite concrete problems in safety of
air trafic control, presented a new form of induction over real
numbers that may be interesting for presenting basic proofs in real
analysis.
Proof Systems and Computer Algebra Systems
A large part of the talks were concerned about connections between
computer algebra systems and proof systems. Peter Paule reminded us, with some
concrete examples, that people in proof system should be more aware of
the power of current computer algebra systems. The talks of Renaud Rioboo presented
a system aiming at combining proofs and computer algebra computations.
The talks of Clemens
Ballarin and Julio
Rubio supplemented the talk of Francis Sergeraert by presenting
an on-going attempt to use techniques from formal methods and
interactive proof checking to ensure the correctness of a large
sofware system for computations in algebraic topology. One
interesting conceptual connection emerged from the talk of Peter Paule, on the
concrete example of checking tables of equalities between special
functions, like for instance cos2x + sin2 x =
1.
(There is actually a NIST-DLMF project of creating a new Digital
Library of Mathematica Functions, and verification is an important
aspect of' this project.) What is done in computer algebra is a purely
algebraic model of the problem (here for instance using differential
algebra to show that the derivative of cos2x +
sin2 x is 0.) But there is a mismatch between
this representation and the representation of expressions as {\em
functions} of real or complex quantities. Typically, the functions may
have pôle, or may involve ambiguities. What interest primarily
the user of such tables is of course the interpretation of expressions
as functions. This suggests a natural place where proof systems may
complement computer algebra system. Such a connection appeared in the
talks of Loic
Pottier and David
Delahaye. The simplest example may be the provided by the equality
x · 1/x = 1. This equality is perfectly valid
from the computer algebra viewpoint, since it is interpreted in the
field of rational expressions (field of fractions of a polynomial
ring). Considered as a function 1/x has a pôle at
x=0 and the proof system will have to generate the condition
x non equal to 0.
Constructive Mathematics
Several talks were given on constructive mathematics. Francis
Sergereart presented a way to do algebraic topology constructively,
which is actually implemented in common lisp. Peter Schuster presented a
constructive definition of the notion of scheme, a basic concept in
modern algebraic geometry. There are probably deep connections between
this presentation, based on point-free topology, and the talks of Henri Lombardi and Hervé Perdry on
dynamical algebras, that would be interesting to explore further. The
talks of Erik
Palmgren and Jesper Carlström were about
Martin-Löf type theory. Type theory appears to be a potential
formalism in which several concepts that were presented at the
workshop could be elegantly expressed. Just to take one example, if we
succeed to express constructive algebraic topology, as presented by Francis Sergeraert,
in type theory, one would have an algorithm (in a functional
programming language) which is correct by construction, thus bypassing
the need of a formal verification a posteriori. In the present stage
however, this may seem utopic (probably the program obtained in this
way would be too inefficient), but this might be an interesting
project. The meeting ended by a talk of Bas Spitters on a constructive proof
of Peter-Weyl's theorem, and it would be interesting to explore
further the algorithmic ideas implicit in this proof.
Impact
The main positive surprise of the seminar was that communication is
possible, and in fact highly appreciated, bewteen quite distinct
fields of mathematics and computer science. One participant expressed
for instance his positive surprise to see in the same talk the name of
Jean-Pierre Serre, who made fundamental contributions in algebraic
topology, and the name of Turing, one of the founder of the
mathematical notion of algorithm. The participants were working in
different fields, but were all deeply interested in the
interconnections between mathematics, algorithms and proofs, and
several participants expressed the opinion that this combination of
different topics with a strong common interest allows for a rich
interaction. What was positive also was the emphasis, common to many
talks, that progress in sophisticated mathematics and algorithms often
implies progress on basics. This seminar was also a wellcome occasion
to have a beginning of a real dialogue between designers and users of
proof systems, and specialists in computer algebra and
mathematics. Such dialogues have already started in research groups
that were represented (Linz, Nijmegen, Paris VI) but the seminar
showed new unexpected research directions (proof theory, constructive
algebraic topology).
One outcome of this week was the decision to create a European group
under the acronym MAP for "Mathematics, Algorithms, Proofs".