Abstract FR:

Cette these propose une formalisation de l'evaluation partielle. Elle fournit par ailleurs quelques outils d'aide a la construction d'evaluateurs partiels (correction des transformations, algorithme, terminaison). Elle est motivee par le constat de lacunes dans des fondements theoriques et dans des mises en uvre pratiques. L'une, notamment, tient au caractere informel de la problematique de l'evaluation partielle: determiner des programmes qui sont a la fois equivalents et plus performants qu'un programme donne. Afin de modeliser precisement la performance d'un programme, nous proposons tout d'abord un cadre general qui permet de representer le processus d'execution (par opposition a la semantique pure). Nous indiquons ensuite comment attribuer un cout a une execution et etudions plusieurs mesures d'efficacite. Cette presentation debouche sur une definition formelle de l'evaluation partielle en termes d'optimisation. Elle met egalement en evidence plusieurs notions d'evaluation partielle optimale. Cette approche est illustree d'exemples qui reposent sur la semantique naturelle et les schemas de programmes recursifs. Nous employons ces memes schemas pour etudier formellement la correction des transformations de pliage/depliage, transformations majeures de l'evaluation partielle. En particulier, nous etablissons quelques lemmes de commutativite sur les systemes de reecriture afin d'etendre le champ d'application des conditions de correction du depliage/pliage faible. D'autre part, nous donnons une definition formelle a l'algorithme de redemarrage generalise, montrons rigoureusement sa terminaison, et examinons quels bons criteres d'arret peuvent l'equiper. Nous concluons notre etude sur une analyse des limites a l'optimisation par evaluation partielle