Non-Termination Inference for Optimal Ter-mination Conditions of Logic Programs - Université de La Réunion Access content directly
Conference Papers Year : 2002

Non-Termination Inference for Optimal Ter-mination Conditions of Logic Programs

Abstract

In this paper, we present an approach to non-termination inference of logic programs. Our framework relies on an extension of the Lifting Theorem, where some specific argument positions can be instantiated while others are generalized. Atomic left looping queries are then generated bottom-up from selected subsets of the binary unfoldings of the program of interest. Then non-termination inference is tailored to attempt proofs of optimality of left termination conditions computed by a termination inference tool. For each class of atomic queries not covered by a termination condition, the aim is to ensure the existence of one query from this class which leads to an infinite search tree. When termination and non-termination analysis produce complementary results for a logic procedure , they induce a characterization of the operational behavior of the logic procedure with respect to the left most selection rule and the language used to describe sets of atomic queries.
Dans cet article, nous présentons une technique d'inférence de conditions de non-termination de programmes logiques. Notre travail repose sur une extension du "Lifting Theo-rem", où des positions d'arguments spécifiques peuvent être instanciées alors que les autres sont généralisées. Des requêtes atomiques qui bouclent à gauche sont alors générées de façon ascendante à partir de sous-ensembles des dépliages binaires du programme traité. L'inférence de non-terminaison est alors utilisée pour tester l'optimalité de conditions de termi-naison gauche générées par un outil d'inférence de terminaison. Pour chaque classe de requêtes atomiques non couverte par une condition de terminaison, nous tentons d'assurer l'existence d'une requête de cette classe qui mène à un arbre de recherche infini. Quand les analyses de terminaison et de non-terminaison produisent des résultats complémentaires pour une procédure logique, on obtient une caractérisation du comportement opérationnel de la procédure par rapport à la règle de sélection gauche et au langage utilisé pour décrire les ensembles de requêtes atomiques.
Fichier principal
Vignette du fichier
Non_termination_inference_for_optimal_termination_conditions_of_logic_programs.pdf (1.8 Mo) Télécharger le fichier
Origin Explicit agreement for this submission
Loading...

Dates and versions

hal-01915407 , version 1 (07-11-2018)

Identifiers

  • HAL Id : hal-01915407 , version 1

Cite

Frédéric Mesnard, Etienne Payet, Ulrich Neumerkel. Non-Termination Inference for Optimal Ter-mination Conditions of Logic Programs. 11èmes Journées Francophones de Programmation en Logique et Programmation par Contraintes (JFPLC'02), Association Française pour la Programmation en Logique et la programmation par Contraintes (AFPLC), May 2002, Nice, France. pp.84-104. ⟨hal-01915407⟩
27 View
29 Download

Share

Gmail Mastodon Facebook X LinkedIn More