Inférence de non-terminaison pour les programmes logiques avec contraintes - Archive ouverte HAL Access content directly
Conference Papers Year : 2004

Inférence de non-terminaison pour les programmes logiques avec contraintes

(1) , (1)
1

Abstract

Termination has been a subject of intensive research in the logic programming community for the last two decades. Most works deal with proving universal left termination of a given class of queries, i.e. finiteness of all the possible derivations produced by a Prolog engine from any query in that class. In contrast, the study of the dual problem: non-termination relativement à the left selection rule i.e the existence of one query in a given class of queries which admits an infinite left derivation, has given rise to only a few papers. In this article, we study non-termination in the more general constraint logic programming framework. We rephrase our previous logic programming approach into this more abstract setting, which leads a necessary and sufficient criteria expressed in a logical way and simpler proofs, as expected. Also, by reconsidering our previous work, we now prove that in some sense, we already had the best syntactic criterion for logic programming. Last but not least, we offer a set of correct algorithms for inferring non-termination for CLP
L'analyse de terminaison des programmes logiques a été sujette à une recherche intensive durant les deux dernières décennies. La majorité des travaux s'est intéressée à la termi-naison universelle gauche d'une classe donnée de requêtes, c'est-à-dire au fait que toutes les dérivations des requêtes de cette classe produites par un moteur Prolog sont finies. En revanche, l'étude du problème dual : la non-terminaison par rapport à la règle de sélection gauche, i.e l'existence d'une requête dans une classe donnée qui admet une dérivation gauche infinie, a fait l'objet de peu d'articles. Dans ce papier, nous étudions la non-terminaison dans le contexte de la programmation logique avec contraintes. Nous reformulons, dans ce cadre plus abstrait, les concepts que nous avions définis pour la programmation logique, ce qui nous donne des cri-tères nécessaires et suffisants exprimés de façon logique ainsi que des preuves plus simples. Par ailleurs, en reconsidérant nos travaux précédents, nous démontrons que dans un certain sens, nous détenions déjà le meilleur critère syntaxique dans le cas de la programmation logique. Enfin, nous décrivons un ensemble d'algorithmes corrects pour l'inférence de non-terminaison des programmes CLP.
Fichier principal
Vignette du fichier
Inference_non-terminaison_pour_programmes_logiques_avec_contraintes.pdf (195.15 Ko) Télécharger le fichier
Origin : Explicit agreement for this submission
Loading...

Dates and versions

hal-01915272 , version 1 (12-11-2018)

Identifiers

  • HAL Id : hal-01915272 , version 1

Cite

Etienne Payet, Frédéric Mesnard. Inférence de non-terminaison pour les programmes logiques avec contraintes. 13èmes Journées Francophones de Programmation en Logique et Programmation par Contraintes (JFPLC 2004), Association Française pour la Programmation en Logique et la programmation par Contraintes, Jun 2004, Angers, France. pp.55-72. ⟨hal-01915272⟩
49 View
3 Download

Share

Gmail Facebook Twitter LinkedIn More