Computing Reviews

A devil’s advocate against termination of direct recursion
Frühwirth T.  PPDP 2015 (Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, Siena, Italy, Jul 14-16, 2015)103-113,2015.Type:Proceedings
Date Reviewed: 08/12/15

A totally correct system terminates. Instead of establishing termination directly, this paper describes a technique based on non-termination. This technique is statically derivable from the program text and produces non-termination results that are informative relative to the system’s failure to terminate.

A logically adept reader may be feeling anxious: to show not non-terminating is not to show termination. The logically sophisticated reader may be anticipating restrictive table setting to support this technique. The technique is described relative to a rule-based constraint language. “Devil’s rules,” syntactically derived from a program’s directly recursive rules, are added to the program, and are designed to drive the program into non-termination, called maximally vicious computations. The central theorem of the paper shows that non-terminating programs contains maximally vicious computations characterized by devil’s rules. In the absence of devil’s rules, a program terminates.

Now for the fine print: a program with devil’s rules may converge to failure, from which nothing can be concluded. In addition, the technique applies only to programs with rules satisfying various conditions needed by devil’s-rule derivations. The technique is in its early days, however, and further work may broaden and strengthen the results it can achieve.

The paper is a vigorous read, requiring knowledge of more advanced forms of logic programming as well as the usual first-order predicate logic. The simple even-predicate running example proved to be a surprisingly effective help when working through the paper carefully.

Reviewer:  R. Clayton Review #: CR143682 (1511-0984)

Reproduction in whole or in part without permission is prohibited.   Copyright 2024 ComputingReviews.com™
Terms of Use
| Privacy Policy