Abstract FR:

Les langages logico-fonctionnels sont des langages de programmation de tres haut niveau permettant de definir dans un formalisme unifie des types de donnees, des fonctions et des predicats (relations). Plusieurs propositions de langages logico-fonctionnels ont ete faites mais toutes se restreignent a des calculs bases sur les termes du premier ordre. Cette restriction permet de programmer avec des types abstraits algebriques mais elle rend difficile la manipulation des structures de donnees du monde reel, modelisees sous la forme de graphes cycliques. L'objectif de cette these est donc d'introduire les graphes cycliques comme structure de donnees de base des langages logico-fonctionnels. Pour cela, nous voyons les programmes comme des systemes de reecriture de graphes cycliques et nous etudions les relations de reecriture et de surreduction qu'ils induisent (semantique operationnelle). Une propriete importante de la reecriture concerne la confluence : elle exprime le determinisme des calculs effectues. De nombreux resultats de confluence existent pour la reecriture de termes mais ils ne s'etendent generalement pas aux graphes cycliques. Nous mettons en evidence une classe de graphes cycliques particuliers, les graphes admissibles, pour laquelle nous donnons une preuve de confluence de la reecriture. Concernant la relation de surreduction, nous en proposons une definition puis nous montrons que ce calcul est coherent et complet par rapport a celui de la reecriture dans le cadre des graphes admissibles. Nous etudions ensuite plusieurs strategies de reecriture et de surreduction de graphes admissibles, c'est-a-dire des algorithmes permettant d'eliminer des calculs inutiles ou redondants. Nous montrons que nos strategies sont optimales selon de nombreux criteres dependants des systemes de reecriture consideres.