International Center for workshops in the Sciences
| Current Workshop | Overview | Back | Print | Home | Search | | |||||||
 |
| |||||||
 | ||
|
Tutorials Arjeh Cohen
(Technische Universiteit 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. Invited talks Michael Beeson Algorithms and Proofs
in Geometry Abstract: The 48 two-dimensional
constructions of 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) Ordering fields Abstract: This lecture considers
a fundamental problem in the algorithmic theory of ordered fields from a
complexity point of view. Contributed talks 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 system. 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 ( Implementing Analysis 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
Mary, 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. [Back] |