OPERATEURS DE MISE EN MEMOIRE EN LAMBDA-CALCUL PUR ET TYPE

Karim M. NOUR

Le l-calcul pur a été inventé vers 1930, et a connu un développement considérable pour ses rapports étroits avec les langages de programmation fonctionnelle. Le l-calcul typé suscite actuellement un grand intérêt à cause du lien qu’il établit entre les notions de programme et de preuve en logique intuitionniste : c’est ce qu’on appelle la “correspondance de Curry-Howard”. Parmi les systèmes de typage qui ont un grand pouvoir d’expression, on trouve le système F des types du second ordre de Girard, ainsi qu’une extension notée AF2 de Krivine, et le système TTR des types récursifs de Parigot. L’intérêt de ces systèmes est que les programmes qu’il donnent sont prouvés .

Krivine a introduit en 1989 la notion d’opérateurs de mise en mémoire pour simuler “l’appel par valeur” dans le cadre d’un “appel par nom”. En l-calcul, la stratégie de réduction gauche (appel par nom) a de bonnes propriétés : elle termine toujours si on l’applique à un terme normalisable; mais avec cette stratégie l’argument d’une fonction est recalculé à chaque utilisation. La notion d’opérateurs de mise en mémoire permet de remédier à ce défault. Krivine a montré qu’en utilisant la traduction de Gödel de la logique classique en logique intuitionniste, on peut trouver, pour chaque type de données, un type très simple pour les opérateurs de mise en mémoire. Ceci donne un moyen d’obtenir ces opérateurs .

Nous étudions dans ce travail quelques propriétés des opérateurs de mise en mémoire en l-calcul pur et typé.

Aprés avoir exposé, dans le chapitre 1, la définition des opérateurs de mise en mémoire, et donné les formes générales de leurs formes normales de tête ; nous introduisons, dans le chapitre 2, le l-calcul dirigé (l-calcul à “trous” dirigés), outil important pour l’étude de ces opérateurs, et nous prouvons que ce l-calcul garde les principales propriétés du l-calcul ordinaire.

Dans le chapitre 3, nous faisons apparâtre les premières propriétés des opérateurs de mise en mémoire :  la stabilité de l’ensemble des opérateurs de mise en mémoire par la β– équivalence, l’existence d’opérateurs pour les ensembles finis de termes normaux clos, et une inégalité contrôlant le temps calcul d’un opérateur.

Le chapitre 4 expose trois sortes de types de données (itératifs, descendants et récursifs) et la caractérisation des objets qu’ils contiennent. Nous y généralisons le théorème de Krivine pour des traductions de Gödel plus “sophistiquées”.

Dans les chapitres 5 et 6, nous étudions les opérateurs forts de mise en mémoire (ceux qui    donnent un terme clos), et nous donnons des conditions nécessaires et suffisantes pour que les représentations récursives et itératives des données en l - calcul possèdent des opérateurs forts, et une condition suffisante pour obtenir des opérateurs propres.

Les chapitres 7 et 8 contiennent les résultats fondamentaux. Après avoir défini la notion de type     - positif (tous les quantificateurs du second ordre sont en position positive dans ce type), et la notion de tranformation de Gödel (une généralisation de la traduction de Gödel classique) du système AF2 et TTT;  nous généralisons, en utilisant des méthodes purement syntaxiques, le théorème de Krivine sur ces types et pour ces transformations.