Ce sujet a été traité (avec talent) par Étienne Miquey pendant son stage de L3.
Avec Emmanuel Beffara.
L'objectif premier du stage est de concevoir et d'implémenter une machine abstraite [1] pour le λ-calcul avec ressources et le λ-calcul différentiel [2]. Pour le λ-calcul standard, l'exécution se fait habituellement par réduction de tête, et la machine de Krivine implémente cette réduction de façon efficace. L'étudiant devra donc se familiariser avec la variante différentielle du λ-calcul, afin de déterminer la bonne façon d'adapter la machine de Krivine. Il s'agira de prendre en compte les aspects propres à ce calcul, comme le non-déterminisme et la gestion des ressources. Il pourra être utile de s'appuyer sur la notion de produit de convolution sur les piles [3].
L'étude du calcul dans la machine obtenue pourra mener à des questions d'ordre sémantique sur les raffinements du λ-calcul: peut-on voir l'exécution des termes avec ressources comme le calcul d'une forme normale ou d'une variante d'arbre de Böhm? Peut-on évaluer le temps et l'espace mémoire nécessaires à l'exécution complète d'un terme, et peut-on les borner sémantiquement [4]?
Avec Emmanuel Beffara.
Les réseaux de démonstration de la logique linéaire sont une syntaxe graphique libérée en grande partie de la bureaucratie syntaxique associée au calcul des séquents, formant en quelque sorte une déduction naturelle pour la logique linéaire. Le principe général est de représenter les règles logiques comme des liens entre les formules actives des prémisses et la (parfois les) formule(s) de conclusion, sans relation a priori avec un contexte. La procédure d'élimination des coupures y est définie comme une interaction locale entre règles logiques et non plus par des tranformations globales sur les arbres de preuves.
Cette notion est un artefact important de la logique linéaire, qui à son tour a permis un certain nombre d'avancées, fournissant les intuitions de la ludique puis de la géométrie de l'interaction. Une version épurée des réseaux de démonstration a été introduite par Lafont [1] comme un cadre générique pour la description d'interactions locales fortement déterministes: les réseaux d'interaction, ensuite généralisés notamment par Mazza [2] sans la contrainte de déterminisme.
La concision du formalisme est à la fois un atout et une difficulté pour le mathématicien: on sort en fait du cadre purement syntaxique où tout est un arbre, et on perd la notion de dernière règle qui servait auparavant de « poignée » par où attraper l'objet démonstration. Ceci explique en partie pourquoi certains résultats apparemment essentiels de la théorie n'ont été formellement établis que très tardivement. L'exemple le plus frappant est la preuve de normalisation forte du système complet de la logique linéaire du second ordre: une preuve était esquissée rapidement dans le papier fondateur de Girard, mais il a fallu attendre le travail très récent de Pagani et Tortora [3] pour avoir une preuve complète, qui d'ailleurs ne suit pas précisément le cheminement annoncé.
Un autre effet secondaire regrettable est l'absence de définition « officielle » des réseaux, c'est-à-dire l'absence de consensus sur une formalisation qui permette de travailler. En conséquence, chaque nouvel article sur le sujet propose sa définition — ou pire: travaille sur une notion laissée suffisament floue pour laisser place à l'interprétation.
L'objectif principal de ce stage est de rechercher une formalisation à la fois suffisament explicite pour donner lieu à une réalisation sur machine et suffisament maniable pour établir des résultats significatifs. À long terme (c'est-à-dire probablement de manière suffisament ambitieuse pour dépasser le cadre de ce seul stage) on souhaiterait disposer des outils nécessaires pour formaliser complètement, dans Coq par exemple, le travail de Pagani et Tortora.
Une première étape à laquelle on pourra se consacrer sera la formalisation des réseaux d'interaction: c'est la notion intuitivement la plus simple, et dont le traitement soulève déjà des difficultés importantes. On se réfèrera au travail de de Falco [4] qui semble rassembler les qualités souhaitées: définition formelle et manipulation aisée. Une contribution possible serait de coder ce travail en Coq, probablement en utilisant les fonctionnalités apportées par ssreflect [5]. On pourra également tenter d'étendre les concepts de de Falco au cadre des réseaux avec tranches (sps dans [3]). Plus fondamentalement on recherchera des « méthodes d'entrée » pour décrire des réseaux de manière concise mais aussi universelle que possible.
Avec Emmanuel Beffara.
Central dans la théorie du λ-calcul, le théorème de Böhm est un résultat de séparation qui établit qu'un modèle non trivial de la βη-équivalence ne peut identifier ne serait-ce que deux termes non équivalents. Il est possible, dans une certaine mesure, d'étendre ce résultat à une extension non-déterministe du λ-calcul [1]. L'objectif de ce stage est d'étudier cette question dans un cadre quantitatif, que l'on peut voir comme un cadre non-déterministe dans lequel le choix est non-idempotent, c'est-à-dire qu'il se comporte comme une somme. Cette recherche est motivée par l'émergence récente de formalismes quantitatifs issus de la logique linéaire [2] ou encore de la théorie de la concurrence [3], et qui peuvent se voir comme une approche des formes de non-déterminisme probabiliste [4] et quantique [5].
Un premier travail important est de chercher comment poser correctement la question. On pourra en particulier chercher à formuler un résultat à la Böhm pour le λ-calcul algébrique [6] sans coefficients, c'est-à-dire surtout comprendre quelle peut être la nature de l'équivalence observationnelle en présence de sommes. Plus élémentairement, la somme nulle peut-elle (ou même doit-elle) être séparée de termes non solvables?
Les suites qu'on peut envisager pour ce travail sont diverses et dépendent en partie des réponses qu'on aura apportées. On pourra en particulier s'intéresser à la robustesse du résultat en présence de coefficients; développer sur la notion d'arbres de Böhm quantitatifs; comparer le pouvoir discriminant des contextes quantitatifs par rapport aux contextes de λ-calcul pur; etc.
Le modèle cohérent du λ-calcul [1], et plus généralement de la déduction naturelle intuitionniste, est le point de départ de l'invention de la logique linéaire par Girard. Il possède la propriété essentielle qu'une fonction stable entre espaces cohérents (éventuellement l'interprétation d'un terme, donc) est univoquement représentée par sa trame: celle-ci est en quelque sorte l'ensemble des instances (entrées,sortie) de la fonction. On a bien « entrées » au pluriel et « sortie » au singulier: pour produire un résultat, un programme fonctionnel peut faire appel à plusieurs instances distinctes de son argument. On peut très grossièrement résumer l'idée de base de la logique linéaire comme le passage du concept (entrées,sortie) à celui de (paquet d'entrées,sortie) où « paquet » est bien au singulier, i.e. l'identité emblématique A⇒B = !A⊸B.
C'est l'instance la plus connue mais pas forcément la plus simple de ce qu'on appelle les sémantiques à trame:
Dans le modèle cohérent, la notion de paquet correspond à celle d'ensemble fini. Mais, sans la structure de cohérence, cette notion ne convient plus: l'ensemble de couples {({α},α); α∈A} (l'interprétation de la déréliction de la logique linéaire dans les espaces cohérents) ne se comporte pas comme une identité intuitionniste (en termes catégoriques, ce n'est pas une transformation naturelle). Dans ce cas, la notion de multi-ensemble fini est mieux adaptée: étonnamment, compter les copies des arguments qu'une fonction utilise fait toute la différence.
On obtient ainsi un modèle extrêmement dépouillé de la logique linéaire et du lambda-calcul: le modèle relationnel. Sa simplicité conceptuelle le rend très expressif: on peut donner des opérateurs de point fixe à tous les types; on y trouve des objets réflexifs (des modèles du λ-calcul pur) extensionnels ou non; on peut interpréter une forme de non déterminisme intrinsèque par l'union des ensembles; on y retrouve une notion de ressource non-uniforme; etc.
Le modèle relationnel peut être utilisé comme base d'une grande variété de sémantiques à trame: il suffit d'adjoindre un peu de structure aux ensembles interprétant les types, en s'assurant que les interprétations des preuves respectent cette structure. Le modèle cohérent multi-ensembliste, variante évidente de l'original, est construit ainsi. On peut également mentionner la notion de totalité de Loader, où celle de finitude d'Ehrhard.
La problématique de fond qu'on propose d'aborder au cours de ce stage est l'exploration de la notion de sémantique à trame, dans son unité comme dans sa diversité. On cherchera en particulier à proposer une exégèse des espaces cohérents originaux, c'est-à-dire à voir comment en cherchant à rendre naturelle la déréliction ensembliste, on est amené à introduire une notion de cohérence. On s'intéressera également au travail récent d'Ehrhard qui permet de voir les domaines de Scott comme une solution orthogonale à la même question. Et on tentera de voir si d'autres constructions encore peuvent convenir. Le sujet est très ouvert et de nombreuses autres pistes méritent d'être explorées, parmi lesquelles: