A Semantic Basis for Termination Analysis

Cohavit Taboch
Department of Mathematics & Computer Science
Ben-Gurion University of the Negev

Joint work with Michael Codish

A Semantics for Termination.
- Logic Programs and Observables
- Call Patterns
- Binary Unfoldings and Termination
An Abstract Semantics for Termination Analysis.
- Abstract Interpreter
- Abstract Domains for Termination Analysis
- A Sufficient Condition for Termination
Conclusions.

(under Prolog's left to right computation rule) : a query either fails, or produces a finite number of answers. All branches in the SLD tree are finite.

a query either fails or produces at least one answer. The computation tree contains at least one success branch before the infinite branches.

Goal : Find a suitable semantics for "observing" termination.

SLD tree - operational semantics

Resultants semantics (Gabbrielli, Levi, and Meo)

(Gabbrielli and Giacobazzi 1994) +

S-semantics (Falaschi et al) - computed answers

C-semantics - correct answers

Minimal model - logical consequences

Computed answers are in the S-semantics.

For each program P and goal G : solving G with P is the same as solving G with the of P.

Non-termination infinite sequence of calls.
is a call in a derivation of with P < , ... >.

There is a call from to in a computation of G with P if and .
The relation on calls is an abstraction of the derivation which preserves termination properties.

This semantics was shown to capture call patterns and computed answers. (Gabbrielli and Giacobazzi 1994).

Domain : ( )
Operator :
Binary Unfoldings of P =

and are observables in the binary unfolding semantics.

The computed answers for G with P are :
The calls that arise in the computations of G with P are :

is non-terminating for P is non-terminating for

A program P is non-terminating for there is an infinite chain in the calls-to relation.
P and create the same set of pairs of related calls for
An infinite chain of calls is created for P the same infinite chain is created for BinUnf(P).

iterate , fail.
iterate retract(flag), iterate.
iterate.

cond_assert(F) in_database(F), !.
cond_assert(F) assert(F), cond_assert(flag).

in_database(G)
       functor(G,N,A), functor(B,N,A),
       call(B), subsumes(B,G), ! .

       user_clause(Head, Body),
       solve(Head, Body).

solve(Head,[ ]) cond_assert(fact(Head)).
solve(Head,[B|_])cond_assert( bin(Head,B) ).
solve(Head,[B|_])bin(B,C), cond_assert(bin(Head,C)).
solve(Head,[B|Bs]) fact(B), solve(Head, Bs).

Using abstract interpretation, obtain a description of the program's binary unfoldings.

For a given query obtain a description of all possible pairs of related calls.

Proving termination is done by showing that no such pair of related calls can create an infinite chain.

An infinite derivation with the binary clauses contains an infinite sub-chain of calls which can be described by one abstract binary clause and one abstract call description.

Dependencies :
- Monotonicity constraints.
- Polyhedra.
Dependencies : "Prop".
Both domains are determined by a .
A strict decrease in in a argument position Termination.

A symbolic norm is a function such that

where

Symbolic norms are similar to semi-linear norms, except variables map to variables.

Symbolic norms can capture .

Can be obtained in two ways :

Monotonicity constraints (Sagiv and Lindenstrauss).
Polyhedra (Van Gelder, King and Benoy). Combined with a widening.

Both methods can be implemented using the entailment and projection mechanisms of the constraints solver.

A term t is instantiated enough with respect to a symbolic norm

is an integer.

For example :

A ground term is always instantiated enough.
A closed list is instantiated enough w.r.t list length norm.

Instantiation dependencies can be obtained by performing analysis on the transformed program.

Selecting a Symbolic Norm for the abstraction.

Absrtacting the program clauses.

Computing the binary unfoldings of the abstract program.

Given an initial abstract query, obtain an approximation of the calls.

Test each binary clause and corresponding calls for termination condition.

Examples

(Sagiv and Lindenstrauss)

When a program is non-terminating the infinite chain of calls contains an infinite sub-chain which is described by one abstract binary clause and one abstract call.
For a given call and recursive binary clause we show that there exists one argument position, which is instaintiated enough, and its size strictly decreases during subsequent calls.
Such a pair of related calls cannot create an infinite chain because of the well foundedness of the < relation on the natural numbers.

The termination test is done by adding constraints of the form

to argument positions which are instantiated enough and testing for inconsistency.

The inconsistency results from a cycle which indicates a strict decrease in the size of an argument position during the derivation.

Termination is observable in the Binary Unfolding semantics.
The semantic basis for termination enables a clean implementation over abstract domains for size and instantiation dependencies.
The abstract binary unfoldings can be computed using a simple meta-interpreter.
Using constraints solver in the algorithm for computing size dependencies, and for the termination test simplifies the analysis.