Séminaire Logique et Interactions

In proof theory, one transforms Hilbert axioms into Gentzen rules to obtain cut-elimination theorems. In algebra, one embeds a given algebra into a complete one for various purposes. It is not surprising that these two are deeply related, since both are concerned with conservative extension. The connection is, however, even tighter than expected. For one thing, the passage from Hilbert axioms to Gentzen rules plays a crucial role for algebraic completion too. For another thing, Maehara-Okada cut-elimination can be construed as generalization of Dedekind-MacNeille completion.

To illustrate the situation, we introduce a hierarchy on nonclassical axioms. One of our goals is then to identify a boundary in the hierarchy, below which proof theory (cut-elimination) works well and above which one finds negative algebraic results (failure of completion).

Besides the general issue, I will also discuss a curious borderline case: logic for compact closed categories with binary products and coproducts. Even though the corresponding variety of lattice-ordered abelian groups is not closed under completions, it has a cut-free hypersequent calculus discovered by Metcalfe, Olivietti and Gabbay. With this example, I will illustrate how our theory works as a heuristic principle for finding a cut-free (hyper)sequent calculus, and also how it might be useful in a categorical setting as well.

Joint work with A. Ciabattoni, N. Galatos and L. Strassburger.

Le modèle relationnel de la logique linéaire (et donc du λ-calcul) possède une propriété de finitude établie par Ehrhard en introduisant la notion d'espace de finitude: quelle que soit la structure de finitude imposée sur les atomes, l'interprétation relationnelle d'une preuve est finitaire dans l'espace de finitude associé à sa conclusion. Ce résultat est à l'origine d'une reformulation de la sémantique quantitative de Girard dans un cadre purement algébrique, et a permis des avancées importantes dans l'extension de la correspondance Curry-Howard, par exemple aux paradigmes de calcul non-déterministes et concurrents (logique linéaire différentielle, λ-calcul avec ressources...).

On s'intéresse ici à la possibilité d'étendre l'interprétation relationnelle finitaire du λ-calcul simplement typé à la famille la plus élémentaire de types de inductifs: les types algébriques récursifs. Le problème est double:

• trouver une interprétation relationnelle des types algébriques récursifs, de leurs constructeurs et de leurs destructeurs (opérateurs de définition par cas);
• établir que cette interprétation est finitaire.

Le premier point ouvre la voie à une interprétation non uniforme des types de données et donc à une justification sémantique de leur introduction dans des langages fonctionnels non-déterministes, voire sensibles aux ressources. Le deuxième permet d'envisager une sémantique quantitative en présence de types de données, le sens d'une telle sémantique restant à développer.

Rappelons que le groupe des permutations sur n éléments est engendré par des involutions. C'est pour cette raison que son graphe de Cayley est non orienté. Ce graphe admet une orientation canonique si l'on demande qu'une arête augmente la longueur d'une permutation. Le graphe dirigé ainsi obtenu est le diagramme de Hasse d'un ensemble ordonné qui est, en plus, un treillis: tout sous ensemble admet une plus petite borne supérieure et une plus grande borne inférieure.

Dans cet exposé nous allons présenter les propriétés d'ordre de ce treillis, le treillis des permutations sur n éléments. Nous allons d'abord représenter une permutation par son ensemble d'inversions, et puis l'ordre par le relation d'inclusion. Puis, après avoir représenté les permutations sup-irréductibles (et inf-irréductibles), nous aborderons le représentation de ces treillis en tant que treillis de concepts et treillis engendré par sa base canonique.

The linear-algebraic λ-calculus extends the λ-calculus with the possibility of making arbitrary linear combinations of λ-calculus terms a.t+b.u. In this paper we provide a System F-like type system for the linear-algebraic λ-calculus, which keeps track of “the amount of a type” that is present in a term. We show that this scalar type system enjoys both the subject-reduction property and the strong-normalisation property, which constitute our main technical results. The latter yields a significant simplification of the linear-algebraic λ-calculus itself, by removing the need for some restrictions in its reduction rules — and thus leaving it more intuitive. More importantly we show that our type system can readily be modified into a probabilistic type system, which guarantees that terms define correct probabilistic functions. Thus we are able to specialize the linear-algebraic λ-calculus into a higher-order, “probabilistic” λ-calculus. Finally we discuss the more long-term aims of this reseach in terms of establishing connections with linear logic, and building up towards a quantum physical logic through the Curry-Howard isomorphism. Thus we begin to investigate the logic induced by the scalar type system, and prove a no-cloning theorem expressed solely in terms of the possible proof methods in this logic.

Les bigèbres classiques ont une structure algébrique d'algèbre associative et une structure cogébrique de cogèbre associative. Ces deux structures sont en liaison via une relation de compatibilité (relation de Hopf). Il existe d'autres types de bigèbres obtenues en modifiant ces différentes structures. Pour certaines d'entre elles on sait généraliser les théorèmes classiques de Poincaré-Birkhoff-Witt et Cartier-Milnor-Moore.

Je présenterai une géométrie de l'interaction (GdI) pour MLL dont les principaux objets sont des graphes, une approche qui généralise la première GdI qui utilisait des permutations. Je montrerai ensuite que cette construction peut être vue comme une version combinatoire de la géométrie de l'interaction dans le facteur hyperfini (restreinte aux multiplicatifs) récemment introduite par J.-Y. Girard. Finalement, je discuterai des éventuelles généralisations de ce cadre pour des fragments plus larges de la logique linéaire.