The 2006 map meeting was held from January 9th (monday) to January 13th (friday), 2006, in Castro Urdiales, Spain.
Lodging and meals took place at the hotel Las Rocas.
In this edition the organization of MAP was sligthly different to the three previous years. Mornings were devoted to invited talks and tutorials. So, the number of contributed talks decreased considerably with respect to previous MAPs. As a consequence, the selection process was more strict. The Scientific Committee tried to keep a trade-off among the different areas with representation in the MAP community. Please, don't consider a non acceptation as a critic to the quality of your work: it is an issue more related to the balance of topics.
Nevertheless, the number of participants in this edition was equivalent to previous MAPs. You were all welcome.
The invited speakers were:
Furthermore, four tutorials were held:
Here you shall find the slides of the talks which were given in this MAP meeting. The title is in gray if no file has been provided yet. By alphabetical order:
We present quantitative versions of some fixed point theorems for contractive type mappings on metric spaces. These are derived with the help of insights and techniques from proof mining. In one case our version is also a qualitative improvement compared to known theorems.
Title: Symbolic Computation: Self-application of Algorithmic Mathematics Author: Bruno Buchberger Abstract: We explain our view that mathematics, in some sense, is essentially symbolic computation. In recent years, with the advent of modern computer technology, this view becomes more and more concrete: Mathematics is always pursued, at the same time, at the object level (exploring mathematical theories) and on the meta-level (observing how theory exploration can be systematized and, maybe, made algorithmic). In the talk we give four examples of techniques used in current systems, like Theorema, for the automation of mathematical theory exploration: computation and proving within the same logic system; the reduction of logical proving to solving in algebraic domains; the use of formula schemes for the invention of definitions, propositions, problems, and algorithms; and the automated generation of conjectures from failing proofs. We finally draw some conclusions about how such systems will change the way how we do mathematical research, how we review, assess, store, and retrieve mathematical knowledge, how we teach, and how we apply mathematics.
Dynamic Galois theory and Splitting Fields
Our main aim with this talk is to introduce a dynamic constructive Galois Theory which allows us to obtain a representation of the splitting field of a separable polynomial over a field. We present some methods which are giving a constructive substitute for the classical splitting field, which does not work when there is no factorization algorithm. With our methodology, we're trying to combine the dynamic evaluation techniques (D5) introduced by Della Dora, Dicrescenzo and Duval with the fantastic Galois theory.
Based on finite cases of the double-negation shift, essentially iterations of "(not not A & not not B) -> not not (A &B)", we compare the functional interpretation of the full double-negation shift using Spector's bar-recursion with the modified realizability of the full double-negation shift.
Will Algebraic Geometry Rescue Program Verification? Deepak Kapur Department of Computer Science University of New Mexico Albuquerque, NM, USA Three different approaches for automatically generating polynomial relations as loop invariants are presented. A method based on quantifier-elimination seems particularly promising since it works for programs with nested loops and procedure calls, as well as it admits numerous heuristics; the use of an incomplete method for quantifier-elimination does not produce an incorrect invariant but rather, a weak invariant. The other two approaches use ideal-theoretic semantics of simple programming language constructs. Polynomial invariants form an ideal which (or its approximations) can be computed using algebraic geometry tools. The approaches are illustrated using a variety of examples. The critical role of algebraic geometry in discovering these results is discussed. It is proposed that equally rich theories about other data structures will have to be developed in order to make progress in automatically generating program invariants expressed in terms of properties of such data structures.
In recent years (though influenced by papers of G. Kreisel going back to the 50's) an applied form of proof theory systematically evolved which sometimes is called `Proof Mining'. A particularly fruitful area of applications of proof theory in mathematics has been numerical and nonlinear functional analysis. This 4-part course gives a survey on the logical foundations of this approach and its applications in analysis.
We present another case study in the general project of proof mining in functional analysis, developed by Kohlenbach. Thus, we obtain a quadratic bound on the rate of asymptotic regularity for the Krasnoselski-Mann iterations of nonexpansive mappings in CAT(0)-spaces, whereas previous results guarantee only exponential bounds.
Computer Algebra, Proving, and the Digital Library of Mathematical Functions
Control Theory (tutorial in four parts)
The purpose of this tutorial is to give a short introduction to control theory (transfer functions/matrices, internal/strong/simultaneous/robust stabilization, parametrization of all stabilizing controllers, optimization problems) within an algebraic analysis approach (fractional ideals, lattices, module theory, homological algebra, Banach algebras).
(Joint work with David Delahaye)
We propose a decision procedure for algebraically closed fields based on a
quantifier elimination method. The procedure is intended to build proofs for
systems of polynomial equations and inequations. We describe how this
procedure can be carried out in a proof assistant using a Computer Algebra
system in a purely skeptical way. We present an implementation in the
particular framework of Coq and Maple giving some details regarding the
interface between the two tools. This allows us to show that a Computer
Algebra system can be used not only to bring additional computational power to
a proof assistant but also to enhance the automation of such tools.
We present a new possible definition for a constructive treatment of Noetherian Rings: the Fan-Noetherian rings; and a meta-theorem on the conditions on a poset which are well suited to provide a constructive theory for Noetherian Rings.
Effective Positivstellensatz
In this conference we present our experience using the ACL2 system to verify computer algebra. First we give a short introduction to the formal verification of programs and the use of theorem provers as a tool for this task. Then, we present a short overview to the ACL2 system, used by our reserch group in Seville to carry out formal verification, and we try to motivate why we think it is suitable for formal verification of symbolic computation systems. Finally we show an example: the formal proof in ACL2 of Dickson's lemma, in the context of the development of a formally verified Common Lisp implementation of Buchberger algorithm.
It is folklore that if a continuous equation has approximate solutions and - in a quantitative manner - at most one solution, then it has a (of course, uniquely determined) exact solution. I first review the standard ways to validate this heuristic principle both in classical mathematics and in constructive mathematics with countable choice, and then indicate how this can be carried over to the choice-free way of doing completions put forward by Mulvey, Stolzenberg, Richman, et al. Moreover, I sketch how the crucial "at most one" hypothesis can be obtained, by invoking Brouwer's fan theorem, from appropriate preconditions of a qualitative nature. In fact, the fan theorem is equivalent to the general validity of the implication from the qualitative to the quantitative uniqueness condition for continuous functions on a compact metric space.
Title : Program Extraction from Normalization Proofs
Abstract: We formalize the standard proof (using computability
predicates) of the existence of normal forms for terms of the simply
typed lambda-calculus. Then we machine-extract a program from this
proof, which turns out to implement the well-known normalization by
evaluation algorithm.
Constructive Algebraic Topology (tutorial in four parts)
Abstracts of F. Sergeraert's Castro-Urdiales talks.
A tutorial about "Constructive Algegraic Topology" was required.
The subject has been naturally divided into four parts.
Castro-1: Combinatorial Topology. The standard simplicial complexes
are not enough for good algebraic topology, the so-called simplicial
*sets* are necessary. Castro-1 is an expository presentation of the
subject with the simplest examples. For serious references, question
Google with "Peter May simplicial objects" and "Goerss Jardine
simplicial theory".
Castro-2. Homological algebra. Devoted to *one* typical example
explaining why standard homological algebra is not effective. The
best reference for elementary homological algebra probably is
MacLane, "Homological Algebra". The talk terminates with the subtle
definitions of effective chain complexes and locally effective chain
complexes.
Castro-3. Effective homology. Combining the notions of effective and
locally effective chain complexes, and the so-called Basic
Perturbation Lemma, an easy and efficient solution is obtained for
Constructive Algebraic topology. The simple example of the effective
homology version of the Serre spectral sequence is used. See also
Google(Rubio Sergeraert Bulletin) in which other more precise
references can be obtained.
Castro-4. An informal exposition about the hard but interesting
problems which are met when the theoretical methods of effective
homology are to be *concretely* implemented on a computer. The
programming context is quite new and leads to numerous exciting
problems.
In my talk I present some new algorithms for unimodular completion over multivariate polynomial rings with coefficients in an infinite fields and or a Noetherian ring containing an infinite field and in which Gröbner bases can be computed. I also show how such algorithms are important in signal processing.
Title: Diagrammatic Specifications of Symbolic Computation Systems
Authors: C. Domínguez, D. Duval, L. Lambán and J. Rubio
Abstract
The aim of this work is to describe the current state of an ongoing
project to formalize, within 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. In a previous work, we gave some hints on the reason why a
key construction (called imp construction) in the specification
of the systems can be understood as a freely generating functor
between suitable categories of diagrammatic realizations. Now, we
will focus on the new open lines, giving a few details on the
problems we have encountered up to now.
Symbolic Computation of A_\infty-structures: (Abstract) In the framework of Effective Algebraic Topology, we are interested in the computation of A-infinity structures. In this poster, we would like to show wich type of pitfalls we had to solve. Thanks to the basic perturbation lemma and the tensor trick, from theorical viewpoint it is possible to obtain the morphisms involved in such structures with the help of a computer. But the problems appear when we translate this mathematical notion to computational world. For short, only two specific problems are explained in this poster: how to solve infinite loops and the extension of class family!
When we study the structure of nonunital rings, they appear some categories of modules over them, one of those is the category of firm modules, i.e. modules $M$ such that the multiplication $R \otimes_R M \to M$ is an isomorphism. The ring itself uses not to be firm, but there is always a special family of firm modules that generates all the others. Those special modules are built from infinite graphs that describe the module structure. Similar patterns in different graphs generate module homomorphisms. Those are the only possible morphisms in some important cases. In order to represent those infinite graphs on a computer, we also need that some basic patterns are repeated. This family is dense and very useful in order to compute morphisms. We represent them and give an algorithm which says when two of such graphs represent isomorphic modules.
Spectral Sequences are a useful tool in Algebraic Topology providing information on homology groups by successive approximations from the homology of appropriate associated complexes. However, they are not real algorithms except in exceptional cases. On the contrary, the effective homology method provides a real algorithm for the computation of homology groups of complicated spaces. In this poster, we explain how the effective homology method can also be used for the computation of spectral sequences. A set of programs has been developed, allowing the user to calculate the whole set of components of spectral sequences associated to filtered complexes.