|Current Workshop | Overview||Back | Home | Search ||
Mathematics: Algorithms and Proofs
Three aspects of exact computation
Abstract: Often algorithms for exact computation work with rewrite methods. Apart from traces or certification of the algorithm implementation itself, there is often little support for a proof of correctness of the result of a computation.
In this tutorial we will look at three instances:
1. Noncommutative polynomial ideals. We will discuss to what extent the Buchberger methods work to produce a Gröbner basis. We will also demonstrate how the package GBNP can be used to produce proofs by means of traces.
2. Automated proofs for graph non-isomorphisms. We will discuss elementary permutation group algorithms and their use for automatically producing proofs of the non-isomorphism of graphs.
3. Rewrite methods for algebras related to knots. We will discuss Tits’ rewrite rules for the symmetric groups and how to extend those to the Brauer algebras. These rewrite rules not only solve the word problem for monomials in the Brauer algebra but also lead to a computational model for the Birman-Murakami-Wenzl algebra, which is used to define the knot invariant known as the Kauffman polynomial. The interesting aspect of the rewrite rules is that they give a normal form that is unique only up to certain homogeneous rewrite rules.
Thierry Coquand (Chalmers)
A logical approach to abstract algebra
Abstract: We shall survey recent works on constructive mathematics, mainly in algebra. These works can be seen as a realisation of Hilbert’s program for a non trivial subset of contemporary abstract algebra. We shall try to precise the connections with point-free topology. Another topic of discussion will be the connections with Kronecker’s approach to algebra.
Per Martin-Löf (
Topos Theory and Type Theory
Abstract: My purpose is to relate type theory to topos theory by taking the concept of model of type theory to be the counterpart of the notion of elementary topos. Projective and inductive limits of comma (or slice) models of type theory will then be considered.
Algorithms and Proofs in Geometry
Abstract: The 48 two-dimensional
Dirk van Dalen (Utrecht University)
The lonely revolutionary. Brouwer’s first program.
Abstract: Rather against the wishes of his Ph.D. adviser Brouwer decided to make his dissertation the starting point for a new foundation of mathematics. It clearly contained the gems of his later work, but it needed a more systematic approach to turn it into a viable program. We will look into the ideas and doubts that led the way to his mature 1918 program. Details from his pre-dissertation notebooks will be helpful to see how Brouwer managed to find a foothold in the much discussed foundations of mathematics around the turn of the century.
Hendrik Lenstra (Universiteit Leiden)
Abstract: This lecture considers a fundamental problem in the algorithmic theory of ordered fields from a complexity point of view.
Thorsten Altenkirch (
Quotient Types in Observational Type Theory
Abstract: In recent work with Conor McBride we have developed Observational Type Theory (OTT) a variant of Martin-Löf Type Theory, which has
an extensional propositional equality while at the same time retaining the computational desirable features of Intensional Type Theory: decidability of
definitional equality and type checking and cononicity, i.e. that every closed term reduces to a value. OTT is currently being implemented as the core of
the Epigram 2 system.
In the present talk I shall focus on the potential of using quotient types in OTT, which among other applications enables us to define
Cauchy Reals. When programming with Reals in Type Theory we exploit the partiality monad (based on recent work with Tarmo
definable in (total) OTT and which enables us to program computationally useful functions over the Reals.
Jesus Aransay (La Rioja)
A mechanised proof of the Basic Perturbation Lemma
Abstract: We present a complete mechanized proof of the result in Homological Algebra known as Basic Perturbation Lemma. The proof carried out in the proof assistant Isabelle, more concretely, in the implementation of Higher Order Logic (HOL) available in the system. Difficulties found, and also on the ongoing stages of our project to give a certified version of some of the algorithms present in the Kenzo computation
Eyvind Briseid (
Using proof mining to find computable rates of convergence for the Picard iteration sequence for non-nonexpansive functions.
Abstract: We show how one in certain cases through a novel application of logical metatheorems for functional analysis, developed by Gerhardy and Kohlenbach, can find computable rates of convergence for the Picard iteration sequence for non-nonexpansive selfmaps of metric spaces. This gives an explanation in logical terms for recent results in metric fixed point theory, where we found highly uniform explicit rates of convergence for certain classes of not necessarily nonexpansive selfmaps of metric spaces.
Jan Draisma (Technische Universiteit Eindhoven)
A scenic tour in tropical geometry
Abstract: Tropical geometry is geometry over the ‘tropical semiring’: the real numbers extended with infinity, endowed with ‘tropical addition’, which is taking the minimum, and ‘tropical multiplication’, which is ordinary addition. Tropical geometry has at least the following three different aspects:
1. It is a tool for solving problems in ordinary algebraic geometry. A famous result of this flavour is Mikhalkin’s work on counting plane curves of given genus g and degree d passing through 3d+ g −1 general points. I myself have a nice application of tropical geometry to secant varieties.
2. Tropicalisation takes objects that are important in ‘ordinary’ mathematics to polyhedral objects that often turn out to be interesting in a (seemingly) different area of mathematics. For instance, tropical matrix multiplication gives an algorithm for computing shortest paths in graphs, the tropical Grassmannian parametrises phylogenetic trees and (a part of) the tropical orthogonal group TOn parametrises n-point metric spaces.
3. Tropical geometry has lots of computational aspects: e.g., how does one compute a tropical basis for an ideal? Can tropical geometry help in computing
ideals for varieties given by a parametrisation?
In this talk (based on work of Sturmfels, Speyer, Gathmann, Markwig, Mikhalkin, Einsiedler, Kapranov, Lind, and others — including myself) I give
examples of each of these aspects.
Gilles Dowek (l’École polytechnique)
The linear-algebraic lambda-calculus (joint work with Pablo Arrighi)
Abstract: We present a minimal programming language combining lambda-calculus and linear algebra. This language is nothing else than the lambdacalculus together with the possibility to make linear combinations of terms (alpha t + beta u). We describe how to execute programs in this language by a few rewrite rules. These rules must be carefully chosen to avoid some paradoxes arising when mixing simplification rules (of linear algebra) with infinities (of lambda-calculus). We mention the perspectives of this work in field of quantum computation.
Harold Edwards (
Addition on Elliptic Curves
Abstract: The addition operation on an elliptic curve (with a base point) is normally described today geometrically in terms of lines intersecting a nonsingular cubic. The algebraic formulas for this operation are cumbersome. Euler’s very first paper on elliptic functions indicated a simple explicit formula for the addition operation on the specific elliptic curve y2 = x4 − 1, and Gauss’s posthumous papers include essentially the same formula. The talk will show that a generalization of Euler’s (and Gauss’s) formula applies to arbitrary elliptic curves, giving a more algorithmic description of the addition and a clear explanation of the j-invariant of an elliptic curve.
Peter Hancock (
Stream Processing, a la Brouwer (Joint work with Neil Ghani and Dirk Pattinson)
Abstract: Continuous functions between streams of discrete values have an intensional representation by coinductive-inductive data structures. Composition of such functions is also representable, by a straightforward operation on their representatives. This may be of interest for data-flow programming. The ideas extend to continuous maps between final coalgebras for a broad class of functors.
Assia Mahboubi (INRIA/MSR)
A formal correctness proof for the subresultant algorithm
Abstract: We describe here a formal proof in the Coq system of the structure theorem for subresultants, which allows to give a formal correctness proof of our implementation of the subresultants algorithm. This algorithm allows to compute gcds of multivariate polynomials with coefficients in a ring efficiently.
The algorithm is simple and widely implemented in computer algebra systems, but the correctness proof is very technical. Up to our knowledge it is the first mechanized proof of this result. We will try to sum up the difficulties of such a formal proof and to point out the decisive steps in this formal development.
Sean McLaughlin (CMU)
A Methodology for Implementing Reusable Decision Procedures
Abstract: Implementing decision procedures for verification tools such as proof assistants and SMT tools can be a major effort. Currently, many different implementations of the same decision procedures exist, or the algorithms only exist for a particular system, and not for others. This is not a good division of labor among the verification community. This talk describes an experimental methodology for designing implementations of decision procedures that can easily be used in multiple systems regardless of implementation language or logical foundation. We also give some (very) preliminary results.
Henri Lombardi (
Constructive real algebra.
Abstract: By ‘real algebra’ we understand here ‘algebraic properties of real numbers’, i.e., properties of real numbers w.r.t. + , − , × , > , _ , max , min , _From a constructive point of view, real algebra is far away from the theory of discrete real closed fields (which was settled by Artin in order to understand real algebra in the framework of classical logic). Most algorithms given in the discrete case fail without sign test. But some do have a good constructive version, e.g., Hilbert’s 17th Problem.
Related topics are the following:
1) Investigating real algebra should be a way of understanding what happens when dropping dependent choice in constructive analysis.
2) Understanding real algebra should be also a first important step for obtaining a constructive version of O-minimal structures.
Russell O’Connor (
Abstract: According to Wikipedia, ‘analysis is the branch of mathematics [...] concerned with the limit process or the concept of convergence.’ These operations take place in spaces that are complete. It is sometimes thought that these spaces are ‘too big’ to be represented by computers, but this is not entirely true. Bishop and Bridges develop an entirely constructive (and hence computational) version of analysis in their seminal work entitled ‘constructive analysis’. This talk will discuss how to implement, in a practical way, analytical concepts such as the real numbers, compact sets, and integrable
functions all in the same way by considering the completion operation as a monad. A monad is a powerful abstract data structure that has been used to implement things from IO to non-determinism in functional languages such as Haskell.
Paulo Oliva (Queen
Modified realizability of classical linear logic
Abstract: It is well-known that the marriage of realizability interpretations with classical logics are not always smooth. One often needs to go through different proofs translations (such as the negative translation and the A-translation) in order to get some useful computational content from proofs. The situation, however, is quite different in the case of classical linear logic (CLL). In this talk I will present a simple and direct modified realizability interpretation of CLL. The interpretation is closely related to de Paiva and Hyland’s categorical interpretations of the propositional fragment of CLL from the early 90’s, and Shirahata’s recent extension of that work dealing with quantifiers. I will show that, given the standard embedding of intuitionistic logic (IL) into CLL, the combined interpretation of IL indeed coincides with Kreisel’s 1962 original interpretation. Time permitting, I will also discuss about an interesting extension of CLL required for the completeness of the interpretation.
Grant Olney Passmore (
Mechanized Theory Development for Formal Computation and Proof in Elementary Algebraic Theories with Small Models
Abstract: We describe a mechanized methodology for the rapid development of formal computational algebra systems within the ACL2 theorem prover. Given a finitely axiomatized elementary theory admitting at least one small* finite model, we show how the model checker MACE4, the firstorder theorem prover Prover9, the TPTP library, and the encapsulation mechanism of ACL2 may all be utilized in tandem to rapidly obtain a conservative extension of the Boyer-Moore logic enriched with deep, formally derived theorems useful to the field of study. We then show how a mathematically natural representation of models may be obtained through a lan- guage of generators and relations, and how through functional instantiation one may perform formally verified computations upon such models that are more trustworthy than similar procedures found in mainstream computer algebra systems.
Finally, the methodology is illustrated in practice through the construction of Steppenwolf-2, a system for formal computational group theory.
Peter Paule (Research
Institute for Symbolic Computation (RISC), J.
A Computer Proof of a Conjecture of Moll
Abstract: Around 2000, Victor Moll, within the context of definite integration, met a specialized family of Jacobi polynomials. He conjectured that the corresponding coefficient sequences are log-concave. In joint work with Manuel Kauers, we settled Moll’s conjecture by a non-trivial usage of computer algebra. - Background information about the conjecture can be found in Moll, Notices of the AMS 49 (2002), 311-317.
Ana Romero Ibañez (Rioja)
Constructive Spectral Sequences
Abstract: Spectral Sequences are a useful tool in Algebraic Topology providing information on homology groups, but they are not real algorithms except in some particular cases. On the contrary, the effective homology method provides algorithms for the computation of homology groups of complicated spaces, and in particular it allows to determine the homology groups of some spaces related to the most common spectral sequences, those of Serre and Eilenberg-Moore. In this talk, we explain how the effective homology technique can also be used to obtain, as a by-product, an algorithm computing every component of the corresponding spectral sequence, in particular the groups Ep,qr , the higher differentials dp,qr , the limit groups Ep,q1 , the filtration
at abutment Hp,q of Hp,q satisfying Ep,q1 = Hp,q/Hp−1,q−1, and also the smallest r stabilizing Ep,qr for p + q given. These methods have been concretely implemented as an extension of the Kenzo computer program.
Peter Schuster (
Labelled Trees of Finite Depth (joint work with Hervé Perdry)
Abstract: We consider the condition that every non-increasing finitely branching tree labelled by a poset has finite depth. As a property of the poset under consideration, it follows from Richman and Seidenberg’s chain condition precisely when the generalised fan theorem holds. Applications of the finite-depth property include the termination of the algorithm producing the mimimal primes over an ideal in a Noetherian ring.
Helmut Schwichtenberg (Munich)
Goedels Dialectica Interpretation
Abstract: We give a presentation of Goedels Dialectica Interpretation based on natural deduction with assumption variables. In this setting the proof of the soundness theorem is particularly perspicious. We then discuss the usability of this approach for machine extraction of computational content from classical existence proofs
Bas Spitters (
Located and overt locales (jww Thierry Coquand)
Abstract: Locatedness is one of the fundamental notions in constructive mathematics. The existence of a positivity predicate on a locale, i.e. the locale being overt, or open, has proved to be fundamental in locale theory in a constructive, or topos theoretic, context. We show that the two notions are intimately connected. A locale is overt when it is located ‘in itself’. A compact sublocale is located when it is overt.
In this talk we will proceed slowly and make connections to the theory of compact sets by Bishop which O’Connor is implementating in Coq.