Weighted graphs: A tool for studying the halting problem and time complexity in term rewriting systems and logic programming. (English) Zbl 0702.68036
Summary: This study is based on the halting and complexity problems for a simple class of logic programs in PROLOG-like languages. Any Prolog program can be expressed in the form of an overlap of some simpler programs whose structures are basic and can be studied formally. The simplest recursive rules are studied here and the weighted graph is introduced to characterise their behaviour. This new syntactic object, the weighted graph, generalises the directed graph. Unfoldings of directed graphs generate infinite regular trees that I generalise by weighting the arrows and putting periods on the variables. The weights along a branch are added during unfolding and the result (modulo of the period) indexes variables. Hence, their interpretations are non-regular trees because of the infinity of variables. This paper presents some of the formal properties of these graphs, finite and infinite interpretation and unification.
Although they have a consistency apart from all possible applications, weighted graphs characterise the behaviour of recursive rules in the form L:-R. They express the most general fixpoint of these rules and range across a finite sequence of recursive rewritings. Within global rewriting systems and logic programming, the halting problem and the existence of solutions are proved to be decidable for this simple recursive rule with linear goals and facts, and the complexity is shown to be at most linear.
Although these problems are undecidable for slightly more complex schemes, it is hoped that from the weighted graphs of each recursive sub- structure of a Prolog program, the whole behaviour of the program will be understandable. Then, the weighted graphs would be the nucleus of an efficient methodological logic programming, which could be called structured logic programming.
Although they have a consistency apart from all possible applications, weighted graphs characterise the behaviour of recursive rules in the form L:-R. They express the most general fixpoint of these rules and range across a finite sequence of recursive rewritings. Within global rewriting systems and logic programming, the halting problem and the existence of solutions are proved to be decidable for this simple recursive rule with linear goals and facts, and the complexity is shown to be at most linear.
Although these problems are undecidable for slightly more complex schemes, it is hoped that from the weighted graphs of each recursive sub- structure of a Prolog program, the whole behaviour of the program will be understandable. Then, the weighted graphs would be the nucleus of an efficient methodological logic programming, which could be called structured logic programming.
MSC:
| 68N17 | Logic programming |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68Q25 | Analysis of algorithms and problem complexity |
| 68Q42 | Grammars and rewriting systems |
| 03D15 | Complexity of computation (including implicit computational complexity) |
| 68T99 | Artificial intelligence |
References:
| [1] | Böhm, C.; Jacopini, G., Flow diagrams, Turing machines and languages with only two formation rules, Comm. ACM, 9, 366-371 (1966) · Zbl 0145.24204 |
| [2] | Colmerauer, H., Prolog II, Manuels de Reference, Theorique et Pratique (1979), GIA: GIA Marseille |
| [3] | Colmerauer, H., Equations and inequetions on finite and infinite trees, FGCS’84 Proc., 85-99 (1984) |
| [4] | Courcelle, B., Fundamental properties of infinite trees, Theoret. Comput. Sci., 17, 95-169 (1983) · Zbl 0521.68013 |
| [5] | Courcelle, B., Equivalence and transfortation of regular systems. Applications to recursive programs schemes and grammars, Theoret. Comput. Sci., 42, 1-122 (1986) · Zbl 0636.68104 |
| [6] | Dauchet, M., Simulation of Turing machines by a left linear rewrite rule, (Internal Report IT153. Internal Report IT153, Chapel Hill, NC, USA. Internal Report IT153. Internal Report IT153, Chapel Hill, NC, USA, Third Internat. Conf. on Rewriting Techniques and Applications (1989), LIFL Lille: LIFL Lille France) · Zbl 0753.68052 |
| [7] | Dershowitz, N., Termination, Dijon, France. Dijon, France, Proc. First Internat. Conf. on Rewriting Techniques and Applications, 180-224 (1985) · Zbl 0581.68031 |
| [8] | Dershowitz, N., Termination of rewriting, J. Symbolic Comput., 3, 69-116 (1987) · Zbl 0637.68035 |
| [9] | Devienne, P., Les graphes orientés pondérés, un outil pour l’étude de la terminaison et de la complexité dans les systeêmes de réécritures et en pro grammation logique, Thesis (1987), Lille, France |
| [10] | Devienne, P., Strongly reduced systems of equations, ICOT Technical Memorandum TM-529. ICOT Technical Memorandum TM-529, Kyoto, Japan. ICOT Technical Memorandum TM-529. ICOT Technical Memorandum TM-529, Kyoto, Japan, Proc. 37th Ann. Convention IPS, 23-24 (1988) |
| [11] | Devienne, P., Weighted graphs, a tool for expressing the behaviour of recursive rules in logic programming, Tokyo, Japan. Tokyo, Japan, Proc. FGCS’88 Proc. (1988) |
| [12] | Devienne, P.; Lebeque, P., Weighted graphs, a tool for logic programming, Nice. Nice, Proc. 11th Colloquium on Trees in Algebra and Programming, 100-111 (1986) · Zbl 0605.68075 |
| [13] | P.Devienne and P. Lebeque, All programming can be done with at most one right recursive rule and three facts, In preparation.; P.Devienne and P. Lebeque, All programming can be done with at most one right recursive rule and three facts, In preparation. |
| [14] | Eder, E., Properties of subtitutions and unifications, J. Symbolic Comput., 1, 31-46 (1985) · Zbl 0589.68063 |
| [15] | Fages, F., Notes sur l’unification des termes du premier ordre finis our infinis, (Internal Report (1983), INRIA-LITP: INRIA-LITP France) |
| [16] | Gaiman, H.; Mairson, H., Undecidable optimisation problems for database logic programs, New York. New York, Proc. Symp. on Logic in Computer Science, 106-115 (1987) |
| [17] | Huet, G., Resolution d’equations dans les langages d’ordre 1,2,…,Ω, (These de doctorat d’etat (1976), Université Paris VI) |
| [18] | Huet, G., Confluent reductions: abstract properties and applications to term rewriting systems, J. ACM, 27, 797-821 (1980) · Zbl 0458.68007 |
| [19] | Huet, G.; Lankford, D. S., On the uniform halting problem for term rewriting systems, (Rapport Laboria, 283 (1978), INRIA Le Chesnay: INRIA Le Chesnay France) |
| [20] | Ionnadis, Y. E., A time bound on the materialisation of some recursively defined views, Stockholm. Stockholm, Proc. 11th Internat. Conf. in Very Large Data Bases, 219-226 (1985) |
| [21] | Lassez, J.; Maher, M. J.; Marriot, K., Unification revisited, J. Minker. J. Minker, Workshop on logic and Data Bases (1987) |
| [22] | Lebégue, P., Contribution à l’étude de la programmation logique par les graphes orientés pondérés, Thesis (1988), Lille, France |
| [23] | Lipton, R. J.; Snyder, W., On the halting of tree replacement systems, Waterloo, Canada. Waterloo, Canada, Proc. Conf. on Theoretical Computer Science, 43-46 (1977) · Zbl 0408.68046 |
| [24] | Lloyd, J. W., Foundations of Logic Programming (1987), Springer: Springer Berlin · Zbl 0547.68005 |
| [25] | Naughton, J. F., Data independent recursion in deductive database, Cambridge. Cambridge, Proc. Symp. on Principles of Database Systems, 267-279 (1986) |
| [26] | Vardi, M. Y., Decidability and undecidability results for boundedness of linear recursive queries, Austin. Austin, Symp. on Principles of Database Systems, 341-351 (1988) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
