Généralisation des Jeux Combinatoires et Applications aux Langages Logiques

M. Guy Cousineau président M. François Fages rapporteur M. Furio Honsell rapporteur M. Roberto Di Cosmo directeur de thèse M. Pierpaolo Degano M. Giorgio Levi Mlle Francesca ScozzariGame theory had, in its origins, a vocation for social and economic sciences, with disparate applications, for example in the processing of medical data. It is perceived today as a very general paradigm of concepts and techniques, whose potential still remains to be discovered in computer science. In this thesis we study a particular branch, combinatorial game theory (with two players), in order to profit from it in the very active field of formal semantics of programming languages. Within a game, we can separate the syntactic aspect, inherent in the possible outcomes of matches, from the semantic aspect, inherent in the forecasts over the winning player and, possibly, inherent in a quantification of profit, in terms of a stake, like wealth or prestige. To model the concept of profit, the selected structure of evaluation should not necessarily be the structure of booleans (win or loose), or that of natural or relative numbers. It is enough for this structure to verify some properties, rather weak, guaranteeing the existence of a semantics, even when the play gives rise to infinite matches, as in the game of bisimulation between concurrent processes, or as in the game of logic programming. In this work, we study the semantic characterization of a logical language (with or without constraints) in terms of a game with two players. The effect of such an interpretation, beyond the intuitive model whose didactic value would deserve to be examined, makes it possible to reuse Alpha-Beta, one of the most celebrated algorithms in combinatorial game theory, as a resolution engine for logical languages. The recent and spectacular results obtained by chess programs (like the defeat of the world champion Kasparov against the IBM program Deep Blue) testify to a kind of artificial intelligence acquired by these programs that might be transposed and exploited in the resolution of logical languages. The resolution of existential conjunctive goals in a first-order theory of Horn clauses provides an interesting case. Indeed, the ability of Alpha-Beta to simplify calculation or, in other words, to prune the uninteresting paths, is not closely related to a particular type of game or profit, but to a well-chosen set of algebraic properties, satisfied by the game of logical programming. The correction of Alpha-Beta is formally proven for a very wide variety of structures. In this way, the computed values could be natural numbers, as in the case of chess, or substitutions or constraints, as in the case of logical languages.La théorie des jeux a développé, à ses débuts, une vocation pour les sciences sociales et économiques, avec des applications disparates, comme par exemple le traitement de données médicales. Elle apparaît aujourd'hui comme un paradigme de concepts et de techniques très général, dont le potentiel reste encore à exploiter en informatique. Dans cette thèse nous étudions une branche particulière, la théorie des jeux combinatoires (à deux joueurs), pour en tirer bénéfice dans le domaine, très actif, des sémantiques formelles des langages de programmation. D'un jeu, nous pouvons séparer l'aspect syntaxique, inhérent aux dénouements possibles des matchs, de l'aspect sémantique, inhérent aux prévisions sur le gagnant et la quantification de son gain (en termes d'un enjeu quelconque, tel que l'argent ou le préstige). Pour modeliser la notion de gain, la structure d'évaluation choisie ne doit pas forcément être celle des booléens (gagné ou perdu), ou celle des entiers naturels ou relatifs. Il suffit qu'elle vérifie des propriétés, assez faibles, garantissant l'existence d'une sémantique même lorsque le jeu donne lieu à des matchs infinis, comme dans le cas du jeu de la bisimulation entre processus concurrents, et du jeu de la programmation logique. Dans ce travail, nous étudions la caractérisation sémantique d'un langage logique (avec ou sans contrainte) en termes de jeu à deux joueurs. Au-delà du modèle intuitif des jeux, dont la valeur pédagogique mériterait d'être approfondie, une telle interprétation permet de réutiliser un des algorithmes les plus utilisés dans la théorie des jeux combinatoire, Alpha-Bêta, comme moteur de résolution pour les langages logiques. Les résultats récents et spectaculaires obtenus par les programmes d'échecs (souvenons-nous de la défaite du champion du monde Kasparov contre le programme Deep Blue d'IBM) témoignent d'une forme d'intelligence artificielle développée dans ces programmes qui peut être transposée et exploitée dans la résolution des langages logiques. La résolution d'interrogations existentielles conjonctives dans une théorie de clauses de Horn du premier ordre est en particulier concernée. En effet, la capacité d'Alpha-Bêta à simplifier le calcul ou, en d'autres termes, sa capacité à éliminer les coups inintéressants, n'est pas intimement liée à un type de jeu ou à un type de gain particuliers, mais demande juste des propriétés algébriques qui sont satisfaites dans le jeu de la programmation logique. La correction d'Alpha-Bêta est prouvée de façon formelle pour un éventail de structures très large. Les valeurs calculées pourront être aussi bien des entiers naturels, comme dans le cas du jeu d'échecs, que des substitutions ou des contraintes, comme dans le cas des langages logiques