Comparer des programmes fonctionnels, ou comment remettre les λ-termes en ordre

L'équivalence de programmes est un sujet central dans l’étude des langages de programmation. Certifier que la sémantique d’un programme est préservée par les transformations et optimisations d’un compilateur est un point crucial dans la formalisation des compilateurs. Cette thèse a pour but de développer plus loin plusieurs aspects de la théorie des équivalences de programmes pour le λ-calcul non typé et pur. Une proposition majeure est d’étudier systématiquement les préordres de programmes plutôt que les équivalences, ce qui est habituel dans l’étude des langages de programmation mais pas systématique pour le langage prototypique qu’est le λ-calcul. Nous montrons que plusieurs concepts centraux dans la théorie du λ-calcul se reformulent comme des propriétés simples sur des préordres de λ-termes. L’équivalence contextuelle est la notion standard et naturelle d’équivalence de programmes : comparer par contexte revient à tester les programmes dans tout environnement d’exécution possible et vérifier qu’ils se comportent de la même manière. Cette notion d’équivalence est malheureusement peu utilisable en pratique pour vérifier l’équivalence de deux programmes dans tout langage assez riche. Nous proposons un raffinement quantitatif de l’équivalence contextuelle, avec pour but d’obtenir une équivalence de programmes sensible à une notion de coût et aussi naturelle que la comparaison contextuelle. L’équivalence d’interaction teste des programmes dans tout environnement d’exécution possible, vérifie que leur comportement est similaire tout en comptant le nombre de communications (ou d’interactions) entre le terme et l’environnement qui l’exécute. Enfin, la dernière partie de cette thèse est consacrée à l’étude des équivalences de programmes pour le λ-calcul équipé d’une évaluation en appel-par-valeur. Cette évaluation est plus efficace que l’évaluation originale, plus fidèle à l’implémentation pratique des langages mais est moins bien étudiée d’un point de vue théorique. Nous étudions un spectre large d’équivalences de programmes, qui apparaissent habituellement quand le langage est étudié avec l’ajout d’effets de bord. Notre cadre pur (sans effets) se prête tout de même à cette étude pour montrer la richesse de toutes les variantes d’équivalences possibles en appel-par-valeur. Nous présentons des définitions unifiant l’étude de toutes ces équivalences de programmes et leurs propriétés en rendant abstraite la notion de stratégie d’évaluation.