14 juin 2018, 11:00 : Séminaire

Pierre Clairambault (LIP, ÉNS Lyon), The true concurrency of Herbrand's theorem

Herbrand's theorem, widely regarded as a cornerstone of proof theory, exposes some of the constructive content of classical logic. In its simplest form, it reduces the validity of a first-order purely existential formula to that of a finite disjunction. In the general case, it reduces first-order validity to propositional validity, by understanding the structure of the assignment of first-order terms to existential quantifiers, and the causal dependency between quantifiers.

In this paper, we show that Herbrand's theorem in its general form can be elegantly stated and proved as a theorem in the framework of concurrent games, a denotational semantics designed to faithfully represent causality and independence in concurrent systems, thereby exposing the concurrency underlying the computational content of classical proofs. The causal structure of concurrent strategies, paired with annotations by first-order terms, is used to specify the dependency between quantifiers implicit in proofs. Furthermore concurrent strategies can be composed, yielding a compositional proof of Herbrand's theorem, simply by interpreting classical sequent proofs in a well-chosen denotational model.

This is joint work with Aurore Alcolei, Martin Hyland, and Glynn Winskel.

Du 12 au 13 juin 2018

Rencontre de réalisabilité au CIRM, organisée par Laura Fontanella et Guillaume Geoffroy.

Voir le site de la rencontre.

7 juin 2018, 11:00 : Séminaire

Pierre Vial (Gallinette, Inria-LS2N, Nantes), Representing permutations without permutations, or the expressive power of sequence types

An intersection type system with given features (strict or not, idempotent or not, relevant or not, rigid or not...) characterizing, e.g., a notion of normalization can be presented in various ways. Recent works by Asada, Ong and Tsukada have championed a rigid description of resources. Whereas in non-rigid paradigms (e.g., standard Taylor expansion or non-idempotent intersection types), bags of resources are multisets and invariant under permutation, in the rigid ones, permutations must be processed explicitly and can be allowed or disallowed. Rigidity enables a fine-grained control of reduction paths and their effects on, e.g., typing derivations. We previously introduced system S, featuring a sequential intersection: a sequence is a family of types indexed by a set of integers. However, one may wonder in what extent the absence of permutations causes a loss of expressivity w.r.t. reduction paths, compared to a usual multiset framework or a rigid one with permutations. Our main contribution is to prove that not only every non-idempotent derivation can be represented by a rigid, permutation-free derivation, but also that any dynamic behavior may be captured in this way. In other words, we prove that system S (sequential intersection) has full expressive power over multiset/ permutation-inclusive intersection. We do so in the most general setting, i.e. by considering coinductive type grammars, so that this work also applies in the study of the infinitary relational model.

26 avril 2018, 11:00 : Séminaire

Andrea Gagna (I2M, Aix-Marseille), Les petites catégories comme modèles des types d'homotopie (suite)

La théorie de l'homotopie des petites catégories a été introduite par Grothendieck avec la définition du foncteur nerf, qui permet de donner une notion sensible d'équivalence faible parmi les petites catégories. Dans sa thèse, Illusie montre (et il attribue la preuve à Quillen) que la catégorie de l'homotopie des petites catégories est équivalente aux types d'homotopie. On donnera une variante de cette preuve qui utilise le théorème A de Quillen.

19 avril 2018, 11:00 : Séminaire

Alexis Saurin (IRIF, Paris 7), Logical by-need

L'analyse de l'appel par nécessité (aussi appelé évaluation paresseuse) est complexe, d'autant plus lorsqu'on considère des opérateurs de contrôle. Ceci suggère de faire appel à la logique, par nécessité, plutôt qu'à chercher à trouver une solution fondée sur de pures considérations opérationnelles. Dans ce séminaire, je présenterai deux telles approches du logical by-need: le premier inspiré par le système L de Curien et Herbelin et le second de la réduction linéaire de tête de Danos et Regnier.

La première approche ne sera qu'évoquée: l'exposé visera surtout à construire un calcul paresseux à partir de la réduction linéaire de tête en trois étapes, à le comparer aux calculs de la littérature et à montrer que cette construction s'étend naturellement aux opérateurs de contrôle fournissant un λμ-calcul paresseux. Selon le temps restant, je discuterai de variantes de l'appel par nécessité (notamment la pleine paresse). Cet exposé s'appuie sur des travaux conduits avec Pédrot ainsi qu'Ariola, Downen, Herbelin et Nakata.

5 avril 2018, 11:00 : Séminaire

Amina Doumane (LIP, ÉNS Lyon), Completeness for identity-free Kleene Lattices

We provide a finite set of axioms for identity-free Kleene lattices, which we prove sound and complete for the equational theory of their relational models. This equational theory was previously proved to coincide with that of language models and to be ExpSpace- complete; expressions of the corresponding syntax moreover make it possible to denote precisely those languages of graphs that can be accepted by Petri automata. Finite axiomatisability was missing to obtain the same picture as for Kleene algebra, regular expressions, and (word) automata.

Our proof builds on the completeness theorem for Kleene algebra, and on a novel automata construction that makes it possible to extract axiomatic proofs using a Kleene-like algorithm.

29 mars 2018, 11:00 : Séminaire

Eduard Balzin (CMLS, École Polytechnique), Les familles de catégories en géométrie et algèbre

Dans cet exposé on parlera des problèmes mathématiques qui peuvent être étudiés en utilisant le formalisme des familles de catégories. Beaucoup d’exemples de familles proviennent de la géométrie, où on considère divers champs à valeurs dans les catégories, et on prend les catégories des sections sous-jacentes. Un autre contexte est celui de l'algèbre, où on peut étudier les familles associées aux catégories monoïdales M. La catégorie des sections d’une telle famille contient les objets algèbres dans M.

Étant donné une famille des catégories munies d'équivalences faibles, on peut se demander si la catégorie des sections est un bon invariant au sens « infini-catégorique ». Nous expliquerons ce problème en détail, en répondant positivement à une conjecture de Hirschowitz et Simpson pour les familles provenant de champs de catégories. Si le temps le permet, on esquissera une approche à cette question dans le cadre des catégories monoïdales.

L'exposé ne supposera aucune connaissance de théorie de l'homotopie, seul une familiarité avec le langage des catégories est requise.

8 mars 2018, 11:00 : Séminaire

Andrea Gagna (I2M, Aix-Marseille), Les petites catégories comme modèles des types d'homotopie

La théorie de l'homotopie des petites catégories a été introduite par Grothendieck avec la définition du foncteur nerf, qui permet de donner une notion sensible d'équivalence faible parmi les petites catégories. Dans sa thèse, Illusie montre (et il attribue la preuve à Quillen) que la catégorie de l'homotopie des petites catégories est équivalente aux types d'homotopie. On donnera une variante de cette preuve qui utilise le théorème A de Quillen.

22 février 2018, 11:00 : Séminaire

Assia Mahboubi (LS2N, Nantes & Inria), Une preuve assistée par ordinateur de l'irrationalité de zeta(3)

L'étude des valeurs de la fonction zeta de Riemann aux entiers impairs est encore aujourd'hui un sujet de recherche actif en théorie des nombres. R. Apéry a obtenu en 1978 un succès spectaculaire en établissant l'irrationalité de zeta(3). Mais le statut, rationnel ou irrationnel des autres entiers positifs impairs est encore inconnu à ce jour. Le point crucial de la présentation originale d'Apéry réside dans l'observation que deux suites particulières sont solutions d'une même récurrence, remarque qui permet d'estimer leurs comportements asymptotiques respectifs. Cette récurrence miraculeuse était difficile à deviner, mais elle s'est aussi révélé difficile à vérifier pour l'auditoire d'Apéry. Depuis les années 90, des chercheurs en combinatoire et en calcul formel ont conçu des algorithmes efficaces qui permettent de "deviner" de telles récurrences, et ainsi de faire des preuves "par calcul formel". Dans cet exposé nous présentons et discutons une preuve formelle de l'irrationalité de zeta(3) basée sur une session de calcul formel qui exécute de tels algorithmes.

(en collaboration avec Frédéric Chyzak, Thomas Sibut-Pinote et Enrico Tassi)

15 février 2018, 11:00 : Séminaire

Giulio Manzonetto (LIPN, Paris 13), Refutation of Sallé's Longstanding Conjecture

The lambda-calculus possesses a strong notion of extensionality, called "the omega-rule", which has been the subject of many investigations. It is a longstanding open problem whether the equivalence obtained by closing the theory of Böhm trees under the omega-rule is strictly included in Morris's original observational theory, as conjectured by Sallé in the seventies. We will first show that Morris's theory satisfies the omega-rule. We will then demonstrate that the two aforementioned theories actually coincide, thus disproving Sallé's conjecture. The proof technique we develop is general enough to provide as a byproduct a new characterization, based on bounded eta-expansions, of the least extensional equality between Böhm trees.

18 janvier 2018, 11:00 : Séminaire

Hadrien Batmalle (IRIF, Paris 7), Préservation de propriétés du modèle de départ en réalisabilité classique

La réalisabilité classique permet d'interpréter des théories mathématiques classiques, comme la théorie des ensembles ZF, dans divers modèles de calcul (lambda-calcul avec continuations, domaines... axiomatisés au moyen d'algèbres de réalisabilité). Elle produit ainsi des modèles de ces théories, et se révèle être une généralisation du forcing de Cohen. Jusqu'ici, la réalisabilité classique a seulement été étudiée à partir d'un modèle de départ "raisonnable", supposé au moins valider AC, voire même défini comme l'univers constructible. Dans cet exposé, on étudiera des modèles de réalisabilité classique issus d'algèbres de réalisabilité usuelles, mais construits sur des modèles de départ "non-triviaux", et on utilisera un nouveau résultat de Krivine pour exporter certaines propriétés du modèle de départ au modèle de réalisabilité.