«Inférer et compiler pour la terminaison
des programmes logiques avec contraintes»
Sébastien Hoarau et Fred Mesnard (IREMIA, Université de La Réunion)
Résumé - Ce papier présente une méthode automatisée qui traite en deux étapes la terminaison de programmes logiques contraints. Dans un premier temps, et en utilisant des techniques d'approximations de programmes et de mu-calcul sur les booléens, la méthode infère un ensemble de classes de requêtes possibles pour la terminaison. Par «possibles» nous entendons que pour chacune de ces classes on peut trouver un ordre des littéraux des clauses du programme garantissant la terminaison. Puis, étant donnée une classe parmi celles-là, la deuxième étape consiste à compiler le programme original en un nouveau par réordonnancement des littéraux à l'intérieur des clauses. Pour ce nouveau programme, la terminaison gauche, au sens universel, de toute requête de la classe considérée est assurée.
«Compilation abstraite de LambdaProlog»
Frédéric Malesieux (École des Mines de Nantes), Olivier Ridoux (IRISA, Rennes) et Patrice Boizumault (École des Mines de Nantes)
Résumé - Nous proposons une méthode d'analyse statique pour des programmes LambdaProlog. Cette méthode utilise la technique de la compilation abstraite et elle a déjà été appliquée à des programmes Prolog par Codish et Demoen. Elle se compose de deux phases principales : l'abstraction du programme et l'abstraction du but. Comme ces deux phases nécessitent des programmes normalisés, nous présentons dans cet article, des procédures de normalisation et d'abstraction de programmes LambdaProlog. L'analyse de programmes LambdaProlog est plus complexe que pour Prolog car le langage inclut les quantificateurs universel et existentiel, l'implication et les lambda-termes (ordre supérieur). La principale difficulté provient de l'ordre supérieur car l'analyse statique ne doit pas seulement découvrir les propriétés des lambda-termes mais également la façon dont ces propriétés sont propagées. La propagation est décrite en terme de fonctions de transfert . Nous appliquons cette méthode à l'analyse de clôture.
Mots clés - Compilation abstraite, LambdaProlog, normalisation, abstraction, clôture