Ceci est une ancienne révision du document !


Cette page regroupe mes projets de recherche commencés mais laissés en sommeil avant d'être terminés.

Système T avec opérateurs de contrôle

Un des buts est d'étendre le lambda-calcul afin d'étendre la correspondance de Curry-Howard. La réalisabilité classique de Krivine ainsi que le $\lambda \mu$-calcul de Parigot sont des avancées indépendantes dans cette direction. D'autres tentatives (par Nakano, Sato ou Kameyama par exemple) insistent sur l'aspect non-déterminisme de ces opérateurs de contrôle. Pour forcer le déterminisme, il faut forcer la stratégie d'évaluation, ce que nous faisons avec un lambda-calcul monadique où seules les valeurs (variables ou abstractions) peuvent être argument d'une réduction.

Afin d'inclure les entiers et la récurrence, c'est le système T de Gödel et non le lambda-calcul qui sera utilisé comme base. Nous obtenons donc un système T par valeur, que nous traduisons vers un système T « nommé » avec des $\mathtt{let}$, puis vers le système T habituel. En montrant la compatibilité de notre traduction avec la réduction habituelle, nous obtenons la normalisation forte de notre système de calcul en la dérivant de celle du système T.

L'idée aurait été ensuite d'ajouter à notre système de calcul des opérateurs de contrôle comme $\mathtt{callcc}$, $\mathtt{catch}$ ou $\mathtt{throw}$, mais le départ de Tristan Crolard mit le projet en sommeil. Voici ma dernière version de travail.

Contenu algorithmique des stratégies du lambda-calcul

Les EMAs ont été développées notamment par Serge Grigorieff et Pierre Valarcher dans leur article. L'idée est que certes les Abstract State Machines de Gurevich peuvent simuler étape par étape toutes les machines usuelles1), mais que simulation n'est pas identification. Ainsi, Serge Grigorieff et Pierre Valarcher montrent que des classes naturelles d'EMAs peuvent être littéralement identifiées à ces machines, ce qui fait des EMAs un modèle mathématique unificateur.

Dans cette optique, j'ai cherché à formaliser sous forme de machines abstraites les différentes stratégies d'évaluation contextuelle utilisées pour le lambda-calcul. Le terme à évaluer n'est donc qu'une entrée, et c'est la stratégie d'évaluation elle-même qui est vue comme un algorithme. Les différentes stratégies étudiées sont l'appel par nom, l'appel par besoin et l'appel par valeur, qui sont respectivement implémentées par la machine de Krivine et deux machines créées pour l'occasion :

$$\begin{array}{r|l@{}c@{}r@{}rcl@{}c@{}r@{}rc}
\text{appel par nom}
&{} \mu			&{}\ \star\ 	&{} (t_1)t_2 \ \star\ 	&{} \pi 	&{} \succ 	&{} \mu, \mathunderscore	&{}\ \star\ 	&{} t_1 \ \star\ 		&{} t_2,\pi	\\
&{} \mu, \mathunderscore			&{}\ \star\ 	&{} \lambda x.t_1 \ \star\ 	&{} t_2,\pi 	&{} \succ 	&{} \mu	&{}\ \star\ 	&{} t_1[t_2/x] \ \star\ 	&{} \pi	\\
\hline
\text{appel par valeur}
&{} \mu			&{}\ \star\ 	&{} (t_1)t_2 \ \star\ 	&{} \pi 	&{} \succ 	&{} \mu, t_1	&{}\ \star\ 	&{} t_2 \ \star\ 		&{} \mathunderscore,\pi	\\
&{} \mu, t			&{}\ \star\ 	&{} v \ \star\ 		&{} \mathunderscore,\pi 	&{} \succ 	&{} \mu, \mathunderscore	&{}\ \star\ 	&{} t \ \star\ 		&{} v, \pi	\\
&{} \mu, \mathunderscore			&{}\ \star\ 	&{} \lambda x.t \ \star\ 	&{} v,\pi 	&{} \succ 	&{} \mu	&{}\ \star\ 	&{} t[v/x] \ \star\ 		&{} \pi	\\
\hline
\text{appel par besoin}
&{} \mu			&{}\ \star\ 	&{} (t_1)t_2 \ \star\ 	&{} \pi 	&{} \succ 	&{}\mu, \mathunderscore	&{}\ \star\ 	&{} t_1 \ \star\ 		&{} t_2,\pi	\\
&{} \mu, \mathunderscore			&{}\ \star\ 	&{} v \ \star\ 		&{} t, \pi 	&{} \succ 	&{} \mu, v	&{}\ \star\ 	&{} t \ \star\ 		&{} \mathunderscore,\pi	\\
&{} \mu, \lambda x.t	&{}\ \star\ 	&{} v \ \star\ 		&{} \mathunderscore,\pi 	&{} \succ 	&{} \mu	&{}\ \star\ 	&{} t[v/x] \ \star\ 		&{} \pi	\\
\end{array}$$

Nous prouvons que nos machines sont correctes, c'est à dire que si un terme est évalué avec une stratégie jusqu'à une valeur finale en $n$ substitutions, alors la machine ne contenant que ce terme2) fait des transitions jusqu'à arriver à la même valeur en ayant fait exactement $n$ substitutions puis s'arrête. Puis nous traduisons ces machines sous forme d'EMA, et discutons des généralisations possibles.

1) En tout cas, les machines dont le calcul est séquentiel, comme les machines de Turing ou les RAMs.
2) C'est à dire que l'antipile $\mu$ et la pile $\pi$ sont vides.