Évènement

Rémy Cerda
I2M, Aix-Marseille Université

Date(s) : 10/06/2024   iCal
14h00 - 18h00

Composition du jury

• Ugo DAL LAGO Rapporteur Professore ordinario, Università di Bologna
• Giulio MANZONETTO Président, Professeur des universités, Université Paris Cité
• Laurent REGNIER Co-directeur, Professeur des universités, Aix-Marseille université
• Christine TASSON Rapporteure, Professeure des universités, ISAE-Supaero
• Femke VAN RAAMSDONK Examinatrice, Assistant professor, Vrije universiteit Amsterdam
• Lionel VAUX AUCLAIR Directeur, Maître de conférences, Aix-Marseille université

Résumé
Depuis son introduction par Church, le λ-calcul a joué un rôle majeur dans un
siècle de développement de l’informatique théorique et de la logique mathéma-
tique, mais aussi dans la naissance de nombreux langages de programmation.
Une propriété cruciale de ce calcul est qu’il n’est pas normalisant en général, de
sorte qu’un intérêt croissant a porté sur la recherche d’approximations de sa dy-
namique. Les outils « classiques » d’approximation, nés dans les années 1970
dans le sillage des sémantiques de Scott, sont essentiellement sémantiques.
Les outils basés sur le développement de Taylor, introduits dans les années 2000
par Ehrhard et Regnier, proposent à l’inverse une approximation dynamique
de la β-réduction. Puisant ses inspirations dans le développement de la logique
linéaire, le développement de Taylor traduit le λ-calcul vers un calcul « à res-
sources » multilinéaire, muni d’une dynamique finitaire. Un théorème de com-
mutation (entre approximation et normalisation) fait notamment l’efficacité de
cette approche, et en justifie le succès. La notion d’arbre de Böhm est centrale
dans cette ligne de recherche. Née de l’idée que les termes normalisants ne sont
pas les seuls à avoir un sens calculatoire, elle généralise la notion de forme nor-
male en constituant une «forme normale à l’infini». La compréhension de la
nature coinductive de cet objet a mené dans les années 1990 à l’introduction de
λ-calculs infinitaires. Dans ces calculs, les termes et les réductions peuvent être
infinis et, dans le cas du calcul 001-infinitaire, l’arbre de Böhm est la notion de
forme normale à l’infini (sans guillemets).
L’idée qui guide cette thèse est que le λ-calcul 001-infinitaire se prête à une gé-
néralisation de l’approximation de Taylor où, en particulier, les arbres de Böhm
seraient des «citoyens ordinaires». L’approximation du λ-calcul fini, et notam-
ment de ses propriétés de normalisation, devient alors un cas particulier de
l’approximation du calcul infinitaire. Cela est permis par le principal résultat
de la thèse, qui établit que la dynamique du calcul à ressources est à même de
simuler la β-réduction infinitaire via le développement de Taylor.
Pour arriver à ce résultat, nous faisons d’abord un détour par une présentation
abstraite d’une syntaxe « mixte » (inductive et coinductive) d’ordre supérieur,
à l’aide d’un formalisme nominal généralisant des travaux récents introduisant
des types coalgébriques avec lieurs. Cela nous permet de définir formellement
des coalgèbres de classes d’α-équivalence de λ-termes infinitaires (chapitre 1).
Dans un second temps, nous définissons les λ-calculs infinitaires à l’aide d’une
présentation coinductive, puis nous rappelons leurs principales propriétés ainsi
que leur lien avec les théories classiques de l’approximation de la β-réduction
(chapitre 2). Ensuite, nous présentons le λ-calcul à ressources comme un cas
particulier d’une réécriture avec sommes, et distinguons ses versions qualita-
tive et quantitative (chapitre 3).
Dans une seconde partie consacrée à l’approximation de Taylor propre-
ment dite, nous commençons par introduire le développement de Taylor
des λ-termes infinitaires et prouvons le théorème de simulation annoncé,
dans sa forme qualitative puis quantitative. Nous démontrons l’efficacité de
ce théorème en le mettant à l’œuvre, proposant notamment une nouvelle
preuve de confluence pour le λ-calcul 001-infinitaire (chapitre 4). Nous nous
penchons également sur la conservativité de la propriété de simulation, et
démontrons l’existence surprenante d’un contre-exemple à cette propriété
réciproque (chapitre 5). Enfin, nous étendons notre travail au cadre paresseux,
c’est-à-dire celui du λ-calcul 101-infinitaire, et nous démontrons un théorème
de commutation pour les arbres de Lévy-Longo (chapitre 6).
Mots-clefs : lambda-calcul, réécriture infinitaire, développement de Taylor,
approximation de programmes, sémantique quantitative.
Abstract
Since its introduction by Church, the λ-calculus has played a major role in a cen-
tury of development in theoretical computer science and mathematical logic,
as well as in the birth of numerous programming languages. A crucial prop-
erty of this calculus is that it is not normalising in general, leading to growing
interest in finding approximations to its dynamics. The ‘classic’ approximation
tools, which emerged in the 1970s in the wake of Scott’s semantics, are essen-
tially semantic. The tools based on Taylor expansion, introduced in the 2000s
by Ehrhard and Regnier, conversely propose a dynamic approximation of the
β-reduction. Drawing its inspiration from the development of linear logic, Tay-
lor expansion translates the λ-calculus into a multilinear ‘resource’ calculus,
equipped with finitary dynamics. A commutation theorem (between approxi-
mation and normalisation) makes this approach particularly effective, and jus-
tifies its success.
The notion of Böhm tree is central to this line of research. Associated with the
idea that normalising terms are not the only computationally meaningful ones,
it generalises the notion of normal form by constituting an ‘infinite normal
form’. Understanding the coinductive nature of this object led in the 1990s to
the introduction of infinitary λ-calculi. In these calculi, terms and reductions
can be infinite and, in the case of the 001-infinitary calculus, the Böhm tree is
the notion of infinite normal form (without quotes).
The idea guiding this thesis is that the 001-infinitary λ-calculus lends itself to
a generalisation of the Taylor approximation where, in particular, Böhm trees
would be ‘ordinary citizens’. The approximation of the finite λ-calculus, and
in particular its normalisation properties, then becomes a special case of the
approximation of the infinitary calculus. This is enabled by the main result of
the thesis, which establishes that the dynamics of the resource calculus is able
to simulate the infinitary β-reduction via Taylor expansion.
To arrive at this result, we first make a diversion via an abstract presentation
of a ‘mixed’ (inductive and coinductive) higher-order syntax, using a nominal
formalism generalising recent work on coalgebraic types with binders. This
allows us to formally define coalgebras of α-equivalence classes of infinite λ-
terms (chapter 1). In a second step, we define infinitary λ-calculi using a coin-
ductive presentation, then recall their main properties as well as their connec-
tion with classical theories of approximation of the β-reduction (chapter 2).
Then, we present the resource λ-calculus as a special case of a rewriting with
sums, and distinguish its qualitative and quantitative flavours (chapter 3).

Emplacement
Luminy

Catégories

• Soutenance de thèse