Non-Failure Analysis for Logic Programs

We provide a method whereby, given mode and (upper approximation) type information, we can detect procedures and goals that can be guaranteed to not fail (i.e., to produce at least one solution or not terminate). The technique is based on an intuitively very simple notion, that of a (set of) tests \covering" the type of a set of variables. We show that the problem of determining a covering is undecidable in general, and give decidability and complexity results for the Herbrand and linear arithmetic constraint systems. We give sound algorithms for determining covering that are precise and e cient in practice. Based on this information, we show how to identify goals and procedures that can be guaranteed to not fail at runtime. Applications of such non-failure information include programming error detection, program transformations and parallel execution optimization, avoiding speculative parallelism and estimating lower bounds on the computational costs of goals, which can be used ...

• Type: Conference
• Year: 1997
• Where: ICLP
• Authors: Saumya K. Debray, Pedro López-García, Manuel V. Hermenegildo
• Keywords: Arithmetic Constraint Systems, Automated Reasoning, ICLP 1997, Parallel Execution Optimization, Upper Approximation