Résumés des interventions

Olivier Bournez

Nous reviendrons sur des dispositifs de calculs parfois très anciens, et sur des modèles mathématiques de ces instruments ou machines. Ces modèles sont tous basés sur le calcul analogique, en travaillant sur des quantités continues plutôt que discrètes. En particulier, on discutera du rôle spécifique joué par le modèle du General Purpose Analog Computer, proposé par Claude Shannon comme modélisant les analyseurs différentiels mécaniques de son époque. On cherchera à comprendre comment ils se comparent aux ordinateurs actuels et aux modèles actuels de l’informatique théorique. On présentera quelques résultats récents qui ont été obtenus et certaines des applications de ces résultats à d’autres contextes. On présentera aussi quelques questions ouvertes et les questions que cela pose sur d’une part les modèles mathématiques de certaines machines, et d’autre part comment on peut mesurer de façon robuste les ressources utilisées par un calcul dans ce cadre.

Walter Dean

Je commencerai par rapidement revoir quelques considérations issues de la pratique de l'informatique théorique qui suggèrent que les algorithmes sont des objets mathématiques abstraits, semblables à des graphes ou à des groupes. J'examinerai ensuite les preuves de l'opinion - peut-être bien connue - selon laquelle ces considérations sont mieux prises en compte en considérant les algorithmes comme une classe d'équivalence de modèles de machines factorisés par simulation mutuelle. Cela suggère une analogie naturelle avec l'abstraction Frégéenne. Mais je suggérerai que les défis auxquels est confrontée une telle théorie des algorithmes sont assez différents de ceux auxquels est confronté le néo-logicisme - c'est-à-dire ceux de l'inconsistance et de la "Bad Company". Je suggérerai plutôt que le défi fondamental d'une théorie "abstractionniste" des algorithmes est de trouver une définition formelle de la simulation qui soit capable de rendre compte des détails de nos pratiques. Je vais illustrer cela à l'aide d'observations concernant l'inter-simulatibilité (apparente) de tous les algorithmes qui résolvent des problèmes complets pour la classe P (c'est-à-dire la complexité polynomiale en temps).

Paolo Mancosu

In this talk I will give a general presentation of definitions by abstraction by first looking at their historical roots in mathematical practice and then by discussing their role in recent foundational programs such as neologicism.

Baptiste Mélès

L'usage de la notion d'abstraction en programmation informatique pourrait de l'extérieur paraître paradoxale, puisqu'il semble s'agir d'un domaine concret, soumis aux contingences de la matière et de l'état de la technique. Nous verrons pourtant que l'on trouve, parmi les « bonnes pratiques » de programmation, des méthodes d'abstraction communes avec celles des mathématiques. Pour le montrer, nous mobiliserons des exemples informatiques variés, des conseils de programmation et, à titre de comparaison, les théories de l'abstraction mathématique d'Albert Lautman et de Jules Vuillemin. Nous verrons ainsi que l'abstraction ne permet pas seulement de bien /connaître/ les objets mais également de bien penser ce que c'est qu'/agir/ sur eux.

Elaine Pimentel

One of the advantages of using sequent systems as a frameworks for logical reasoning is that the resulting calculi are often simple, have good proof theoretical properties (like cut-elimination, consistency, etc) and can be easily implemented, e.g. using rewriting. Hence it would be heaven if we could add axioms in mathematical theories to first order logics and reason about them using all the machinery already built for the sequent framework. Indeed, the general problem of extending standard proof-theoretical results obtained for pure logic to certain class of non-logical axioms has been focus of attention for quite some time now. The main obstacle for this agenda is that adding non-logical axioms to systems while still maintaining the good proof theoretical properties it is not an easy task. In this talk, we will show a systematic way of adding transforming axioms into inference rules, and smoothly adding the resulting rules into well known sequent systems. The method is based on the notions of focusing and polarities, and it will be illustrated for the case of Euclidean Geometry.

This is a joint work with Dale Miller, Sonia Marin and Marco Volpe.

Natacha Portier

Dans cet exposé interactif, nous parlerons de ce que sont le calcul et la complexité. Je partirai de vos réponses à mes questions pour introduire des notions et engager la discussion.

Sylviane Schwer

Alors que la notion d’algorithmique est bien connue des mathématiciens depuis l’antiquité, l’étude de leur complexité n’émerge vraiment à la fin du XIX° siècle, en particulier avec les travaux d’Emile Lemoine (1840-1912) sur la géométrographie, plutôt dans un contexte non académique. Nous nous proposons de présenter ses travaux et d’en discuter la modernité. Compas, régles et feuilles de papier sont les bienvenus pour cette séance.