« Constructivisme et extraction de programmes »
Rencontre de l'ACI GEOCAL
Le 25 novembre 2004, Per Martin-Löf (Stockholm) recevra le titre de
Docteur Honoris Causa de
l'Université de la
Méditerranée.
À l'occasion de sa venue à Marseille, l'ACI GEOCAL
organise une rencontre dont le thème général est «
constructivisme et extraction de programmes ». Cette rencontre
aura lieu sur le Campus de Luminy les deux jours précédant la
remise officielle du titre de Docteur Honoris Causa à Per
Martin-Löf.
Très informelle, cette rencontre consistera en une série d'exposés
donnés par des orateurs invités dont les travaux ont, ou ont eu, des
liens profonds avec les contributions fondamentales de Per Martin-Löf à la
logique et à l'informatique théorique (intuitionisme, théorie des types...).
Ces exposés porteront sur des sujets liés au constructivisme et à
l'extraction de programme, mais pas uniquement. Notre motivation est bien
moins l'homogénéité thématique que l'espoir de voir surgir des discussions
(controverses ?) parmi l'auditoire et les orateurs.
L'organisation de cette rencontre a reçu le soutien actif de la
Faculté des Sciences de Luminy, du
Centre International de Rencontres Mathématiques et de
l'Institut
de Mathématiques de Luminy.
Nous les en remercions chaleureusement.
Inscriptions
Envoyer un mail à Marie-Renée Fleury-Donnadieu
: mrd[_AT_]iml.univ-mrs.fr, en précisant bien :
- Vos dates d'arrivée et de départ.
-
Et quels repas vous souhaitez prendre au CIRM, parmi ceux de
- mardi 23 midi
- mercredi 24 midi
- mercredi 24 soir (bouillabaisse).
Lieu
La rencontre se tiendra à la Faculté des Sciences de
Luminy, dans l'amphithéatre 12 (batiment 9 sur le plan
suivant), et les repas seront pris au CIRM.
Pour se rendre à Luminy : le plus simple est de prendre le
métro jusqu'au Rond-Point du Prado, puis le bus 21 (voir le site de la
RTM et aussi Le Pilote).
NB: il y a aussi une version rapide du 21, le JETBUS, départ du
Rond-Point du Prado, toutes les 15mn entre 7h20 et 9h30. Durée du
trajet: 20mn. Retour vers le Rond-Point du Prado dans l'après-midi:
toutes les 15mn entre 16h15 et 18h15. Utilisable avec les cartes de transport de la
RTM (Solo qu'on peut acheter dans le bus, Double Solo ou
Libertés).
Pour se rendre au CIRM : accès.
Le CIRM correspond au numéro 12 (rouge) sur ce
plan
du campus de Luminy.
Hôtels
Chacun devra réserver son hôtel. On pourra consulter cette liste
à cet effet.
Liste des orateurs
General program
 |
- Tuesday:
- 8'45--9'05: reception and coffe at the "Institut mathématique de Luminy" (IML),
3rd floor in room 310;
- 9'15--12'15: talks in "amphithéatre 12" in building B (behind the IML
building);
- 12'15--14'00: lunch at the "Centre international de rencontres
mathématiques" (CIRM), which lies on the right of the main road;
- 14'00--15'30: talks in amphithéatre 12;
- 15'30--16'00: coffe at the IML, room 310;
- 16'00-17'30: last talks for the day, in amphithéatre 12.
- Wednesday:
- 9'00--9'20: reception and coffe at the "Institut mathématique de Luminy" (IML),
3rd floor in room 310;
- 9'30--12'15: talks in "amphithéatre 12" in building B (behind the IML
building);
- 12'15--14'00: lunch at the "Centre international de rencontres
mathématiques" (CIRM), which lies on the right of the main road;
- 14'00--16'00: talks in amphithéatre 12;
- 16'00--16'30: coffe at the IML, room 310;
- 16'30-17'30: last talk for the day, in amphithéatre 12.
|
Programme provisoire
Mardi 23 novembre :
Mercredi 24 novembre :
Jeudi 25 Novembre, matin : amphithéatre Herbrand (130--134,
premier étage), à l'Institut
mathématique de Luminy
Jeudi 25 novembre, 16h :
Journée académique et scientifique de
de l'Université de la
Méditerranée, à la Faculté de
médecine, salle de
conférence Maurice Toga, 27 boulevard Jean-Moulin, 13385 Marseille,
métro Timone.
Le programme de la cérémonie officielle, au cours de laquelle Per
Martin-Löf recevra le Doctorat Honoris Causa, se trouve ici.
La remise des titres de Docteur Honoris Causa aura lieu à 18h.
Organisateurs
La rencontre est organisée par Thomas Ehrhard,
Marie-Renée Fleury-Donnadieu
et Pierre Hyvernat.
Pour toute question concernant la rencontre, vous pouvez envoyer un email
à Marie-Renée
Fleury-Donnadieu (mrd[_AT_]iml.univ-mrs.fr) ou à Pierre Hyvernat
(hyvernat[_AT_]iml.univ-mrs.fr).
Résumés
Peter Hancock
Programs and the real world.
I first learnt about type theory and something about programming from Per.
After a few years I was employed writing programs to monitor and control
various (usually dangerous) things: scientific experiments on human hearing,
heavy machinery, computer systems running user programs, and transactions
involving bank accounts. It has not always been easy to reconcile theory with
practice. I shall present some resulting ideas about programs, programming,
constructive mathematics, and applying mathematics in the physical (or in any
sense "real") world.
Ulrich Berger
A Semantic Strong Normalization Proof for Higher-Type Rewrite Systems.
We consider the untyped lambda calculus with constructors and recursively
defined constants. We define the n-th approximation of a term M as the term
M_n obtained by replacing every constant c with a constant c_n which is
defined like c except that it unfolds only n times. We show that if M does
not denote bottom in a suitable strict domain-theoretic model and all M_n are
strongly normalizing, then M is strongly normalizing. We transfer this result
to typed lambda calculi extended by various forms of transfinite- and
bar-recursion in higher types for which strong normalization was hitherto
unknown. The motivation for this work comes from computational problems
arising in connection with program extraction from classical proofs.
Martin Hofmann
Non size increasing polytime computation: 5 years later.
In 1999 I have proposed an extension of multiplicative linear logic with a new
type <> and inductive datatypes where each constructor takes an extra
argument of type <>. For example, unary natural numbers are a type N and
come with constants 0:N and S:<> -o N -o N and an iteration principle:
from closed terms z:A and s:<> -o A -o A derive It(z,s):N -o A. There
are no closed terms of type <>.
It was shown that all functions on lists of booleans definable in this system
are non-size increasing (length of f(l) <= length(l)) and polytime
computable. Later in 2002 I was able to show that all non size-increasing
polytime functions are definable in the system, in particular all
characteristic functions of problems in P.
One (arguable) deficiency of the system is that data types are primitive
concepts and not definable via impredicative encodings as is done in systems
like Light or Soft Linear Logic (LLL, SLL). On the other hand, concrete
programming is much easier in my system than in those systems.
Over the last two years I attempted to extend my system with impredicative
quantification and a !-modality so as to allow for impredicative encodings of
data types and better comparison with LLL, SLL. Doing so is surprisingly
difficult but some partial results begin to emerge.
The talk will recall the existing results on non size-increasing computation
and also discuss the recent advances.
Yves Bertot
Type theory based descriptions of partial co-recursive functions.
Techniques have been proposed recently to describe partial recursive functions
in type theory with inductive types. We study an extension of these
techniques to co-recursive functions and show how that they fit in frameworks
that accepted guarded co-recursive definitions. We give an example with
filters on streams and Eratosthene's sieve.
Assia Mahboubi
Quantifier elimination over real closed fields inside the Coq system
It is known since the work of Tarski in 1948 that one can perform
quantifier elimination in the theory of a real closed field. This result
has fundamental consequences in real algebraic geomerty. In particular
it is possible to build a decision procedure to decide whether a
polynomial system with rational coefficients has a real solution or not.
We will explain how to design such a decision procedure inside the Coq
system, relying on the cylindrical algebraic decomposition, which is a
more recent (Collins 1966) and a more efficient method than Tarski's
historical one.
Gilles Dowek
Axiom vs. computation rules: a state of the art.
In the history of logic, several formalisms have proposed to replace axioms by
compuation rules. I will review some of them, trying to show that this idea
was independently proposed in several contexts. I will then discuss the
following open question: in predicate logic can we always replace axioms by
computation rules.
Thierry Coquand
Elimination of choice sequences and commutative algebra.
The introduction of "Notes on Constructive Mathematics" (which presents the
thesis work of Per Martin-Löf) contains a clear explanation of how
Brouwer's bar theorem can be formulated in constructive mathematics. After
presenting this explanation in the case of the fan theorem (compactness of
Cantor space), we indicate how the same principle can be used in commutative
algebra. One can in this way simplify the proofs of basic theorems
(``Splitting off'' theorem of Serre, Bass stable range theorem, as formulated
by Heitmann). In one case, the simplification is significant enough to suggest
an improved version of the theorem (Forster-Swan's theorem).
Thomas Streicher
A Type-Theoretic Reconstruction of Joyal and Moerdijk's Algebraic Set Theory
(and a Model of CZF+Sep where Every Set is Subcountable).
We show how Joyal and Moerdijk's purely categorical construction of initial
Zermelo-Fraenkel algebras can be rephrased in a type theoretic fashion. It
boils down to a modification of the "Aczel construction" showing that for a
universe U (in the sense of Martin-Loef) the type V = (W A:U) A gives rise to
a model of CZF. For showing that V validates Strong Collection and Subset
Collection Aczel intrinsically employed the choice principles ensured by
Martin-Loef type theory. Our construction deviates from Aczel's in the
following respects:
-
propositions are not interpreted as elements of U but instead as
elements of a type Prop of *proof-irrelevant* propositions
-
Prop may be assumed as impredicative,
i.e. closed under arbitrary products.
As propositions are now proof-irrelevant AC is not for free anymore. To
overcome this problem Joyal and Moerdijk have introduced a kind of type
theoretic collection axiom (ttCA) saying that for any surjective e : X
-->> A with A in U there exists a map f : C -> X with C in U and $e
\circ f$ still surjective. An alternative to ttCA is the Projective Cover
Axiom (PCA) saying that every type A in U can be covered by a projective
object C (i.e. a C for which choice holds) in U. Whereas ttCA holds in
Grothendieck and realizability toposes the simpler axiom PCA holds only in
realizability toposes.
If Prop is an element of U then our modification of the Aczel construction
gives rise to models of IZF. However, if U is interpreted as the modest sets
over K_1 (the first Kleene algebra) and Prop as the assembly of
proof-irrelevant modest sets then V = (W A:U) A gives rise to a model of CZF
with full separation where every set is subcountable and which, therefore,
refutes the power set axiom.
From work of Rathjen it is known that CZF+Sep has the strength of Second Order
Arithmetic. Of course, one might like to construct models of CZF (without
restricting the metatheory to be predicative) which also refute unbounded
separation. This, however, seems to be hard because we don't know of any
(non-term) models of type theory with a universe and a predicative type Prop.
Lutz Straßburger
Naming proofs in classical propositional logic
We present a theory of proof denotations in classical propositional logic. The
abstract definition is in terms of a semiring of weights, and two concrete
instances are explored. With the Boolean semiring we get a theory of classical
proof nets, with a geometric correctness criterion, a sequentialization
theorem, and a strongly normalizing cut-elimination procedure. With the
semiring of natural numbers, we obtain a sound semantics for classical logic,
in which fewer proofs are identified. Though a ``real'' sequentialization
theorem is missing, these proof nets have a grip on complexity issues. In both
cases the cut elimination procedure is closely related to its equivalent in the
calculus of structures, and we get ``Boolean'' categories which are not posets.
Paul-André Melliès
Asynchronous games: an innocent model of linear logic.
Since its early days, deterministic sequential game semantics has been limited
to linear or polarized fragments of linear logic. Every attempt to extend the
semantics to full propositional linear logic has bumped against the so-called
Blass problem, which indicates (misleadingly) that a category of sequential
games cannot be self-dual and cartesian at the same time. We circumvent this
problem here by considering
(1) that sequential games are inherently positional;
(2) that they admit internal positions as well as external positions.
We construct in this way an innocent model of propositional linear logic,
which incorporates the well-bracketed and the non well-bracketed variants of
the original arena game model by Hyland, Ong and Nickau.