Lambda-Calcul, Réécriture, Réplication par noeuds, Applications généralisées, Types intersection, Substitutions explicites

Le lambda-calcul est un modèle mathématique des langages de programmation fonctionnels, avec un accent sur l'application de fonctions. Il est intéressant de considérer des variants du lambda-calcul pour modéliser des comportements calculatoires spécifiques. Le lambda-calcul atomique et les lambda-calculs avec applications généralisées sont deux variants (indépendants) du lambda-calcul provenant d'interprétations calculatoires de la théorie de la démonstration. Alors que les langages de programmation sont basés sur des stratégies d'évaluation déterministes spécifiques, la littérature existante sur le lambda-calcul atomique et les applications généralisées ne s'étendent que sur la théorie générale des calculs. En particulier, la réduction des termes n'est pas restreinte, et seulement analysée qualitativement. Cela induit un écart entre la théorie et la pratique, que nous cherchons à diminuer dans cette thèse. À partir du lambda-calcul atomique, nous isolons la notion la plus saillante de sa sémantique opérationnelle, que nous appelons réplication par noeuds. C'est une procédure de substitution particulière, qui duplique les termes finement, un noeud de l'arbre syntaxique à la fois. Nous poursuivons avec les lambda-calculs à applications généralisées. Ceux-ci utilisent une application ternaire qui ajoute une continuation à l'application binaire habituelle. Dans ce travail, nous développons les théories opérationnelles basées sur la réplication par noeuds et les applications généralisées séparément. Pour les deux: À un niveau opérationnel, nous donnons plusieurs stratégies d'évaluation, toutes observationnellement équivalentes aux stratégies correspondantes du lambda-calcul. À un niveau logique, notre approche est guidée par les types quantitatifs. Nous définissons différents systèmes de types qui caractérisent des propriétés sémantiques par induction, mais donnent aussi des bornes quantitatives sur la longueur de réduction et la taille des formes normales. Plus précisément, dans la première partie de cette thèse, nous implémentons la réplication par noeuds au moyen d'un calcul à substitutions explicites. Nous montrons en particulier comment la réplication par noeuds peut être utilisée pour implémenter la pleine paresse, une stratégie d'évaluation bien connue de langages de programmations comme Haskell. Nous montrons des propriétés d'équivalence observationnelle reliant la sémantique pleinement paresseuse aux sémantiques usuelles. Dans la deuxième partie de cette thèse, nous commençons par une caractérisation opérationnelle et logique de la solvabilité dans les lambda-calculs à applications généralisées. Nous montrons comment ce cadre donne naissance à une remarquable sémantique opérationnelle de l'appel-par-valeur. La caractérisation en appel-par-nom s'appuie sur un nouveau calcul à applications généralisées. Nous prouvons dans les deux cas que les sémantiques opérationnelles sont compatibles avec un modèle quantitatif, au contraire de celle du calcul en appel-par-nom originel. Nous prouvons ensuite des propriétés essentielles de ce nouveau calcul en appel-par-nom, et montrons l'équivalence observationnelle avec l'original.