Slides
Several objects can be associated to a list of vectors with =
integer=0A=
coordinates: among others, a family of tori called toric arrangement,=0A=
a convex polytope called zonotope, a function called vector partition=0A=
function; these objects have been described in a recent book by De=0A=
Concini and Procesi. The linear algebra of the list of vectors is=0A=
axiomatized by the combinatorial notion of a matroid; but several=0A=
properties of the objects above depend also on the arithmetics of the=0A=
list. This can be encoded by the notion of a "matroid over=0A=
Z". Similarly, applications to tropical geometry suggest the=0A=
introduction of matroids over a discrete valuation ring. Motivated by=0A=
the examples above, we introduce the more general notion of a "matroid=0A=
over a commutative ring R". Such a matroid arises for example from a=0A=
list of elements in a R-module. When R is a Dedekind domain, we can=0A=
extend the usual properties and operations holding for matroids (e.g.,=0A=
duality). We can also compute the Tutte-Grothendieck ring of matroids=0A=
over R; the class of a matroid in such a ring specializes to several=0A=
invariants, such as the Tutte polynomial and the Tutte=0A=
quasipolynomial. We will also outline other possible applications and=0A=
open problems.=0A=
=0A=
(Joint work with Alex Fink).=0A=
Anders M=C3=B6rtberg and Cyril Cohen: Formalizing =
elementary=20
divisor rings in Coq
An elementary divisor ring is a commutative ring where every matrix =
is=0A=
equivalent to a matrix in Smith normal form. It is well known that=0A=
principal ideal domains are elementary divisor rings, but it is an=0A=
open problem whether the generalization to B=C3=A9zout domains, rings =
where=0A=
every finitely generated ideal is principal, are elementary divisor=0A=
rings or not. We have formalized, using the Coq proof assistant=0A=
together with the SSReflect extension, different extension that we can=0A=
extend B=C3=A9zout domains with in order to show that they are =
elementary=0A=
divisor rings. The extensions we have considered are: existence of a=0A=
gdco operation, adequacy, Krull dimension less than or equal to 1 and=0A=
rings where strict divisibility is well-founded.=0A=
Grant Passmore: Exact global optimization on=20
demand
Joint work with Leonardo de Moura of Microsoft Research, Redmond.=0A=
=0A=
We present a method for exact global nonlinear optimization based on a=0A=
real algebraic adaptation of the conflict-driven clause learning=0A=
(CDCL) approach of modern SAT solving. This method allows polynomial=0A=
objective functions to be constrained by real algebraic constraint=0A=
systems with arbitrary boolean structure. Moreover, it can correctly=0A=
determine when an objective function is unbounded, and can compute=0A=
exact infima and suprema when they exist. The method requires=0A=
computations over real closed fields containing infinitesimals=0A=
(cf. [1]).=0A=
=0A=
References:=0A=
1. Leonardo de Moura and Grant Olney Passmore. Computation in Real=0A=
Closed Infinitesimal and Transcendental Extensions of the Rationals.=0A=
In Proceedings of the 24th International Conference on Automated=0A=
Deduction (CADE) (2013)=0A=
Claude Quitt=C3=A9: Playing with monomials of =
k[X_1, =E2=80=A6,=20
X_n]
The context is the graded resolution of monomial ideals of k[X_1, =
=E2=80=A6,=0A=
X_n], where k is a field. The speaker wishes to explain carefully some=0A=
experiments which led him to understand parts of the correspondance=0A=
between the monomial world and the simplicial world. In particular :=0A=
Stanley-Reisner correspondance, various "fine-grading" syzygies=0A=
formulas (Hochster, Bayer-Charalambous-Popescu), Alexander duality,=0A=
etc. Tools: algebraic and simplicial Koszul complexes.=0A=
Christophe Raffalli: Hilbert's 17th problem via=20
cut-elimination
Hilbert's seventeen problem, solved by Artin, says that every =
positive=0A=
polynomial can be written as a sum of squares of rational=0A=
fraction. Since Artin, effective proof have been given by Lombardi -=0A=
Roy - Perrucci for the latest one which give a bound to the degree as=0A=
a tower of five exponentials.=0A=
=0A=
We will see how such a proof can be presented as a result of cut=0A=
elimination, showing that replacing model theory by proof theory is a=0A=
possible method to make a result effective.=0A=
=0A=
The main contribution of our work is the fact that we implemented the=0A=
procedure and we introduced a notion of PBDD that requires smaller=0A=
degrees, making it possible to extract the wanted equalities yet only=0A=
for the simplest positive polynomials (which was not possible before=0A=
from such an effective proof).=0A=
Ana Romero: Spectral sequences for computing =
persistent=20
homology
Slides=
DIV>
A filtration of the object to be studied is the heart of both =
subjects=0A=
persistent homology and spectral sequences; in the talk I will present=0A=
the complete relation between them, focusing on constructive and=0A=
algorithmic points of views. By using some previous programs for=0A=
computing spectral sequences, we obtain persistent homology programs=0A=
applicable to spaces not of finite type (provided they are spaces with=0A=
effective homology) and with Z-coefficients (significantly=0A=
generalizing the usual presentation of persistent homology over a=0A=
field).=0A=
Peter Schuster: Eliminating Krull's Lemma for =
Horn=20
Clauses
Scarpellini [3] has characterised algebraically when in =
classical=0A=
logic a certain kind of propositional geometric implication in the=0A=
language of rings can be proved for commutative rings and for integral=0A=
domains, respectively. By interpolation, we extend this=0A=
characterisation to the provability of such implications for reduced=0A=
rings: that is, commutative rings in which 0 is the only nilpotent=0A=
element.=0A=
=0A=
The characterisation above implies that the theory of integral domains=0A=
is conservative for Horn clauses over the theory of reduced rings.=0A=
This allows to eliminate Krull's Lemma for commutative rings from some=0A=
of the so- called short and elegant proofs in commutative algebra in=0A=
which the general case is reduced to the special case by reduction=0A=
modulo a generic prime ideal. The method applies, in particular, to=0A=
the example studied in [1, 2, 4]: that the non-constant coecients of=0A=
an invertible polynomial are all nilpotent.=0A=
=0A=
1. Henrik Persson. An application of the constructive spectrum of a=0A=
ring. In Type Theory and the Integrated Logic of Programs. Chalmers=0A=
University and University of Goeteborg, 1999. PhD thesis.=0A=
=0A=
2. Fred Richman. Nontrivial uses of trivial=0A=
rings. Proc. Amer. Math. Soc.,103(4):1012-1014, 1988.=0A=
=0A=
3. Bruno Scarpellini. On the metamathematics of rings and integral=0A=
domains. Trans. Amer. Math. Soc., 138:71-96, 1969.=0A=
=0A=
4. Peter Schuster. Induction in algebra: a first case study. In 2012=0A=
27th Annual ACM/IEEE Symposium on Logic in Computer Science, pages=0A=
581-585. IEEE Computer Society Publications, 2012. Proceedings, LICS=0A=
2012, Dubrovnik, Croatia, June 2012. Journal version: Log. Methods=0A=
Comput. Sci. (3:20) 9 (2013).=0A=
Francis Sergeraert: Spectral Sequences =
downgraded to=20
elementary Gauss Reductions
The standard Spectral Sequences of Algebraic Topology had =
been=0A=
downgraded 25 years ago by Julio Rubio to the Basic Perturbation=0A=
Lemma, an "elementary" result of homological algebra, in fact=0A=
relatively complex. The talk is devoted to a reduction of this=0A=
"lemma" to elementary Gauss reductions, already known by the=0A=
Babylonians, combined with the invertibility of 1-x when |x| < 1.=0A=
Bas Spitters: Constructive algebra and geometric=20
mathematics
Vickers observed that predicative techniques from formal topology =
are=0A=
often preserved under pullbacks of geometric morphisms. This provides=0A=
a clear technical advantage to such constructions. Constructive=0A=
algebra, as developed by Coquand and Lombardi provides another=0A=
important application.=0A=
=0A=
I will provide a short overview of some recent such results in=0A=
analysis, mostly based on our recent article:=0A=
=0A=
Bas Spitters, Steven Vickers, and Sander Wolters - Gelfand spectra in=0A=
Grothendieck toposes using geometric mathematics, 1310.0705, 2013.=0A=
under revision for QPL 2012 post-proceedings in EPTCS.=0A=
=0A=
http://www.cs.ru.nl/~spitters/geoBS.pdf=0A=
Claire T=C3=AAte: Depth, dimension and resolution in =
Commutative=20
Algebra
First we introduce two fondamental tools in the theory of depth: =
the=0A=
Koszul complex and the Cech complex for a finite sequence (a_1,=E2=80=A6 =
,a_n)=0A=
in a commutative ring. We give some cohomological properties of these=0A=
complexes. By using some basic examples, we try to make explicit the=0A=
links between depth, Krull dimension and resolutions. At the end we=0A=
illustrate a celebrated Serre theorem characterizing regular rings by=0A=
existence of finite projective resolutions: we explain THE resolution=0A=
of the ideal of a point of an hypersurface.=0A=
Xavier Caruso, David Roe and Tristan Vaccon: =
Tracking p-adic=20
precision
Slides=
DIV>
We present a new method to propagate p-adic precision in =
computations,=0A=
which also applies to other ultrametric fields. We illustrate it with=0A=
many examples and give a toy application to the stable computation of=0A=
the SOMOS 4 sequence. Our methods relies on elementary ultrametric=0A=
calculus and can either be applied on the fly or as a preparatory=0A=
step.=0A=
Marc Giusti and Jean-Claude Yakoubsohn: =
Multiplicity=20
hunting and approximating multiple roots of polynomial systems
The computation of the multiplicity and the approximation of =
isolated=0A=
multiple roots of polynomial systems is a difficult problem.=0A=
=0A=
In recent years, there has been an increase of activity in this area.=0A=
Our goal is to translate the theoretical background developed in the=0A=
last century on the theory of singularities in terms of computation=0A=
and complexity.=0A=
=0A=
This paper presents several different views that are relevant to=0A=
address the following issues : predict the multiplicity of a root=0A=
and/or determine the number of roots in a ball, approximate fast a=0A=
multiple root and give complexity results for such problems. We=0A=
propose a new method to determine a regular system, called equivalent=0A=
but deflated, i.e., admitting the same root as the initial singular=0A=
one.=0A=
=0A=
Finally, we perform a numerical analysis of our approach.=0A=
Noam Zeilberger: Refining the meaning of =
types
Complete the following sequence:=0A=
=0A=
* number theorists study numbers=0A=
* group theorists study groups=0A=
* knot theorists study knots=0A=
* type theorists study ___=0A=
=0A=
Many mathematicians would hesitate at giving the obvious answer,=0A=
because of their inability to explain just what "types" are. Instead=0A=
they might point to a bunch of different papers where various formal=0A=
systems are studied, and conclude that "type theorists study type=0A=
theories".=0A=
=0A=
I believe that an important reason for this lack of consensus is that=0A=
in practice, types are actually used with two very different=0A=
intuitions in mind, corresponding to the distinction the late John=0A=
Reynolds termed "intrinsic" versus "extrinsic" [1]. For several=0A=
years, Paul-Andr=C3=A9 Melli=C3=A8s and I have been =
developing a=0A=
category-theoretic approach to type theory that aims to reconcile=0A=
these two opposing intuitions, the essence of which may be explained=0A=
by the following simple idea: just as any category may be viewed (=C3=A0 =
la=0A=
Lambek) as a deductive system (supporting composition of deductions),=0A=
any *functor* may be viewed as a type system (supporting composition=0A=
of typing derivations). Our approach is closely related to (and partly=0A=
inspired by) an idea which appears in the type-theoretic literature=0A=
under the heading of "refinement", developed especially by Frank=0A=
Pfenning and his students. In the talk, I will begin by giving a=0A=
partial survey of the work on type refinement and some of the=0A=
practical motivations behind it. Then I will introduce our abstract=0A=
definition of a type (refinement) system, and describe various ways it=0A=
can be used.=0A=
=0A=
=0A=
1. John C. Reynolds, "The Meaning of Types -- From Intrinsic to=0A=
Extrinsic Semantics", BRICS Report Series RS-00-32, December=0A=
2000. Available from http://www.brics.dk/RS/00/32/=0A=
------=_NextPart_000_0000_01D1462F.BD948710
Content-Type: text/css;
charset="iso-8859-1"
Content-Transfer-Encoding: quoted-printable
Content-Location: http://perso.crans.org/cohen/map2014/css/default.css
body {
margin: 0px auto; width: 700px; color: black; font-family: verdana; =
font-size: 18px;
}
div#content {
text-align: justify;
}
div#content h1 {
text-align: center;
}
div#content table {
width: 700px;
}
div#content pre {
font-size: 15px;
}
div#header {
padding: 12px 0px; margin-bottom: 30px; border-bottom-color: red; =
border-bottom-width: 2px; border-bottom-style: solid;
}
div#logo a {
color: black; font-size: 18px; font-weight: bold; text-decoration: =
none; float: left;
}
div#header #navigation {
text-align: right;
}
div#header #navigation a {
color: black; text-transform: uppercase; font-size: 16px; font-weight: =
bold; text-decoration: none; margin-left: 12px;
}
div#footer {
padding: 12px 0px; text-align: right; color: rgb(85, 85, 85); =
font-size: 12px; margin-top: 30px; border-top-color: red; =
border-top-width: 2px; border-top-style: solid;
}
h1 {
font-size: 24px;
}
h2 {
font-size: 20px;
}
div.info {
color: rgb(85, 85, 85); font-size: 14px; font-style: italic;
}
.schedule {
border: 2px solid black; border-image: none; border-collapse: collapse;
}
.schedule td {
border: 1px solid black; border-image: none;
}
.time {
width: 160px;
}
.who {
width: 200px; text-align: left;
}
.talk {
width: 440px; text-align: left;
}
.talk a {
text-decoration: none;
}
------=_NextPart_000_0000_01D1462F.BD948710
Content-Type: application/octet-stream
Content-Transfer-Encoding: quoted-printable
Content-Location: http://openfontlibrary.org/face/grundschrift
@font-face {
font-family: GrundschriftBold;
src: =
url(/assets/fonts/grundschrift/34791c82d6efc31c7344cb450c4a2c1c/3349e8178=
4a7d0d0390648bf807b669a/GrundschriftBold.otf) format("opentype");
font-weight: bold;
font-style: normal;
}
@font-face {
font-family: GrundschriftKontur;
src: =
url(/assets/fonts/grundschrift/34791c82d6efc31c7344cb450c4a2c1c/640f409e0=
9f210c6e9696b26cfc3951f/GrundschriftKontur.otf) format("opentype");
font-weight: normal;
font-style: normal;
}
@font-face {
font-family: GrundschriftNormal;
src: =
url(/assets/fonts/grundschrift/34791c82d6efc31c7344cb450c4a2c1c/d3fa37979=
cd87a8e5e7eeec4d386d5aa/GrundschriftNormal.otf) format("opentype");
font-weight: normal;
font-style: normal;
}
@font-face {
font-family: GrundschriftPunkt;
src: =
url(/assets/fonts/grundschrift/34791c82d6efc31c7344cb450c4a2c1c/5084732bd=
96eabfe0bfeb11347c222fd/GrundschriftPunkt.otf) format("opentype");
font-weight: normal;
font-style: normal;
}
@font-face {
font-family: GrundschriftRegular;
src: =
url(/assets/fonts/grundschrift/c118292e03bce13629cacdfbafbb084d/66a2c543f=
aff2aca0eb5774cb9714f25/GrundschriftRegular.otf) format("opentype");
font-weight: normal;
font-style: normal;
}
@font-face {
font-family: Grundschrift;
src: =
url(/assets/fonts/grundschrift/34791c82d6efc31c7344cb450c4a2c1c/3349e8178=
4a7d0d0390648bf807b669a/GrundschriftBold.otf) format("opentype");
font-weight: bold;
font-style: normal;
}
@font-face {
font-family: Grundschrift;
src: =
url(/assets/fonts/grundschrift/34791c82d6efc31c7344cb450c4a2c1c/640f409e0=
9f210c6e9696b26cfc3951f/GrundschriftKontur.otf) format("opentype");
font-weight: normal;
font-style: normal;
}
@font-face {
font-family: Grundschrift;
src: =
url(/assets/fonts/grundschrift/34791c82d6efc31c7344cb450c4a2c1c/d3fa37979=
cd87a8e5e7eeec4d386d5aa/GrundschriftNormal.otf) format("opentype");
font-weight: normal;
font-style: normal;
}
@font-face {
font-family: Grundschrift;
src: =
url(/assets/fonts/grundschrift/34791c82d6efc31c7344cb450c4a2c1c/5084732bd=
96eabfe0bfeb11347c222fd/GrundschriftPunkt.otf) format("opentype");
font-weight: normal;
font-style: normal;
}
@font-face {
font-family: Grundschrift;
src: =
url(/assets/fonts/grundschrift/c118292e03bce13629cacdfbafbb084d/66a2c543f=
aff2aca0eb5774cb9714f25/GrundschriftRegular.otf) format("opentype");
font-weight: normal;
font-style: normal;
}
------=_NextPart_000_0000_01D1462F.BD948710
Content-Type: application/octet-stream
Content-Transfer-Encoding: quoted-printable
Content-Location: http://openfontlibrary.org/face/freeuniversal
@font-face {
font-family: FreeUniversalBold;
src: =
url(/assets/fonts/freeuniversal/5077bdf47767ac210dd15ea83870df66/7952a9d9=
16c9338fb6cbbaa6f70c630c/FreeUniversalBold.ttf) format("truetype");
font-weight: bold;
font-style: normal;
}
@font-face {
font-family: FreeUniversalBoldItalic;
src: =
url(/assets/fonts/freeuniversal/5077bdf47767ac210dd15ea83870df66/e2619057=
037d5bcee341cf86b4bfd55a/FreeUniversalBoldItalic.ttf) =
format("truetype");
font-weight: bold;
font-style: italic;
}
@font-face {
font-family: FreeUniversalItalic;
src: =
url(/assets/fonts/freeuniversal/5077bdf47767ac210dd15ea83870df66/d435b9e2=
7ac6476c1c5d009830de9fdd/FreeUniversalItalic.ttf) format("truetype");
font-weight: normal;
font-style: italic;
}
@font-face {
font-family: FreeUniversalRegular;
src: =
url(/assets/fonts/freeuniversal/5077bdf47767ac210dd15ea83870df66/0ae90cb4=
327d4bce8721841d9bb80a7e/FreeUniversalRegular.ttf) format("truetype");
font-weight: normal;
font-style: normal;
}
@font-face {
font-family: FreeUniversal;
src: =
url(/assets/fonts/freeuniversal/5077bdf47767ac210dd15ea83870df66/7952a9d9=
16c9338fb6cbbaa6f70c630c/FreeUniversalBold.ttf) format("truetype");
font-weight: bold;
font-style: normal;
}
@font-face {
font-family: FreeUniversal;
src: =
url(/assets/fonts/freeuniversal/5077bdf47767ac210dd15ea83870df66/e2619057=
037d5bcee341cf86b4bfd55a/FreeUniversalBoldItalic.ttf) =
format("truetype");
font-weight: bold;
font-style: italic;
}
@font-face {
font-family: FreeUniversal;
src: =
url(/assets/fonts/freeuniversal/5077bdf47767ac210dd15ea83870df66/d435b9e2=
7ac6476c1c5d009830de9fdd/FreeUniversalItalic.ttf) format("truetype");
font-weight: normal;
font-style: italic;
}
@font-face {
font-family: FreeUniversal;
src: =
url(/assets/fonts/freeuniversal/5077bdf47767ac210dd15ea83870df66/0ae90cb4=
327d4bce8721841d9bb80a7e/FreeUniversalRegular.ttf) format("truetype");
font-weight: normal;
font-style: normal;
}
------=_NextPart_000_0000_01D1462F.BD948710--