Le système F en logique linéaire

Christian RETORÉ

Mémoire de DEA ( Diplôme d’Études Approfondies) de mathématiques

Sous la direction de Jean-Yves Girard

Equipe de logique, UFR de mathématiques, Université Paris 7

(Aujourd'hui Equipe de logique, Institut de Mathématiques de Jussieu-Paris Rive Gauche, Université Paris Cité et Université Paris Sorbonne)

Septembre 1987


--- English translation below


Mettre en ligne mon mémoire de DEA (1987) est pour moi assez gênant, quand bien même quelques collègues (un peu dérangés ?)  me l'auraient demandé récemment  (2025): mise en page rudimentaire issue des premiers traitements de texte, notations parfois ésotériques, impression sur une imprimante à aiguille d’époque, avec en prime quelques ajouts manuscrits ; et ce n’est pas qu’un problème de forme : bibliographie inexistante, rédaction excessivement détaillée de passages évidents, rédaction elliptique voire obscure de passages nettement plus compliqués, sans parler des probables erreurs, qui vu la forme passent plus facilement sous les radars.

Plusieurs plateformes de diffusion (HAL, arXiv) ont d’ailleurs refusé sa mise en ligne, au motif — difficilement contestable — que le document est trop « crado » pour les standards actuels, ou que ce n’est qu’un mémoire de DEA, en français de surcroît.

Et pourtant, ce texte contient quelques observations sur les schémas de réduction autres que l'élimination des coupures, qui, manifestement, ne sont mentionnés nulle part ailleurs et continuent d’intéresser de drôles de gens. Qu’on se rassure : il ne s’agit en rien de contributions majeures — plutôt des observations modestes mais originales, dont la seule particularité est d’être restées inaccessibles. Et merci à Vincent Danos d’avoir très correctement cité ce torchon dans sa thèse (Une application de la logique linéaire…, Paris 7, 1990), geste que je me permets de lui rendre, quarante ans plus tard ;-)

En dépit de  l’évidente indigence de la forme — et par endroits du contenu —  la présence, malgré tout, de quelques remarques pertinentes et éventuellement utiles, ne serait ce que pour se moquer,  me conduit à rendre ce mémoire disponible tel quel.

Cette situation me rappelle une scène de David Lodge : lors d’une soirée bien arrosée entre universitaires, chacun est prié de révéler une action ou un propos dont il a honte. Un jeune universitaire en langue et littérature anglaise avoue qu’il n’a jamais lu d'oeuvre de Shakespeare. Sur le moment, les autres sont épatés par son culot et rigolent; mais ensuite, les mêmes collègues lui tiennent rigueur de cet aveu pour son avancement. Je pense que chacun d'entre nous a  déjà vu ou vécu une situation similaire.

Comme tout cela m'énerve, plutôt que de réécrire, lisser ou maquiller ce travail ancien pour le conformer aux attentes acutelles — et, plus simplement, par fainéantise ;-) — je rends le dit rapport public tel quel, avec ses défauts bien visibles.

Étant aujourd’hui en fin de carrière, et même émérite, le risque est minime ; et il me plaît d’en profiter pour rappeler que les travaux non professionnels,  peuvent aussi contenir remarques pertinentes longtemps après alors que la production de haut niveau appréciée des comités d'évaluations conduit assez souvent, hélas, à des publications qui cessent rapidement d’intéresser qui que ce soit.

Et puisque le ridicule, pas plus que la honte, ne tue, c’est par ici.

-----

Putting my DEA dissertation (1987) online is, for me, rather embarrassing — even if a few colleagues (slightly unhinged?) have recently (2025) encouraged me to do so: rudimentary formatting produced by early word processors, occasionally esoteric notation, output from a period dot‑matrix printer, and, for good measure, a few handwritten additions. Nor is this merely a question of appearance: there is no bibliography, an excessively detailed treatment of obvious points, an elliptical — at times obscure — handling of considerably more difficult ones, not to mention the likely errors, which, given the presentation, have every chance of slipping unnoticed under the radar.

Several dissemination platforms (HAL, arXiv) have in fact refused to host it, on the — hardly disputable — grounds that the document is too “scruffy” by current standards, or simply that it is only a DEA dissertation, in French at that.

And yet the text does contain a number of observations on reduction schemes other than cut‑elimination which, apparently, are mentioned nowhere else and continue to interest some rather odd people. Let there be no misunderstanding: these are not major contributions — merely modest but original remarks, whose sole distinction is to have remained inaccessible. My thanks to Vincent Danos for having quite properly cited this piece of rubbish in his thesis (Une application de la logique linéaire…, Paris 7, 1990); I am pleased to return the favour forty years on ;-)

Despite the evident poverty of the form — and, in places, of the content — the persistence of a few remarks that are at least pertinent, and occasionally useful, if only as material for mockery, is enough to justify making the dissertation available as it stands.

The situation reminds me of a scene from David Lodge: at a well‑lubricated gathering of academics, each guest is invited to confess some act or remark of which they are ashamed. A young lecturer in English literature admits that he has never read Shakespeare. At the time, his colleagues admire the cheek and laugh; later, the very same colleagues quietly hold it against him when it comes to promotion. Most of us will have seen some version of this.

As all this irritates me, rather than rewriting, smoothing, or dressing up this early work to meet contemporary expectations — and, more simply, out of laziness ;-) — I am making the document public exactly as it is, flaws plainly visible.

Now that I am at the end of my career — indeed emeritus — the risk is minimal; and I take the opportunity to point out that non‑professional work can also contain remarks of lasting relevance, sometimes more so than the polished productions that circulate officially — the high-standard sort of output favoured by evaluation committees all too often resulting, regrettably, in publications that very quickly cease to interest anyone at all.

And since neither ridicule nor embarrassment is fatal, here it is.