Dagstuhl Seminar Proceedings, Volume 5021
Dagstuhl Seminar Proceedings
DagSemProc
https://www.dagstuhl.de/dagpub/1862-4405
https://dblp.org/db/series/dagstuhl
1862-4405
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
5021
2006
https://drops.dagstuhl.de/entities/volume/DagSemProc-volume-5021
05021 Abstracts Collection – Mathematics, Algorithms, Proofs
From 09.01.05 to 14.01.05, the Dagstuhl Seminar 05021 ``Mathematics, Algorithms, Proofs'' was held in the International Conference and Research Center (IBFI),
Schloss Dagstuhl.
During the seminar, several participants presented their current
research, and ongoing work and open problems were discussed. Abstracts of
the presentations given during the seminar as well as abstracts of
seminar results and ideas are put together in this paper. The first section
describes the seminar topics and goals in general.
LinkstFo extended abstracts or full papers are provided, if available.
Constructive mathematics
computer algebra
proof systems
1-15
Regular Paper
Thierry
Coquand
Thierry Coquand
Henri
Lombardi
Henri Lombardi
Marie-Françoise
Roy
Marie-Françoise Roy
10.4230/DagSemProc.05021.1
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
05021 Executive Summary – Mathematics, Algorithms, Proofs
This workshop was the third MAP meeting,
a continuation of the seminar "Verification and constructive algebra" held in Dagstuhl from 6 to 10 January 2003.
The goal of these meetings is to bring together people from the communities of formal proofs, constructive
mathematics and computer algebra (in a wide meaning).
The special
emphasis of the present meeting was on the constructive mathematics and efficient proofs in computer algebra.
Constructive mathematics
computer algebra
proof systems
1-3
Regular Paper
Thierry
Coquand
Thierry Coquand
10.4230/DagSemProc.05021.2
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
A dynamical solution of Kronecker's problem
In this paper,
I present a new decision procedure for the ideal
membership problem for polynomial rings over principal domains
using discrete valuation domains. As a particular case, I solve a
fundamental algorithmic question in the theory of multivariate
polynomials over the integers called ``Kronecker's problem", that
is the problem of finding a decision procedure for the ideal
membership problem for $mathbb{Z}[X_1,ldots, X_n]$. The
techniques utilized are easily generalizable to Dedekind domains.
In order to avoid the expensive complete factorization in the
basic principal ring, I introduce the notion of ``dynamical
Gr"obner bases" of polynomial ideals over a principal domain. As
application, I give an alternative dynamical solution to
``Kronecker's problem".
Dynamical GrÃƒÂ¶bner basis
ideal membership problem
principal domains
1-9
Regular Paper
Ihsen
Yengui
Ihsen Yengui
10.4230/DagSemProc.05021.3
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
A Nilregular Element Property
An element or an ideal of a commutative ring is nilregular if and only if
it is regular modulo the nilradical. We prove that if the ring is
Noetherian, then every nilregular ideal contains a nilregular element. In
constructive mathematics, this proof can then be seen as an algorithm to
produce nilregular elements of nilregular ideals whenever the ring is coherent,
Noetherian, and discrete. As an application, we give a constructive proof of
the Eisenbud--Evans--Storch theorem that every algebraic set in
$n$--dimensional affine space is the intersection of $n$ hypersurfaces.
The input of the algorithm is an arbitrary finite list of polynomials,
which need not arrive in a special form such as a Gr"obner basis.
We dispense with prime ideals when defining concepts or carrying out proofs.
Lists of generators
polynomial ideals
Krull dimension
Zariski topology
commutative Noetherian rings
constructive algebra
1-6
Regular Paper
Thierry
Coquand
Thierry Coquand
Henri
Lombardi
Henri Lombardi
Peter
Schuster
Peter Schuster
10.4230/DagSemProc.05021.4
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
Abel and the Concept of the Genus of a Curve
This talk is about the treatement of the Genus of a Curve by Abel, following the book "Essays in Constructive Mathematics".
Constructive Mathematics
1-2
Regular Paper
Harold M.
Edwards
Harold M. Edwards
10.4230/DagSemProc.05021.5
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
Approximate fixed points of nonexpansive functions in product spaces
In this talk, we present another case study in the general program of proof mining in fixed point theory. Thus, we generalize results obtained by W. Kirk in the theory of approximated fixed points of nonexpansive mappings in product spaces
Proof mining
fixed point theory
approximated fixed points
nonexpansive functions
product spaces
1-5
Regular Paper
Ulrich
Kohlenbach
Ulrich Kohlenbach
Laurentiu
Leustean
Laurentiu Leustean
10.4230/DagSemProc.05021.6
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
Certified mathematical hierarchies: the FoCal system
The focal language (formerly Foc) allows a
programmer to incrementally build mathematical
structures and to formally prove their
correctness. focal encourages a development
process by refinement, deriving step-by-step
implementations from specifications. This
refinement process is realized using an
inheritance mechanism on structures which can mix
primitive operations, axioms, algorithms and
proofs. Inheritance from existing structures allows to reuse their components under some
conditions, which are statically checked by the compiler.
In this talk, we first present the main
constructions of the language. Then we show a
shallow embedding of these constructions in
the Coq proof assistant, which is used to check
the proofs made in Focal. Such a proof can be
either an hand-written Coq script, made in an
environment set up by the Focal compiler, or a
Coq term given the zenon theorem prover, which is partly developped within Focal. Last, we present a formalization of focal structures and show that the Coq embedding is conform to this model.
Specifications
proofs
inheritance
refinement
types
Focal
Coq
computer algebra
mathematics
1-12
Regular Paper
Virgile
Prevosto
Virgile Prevosto
10.4230/DagSemProc.05021.7
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
Coequalisers of formal topology
We give a predicative construction of quotients of formal topologies. Along with earlier results on the match up between of continuous functions on real numbers (in the sense of Bishop's constructive mathematics) and approximable mappings on the formal space of reals, we argue that formal topology gives an adequate foundation for constructive algebraic topology, also in the predicative sense. Predicativity is of essence when formalising the subject in logical frameworks based on Martin-LÃƒÂ¶f type theories.
Formal topology
type theory
1-12
Regular Paper
Erik
Palmgren
Erik Palmgren
10.4230/DagSemProc.05021.8
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
Constructive algebraic integration theory without choice
We present a constructive algebraic integration theory. The theory is constructive in the sense of Bishop, however we avoid the axiom of countable, or dependent, choice. Thus our results can be interpreted in any topos. Since we avoid impredicative methods the results may also be interpreted in Martin-LÃƒÂ¶f type theory or in a predicative topos in the sense of Moerdijk and Palmgren.
We outline how to develop most of Bishop's theorems on integration theory that do not mention points explicitly. Coquand's constructive version of the
Stone representation theorem is an important tool in this process. It is also used to give a new proof of Bishop's spectral theorem.
Algebraic integration theory
spectral theorem
choiceless constructive mathematics
pointfree topology
1-13
Regular Paper
Bas
Spitters
Bas Spitters
10.4230/DagSemProc.05021.9
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
Constructive Proofs or Constructive Statements?
A question raised at previous MAP meetings is
the following. Is Sergeraert's "Constructive
Algebraic Topology" (CAT, in short) really
constructive (in the strict logical sense of the
word "constructive")? We have not an answer to
that question, but we are interested in the
following: could have a positive (or negative)
answer to the previous question an influence in
the problem of proving the correctness of CAT
programs (as Kenzo)?
Studying this problem, we have observed that, in
fact, many CAT programs can be extracted from
the statements (that is, from the specification
of certain objects and constructions), without
needing an extraction from proofs. This remark
shows that the logic used in the proofs is
uncoupled with respect to the correctness of
programs. Thus, the first question posed could
be quite irrelevant from the practical point of
view. These rather speculative ideas will be
illustrated by means of some elementary
examples, where the Isabelle code extraction
tool can be successfully applied.
Program extraction
symbolic computation
constructive logic
1-4
Regular Paper
Julio
Rubio Garcia
Julio Rubio Garcia
10.4230/DagSemProc.05021.10
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
Diagrammatic logic and exceptions:an introduction
For dealing with computational effects in computer
science, it may be helpful to use several logics:
typically, a logic with implicit effects for the
language, and a more classical logic for the user.
Hence, the study of computational effects should
take place in a framework where distinct logics
can be related. In this paper, such a framework is
presented: it is a category, called the category
of propagators. Each propagator defines a kind of
logic, called a diagrammatic logic, which is
endowed with a deduction system and a sound notion
of models. Morphisms of propagators provide the
required relationships between diagrammatic
logics. The category of propagators has been
introduced by Duval and Lair in 2002, it is based
on the notion of sketches, which is due to
Ehresmann in the 1960's. Then, the paper outlines
how Duval and Reynaud in 2004 used the category of
propagators for dealing with the computational
effect of raising and handling exceptions. Another
application of diagrammatic logic is presented by
Dominguez et al. in the same conference
Specifications
Semantics
Exceptions
Sketches
Diagrammatic Logic
Extensive Categories
Monads.
1-0
Regular Paper
Dominique
Duval
Dominique Duval
Jean-Claude
Reynaud
Jean-Claude Reynaud
10.4230/DagSemProc.05021.11
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
Enabling conditions for interpolated rings
If A is a subring of a ring B, then an interpolated ring is the union of A and {b in B : P} for some proposition P. These interpolated rings come up frequently in the construction of Brouwerian examples. We study conditions on the inclusion of A in B that guarantee, for some property of rings, that if A and B both have that property, then so does any interpolated ring. Classically, no condition is necessary because each interpolated ring is either A or B. We also would like such a condition to be necessary in the sense that if it fails, and every interpolated ring has the property, then some omniscience principle holds.
Brouwerian example
interpolated ring
intuitionistic algebra
1-7
Regular Paper
Fred
Richman
Fred Richman
10.4230/DagSemProc.05021.12
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
Generalized metatheorems on the extractability of uniform bounds in functional analysis
Recently U.Kohlenbach proved general metatheorems for the extraction of (uniform) bounds from classical
proofs in functional analysis. The proof was based on
a combination of GÃƒÂ¶del's functional interpretation
and Bezem's strong majorization relation. We present
a generalization of the majorization relation which
allows to generalize Kohlenbach's metatheorems
significantly. Finally, we will discuss some examples
which are now covered by the new metatheorems.
Proof mining
majorization
1-5
Regular Paper
Philipp
Gerhardy
Philipp Gerhardy
Ulrich
Kohlenbach
Ulrich Kohlenbach
10.4230/DagSemProc.05021.13
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
Henselian Local Rings: Around a Work in Progress
I shall outline an elementary and effective construction of the Henselization of a local ring (which could be implemented in some computer algebra systems) and an effective proof of several classical results about Henselian local rings.
Local rings
henselian local rings
1-8
Regular Paper
Hervé
Perdry
Hervé Perdry
Mariemi
Alonso
Mariemi Alonso
Henri
Lombardi
Henri Lombardi
10.4230/DagSemProc.05021.14
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
Introduction to My Book "Essays in Constructive Mathematics"
The talk will describe the overall approach and the major topics of the book, recently published by Springer.
Constructive Mathematics
Galois Theory
Genus of a Curve.
1-2
Regular Paper
Harold M.
Edwards
Harold M. Edwards
10.4230/DagSemProc.05021.15
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
Introduction to the Flyspeck Project
This article gives an introduction to a long-term project called Flyspeck, whose purpose is to give a formal verification of the Kepler Conjecture. The Kepler Conjecture asserts that the density of a
packing of equal radius balls in three dimensions cannot exceed $pi/sqrt{18}$.
The original proof of the Kepler Conjecture, from 1998, relies extensively on computer calculations. Because the proof relies on relatively few external results, it is a natural choice for a formalization effort.
Certified proofs
Kepler conjecture
1-11
Regular Paper
Thomas C.
Hales
Thomas C. Hales
10.4230/DagSemProc.05021.16
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
Programming and certifying a CAD algorithm in the Coq system
A. Tarski has shown in 1948 that one can perform quantifier elimination in the theory of real closed fields. The introduction of the Cylindrical Algebraic Decomposition (CAD) method has later allowed to design rather feasible algorithms. Our aim is to program a reflectional decision procedure for the Coq system, using the CAD, to decide whether a (possibly multivariate) system of polynomial inequalities with rational coefficients has a solution or not. We have therefore
implemented various computer algebra tools
like gcd computations, subresultant polynomial or Bernstein polynomials.
Computer algebra
Bernstein polynomials
subresultants
CAD
Coq
certification.
1-18
Regular Paper
Assia
Mahboubi
Assia Mahboubi
10.4230/DagSemProc.05021.17
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
Proving Bounds for Real Linear Programs in Isabelle/HOL
Linear programming is a basic mathematical technique for optimizing a
linear function on a domain that is constrained by linear inequalities.
We restrict ourselves to linear programs on bounded domains that involve only
real variables. In the context of theorem proving, this restriction makes it
possible for any given linear program to obtain certificates from external
linear programming tools that help to prove arbitrarily precise bounds for the
given linear program. To this end, an explicit formalization of matrices
in Isabelle/HOL is presented, and how the concept of lattice-ordered rings
allows for a smooth integration of matrices with the axiomatic type classes of
Isabelle.
As our work is a contribution to the Flyspeck project, we demonstrate that via
reflection and with the above techniques it is now possible to prove bounds
for the linear programs arising in the proof of the Kepler conjecture
sufficiently fast.
Certified proofs
Kepler conjecture
1-2
Regular Paper
Steven
Obua
Steven Obua
10.4230/DagSemProc.05021.18
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
Some Notes On ``When is 0.999... equal to 1?
In joint work Robin Pemantle and I (2004) consider a doubly infinite sum which is not equal to 1, as first suspected, but evaluates to a sum of products of values of the zeta function. Subsequently, I report on this project.
Symbolic summation
computer algebra
proofs
harmonic numbers
zeta-relations
1-3
Regular Paper
Carsten
Schneider
Carsten Schneider
10.4230/DagSemProc.05021.19
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
Subdiscriminant of symmetric matrices are sums of squares
We present a very elementary algebraic proof providing an explicit sum of squares.
This result generalizes a result on discriminants of symmetric matrices
due to Ilyushechkin
and proved also by P. Lax.
Real algebra
sums of squares
subdiscriminants
1-4
Regular Paper
Marie-Françoise
Roy
Marie-Françoise Roy
10.4230/DagSemProc.05021.20
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
Towards a Verified Enumeration of All Tame Plane Graphs
In his proof of the Kepler conjecture, Thomas Hales introduced the notion of tame graphs and provided a Java program for enumerating all tame plane graphs. We have translated his Java program into an executable function in HOL ("the generator"), have formalized the notions of tameness and planarity in HOL, and have partially proved that the generator returns all tame plane graphs. Running the generator in ML has shows that the list of plane tame graphs ("the archive") that Thomas Hales also provides is complete. Once we have finished the completeness proof for the generator.
In addition we checked the redundancy of the archive by formalising an executable notion of isomorphism between plane graphs, and checking if the archive contains only graphs produced by the generator. It turned out that 2257 of the 5128 graphs in the archive are either not tame or isomorphic to another graph in the archive.
Kepler conjecture
certified proofs
flyspeck
1-25
Regular Paper
Tobias
Nipkow
Tobias Nipkow
Gertrud
Bauer
Gertrud Bauer
10.4230/DagSemProc.05021.21
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
Towards Diagrammatic Specifications of Symbolic Computation Systems
The aim of this work is to present an ongoing project to
formalize, in the framework of diagrammatic logic (due to
Dominique Duval and Christian Lair) some data structures appearing
in Sergeraert's symbolic computation systems Kenzo and EAT. More
precisely, we intend to translate into the diagrammatic setting a
previous work based on standard algebraic specification
techniques. In particular, we give hints on the reason why an
important construction (called imp construction) in the
specification of the systems can be understood as a freely
generating functor between suitable categories of diagrammatic
realizations. Even if very partial, these positive results seem to
indicate that this new kind of specification is promising in the
field of symbolic computation.
Specification
symbolic computation
sketches
diagrammatic logic
1-23
Regular Paper
César
Dominguez
César Dominguez
Dominique
Duval
Dominique Duval
Laureano
Lamban
Laureano Lamban
Julio
Rubio Garcia
Julio Rubio Garcia
10.4230/DagSemProc.05021.22
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
Unifying Functional Interpretations
The purpose of this article is to present a parametrised functional interpretation. Depending on the choice of the two parameters one obtains well-known functional interpretations, among others GÃƒÂ¶del's Dialectica interpretation, Diller-Nahm's variant of the Dialectica interpretation, Kreisel's modified realizability, Kohlenbach's monotone interpretations and Stein's family of functional interpretations. We show that all these interpretations only differ on two basic choices, which are captured by the parameters, namely the choices of (1) "how much" of the counter-examples for A becomes witnesses for the negation of A, and of (2) "how much" information about the witnesses of A one is interested in.
Functional interpretation
modified realizability
Dialectica interpretation
intuitionistic logic
1-20
Regular Paper
Paulo
Oliva
Paulo Oliva
10.4230/DagSemProc.05021.23
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode