Sujets de stage

Exécution en λ-calcul avec ressources

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]?

Références

  1. Jean-Louis Krivine, A call-by-name lambda-calculus machine, Higher Order and Symbolic Computation 20, p.199-207 (2007).
  2. Thomas Ehrhard et Laurent Regnier, The differential lambda-calculus, Theoretical Computer Science (2004).
  3. Lionel Vaux, Convolution lambda-bar-mu-calculus, Proceedings of TLCA 2007.
  4. Daniel de Carvalho, Execution Time of lambda-Terms via Denotational Semantics and Intersection Types (2009).

Formalisation des réseaux de démonstration

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 transformations 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 suffisamment explicite pour donner lieu à une réalisation sur machine et suffisamment maniable pour établir des résultats significatifs. À long terme (c'est-à-dire probablement de manière assez 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.

Références

  1. Yves Lafont, From Proof-Nets to Interaction Nets, in Advances in Linear Logic, Cambridge University Press (1995)
  2. Damiano Mazza, Interaction Nets: Semantics and Concurrent Extensions, Thèse de doctorat, Université de la Méditerranée/Roma 3 (2006)
  3. Michele Pagani, Lorenzo Tortora de Falco, Strong normalization property for second order linear logic, Theoretical Computer Science (2010)
  4. Marc de Falco, An Explicit Framework for Interaction Nets, RTA 2009
  5. Gonthier et al. Voir le site du projet math-components.

Séparation dans un cadre quantitatif

Avec Emmanuel Beffara.

Michele Alberti a commencé à attaquer ce sujet durant son stage de M2 en 2011, puis dans sa thèse en cotutelle avec l’université de Bologne (équipe Focus). Durant le M2, il a étudié le résultat qualitatif de Manzonetto et Pagani (TLCA 2011). Ses premiers résultats en thèse permettent de mieux cerner la notion de forme normale (JFLA 2013). Le sujet est suffisamment riche pour qu’on l’aborde simultanément sous plusieurs angles : en février 2013, Thomas Leventis (M2 Lyon) a démarré son stage de M2, avec pour objectif un résultat de séparation pour le λ-calcul probabiliste.

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.

Références

  1. Ugo de'Liguoro, Adolfo Piperno, Non Deterministic Extensions of Untyped Lambda-Calculus, Information and Computation, 1995.
  2. Thomas Ehrhard et Laurent Regnier, The differential lambda-calculus, Theoretical Computer Science (2004)
  3. Emmanuel Beffara, Quantitative testing semantics for non-interleaving
  4. Vincent Danos, Thomas Ehrhard, On probabilistic coherence spaces (2008)
  5. P. Arrighi and G. Dowek, Linear-algebraic lambda-calculus: higher-order, encodings and confluence Proceedings of RTA 2008
  6. Lionel Vaux, The Algebraic lambda-calculus, Mathematical Structures in Computer Science (2009)

Sémantiques à trame de la logique linéaire et du λ-calcul

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:

Références

  1. Jean-Yves Girard et al., Proofs and Types, 1989.

Dernière mise à jour
le 4 mars 2013.

XHTML et CSS valides?