Binding-Time Annotations without Binding-Time Analysis

The basic task of binding-time analysis (BTA) is to compute annotations that guide the unfolding decisions of a specialiser. The main problem is to guarantee that the specialisation will terminate. In the context of logic programming, only few automatic such analyses have been developed, the most sophisticated among them relying on the result of a separate termination analysis. In this work, we devise an analysis that generates the annotations during termination analysis, which allows much more liberal unfoldings than earlier approaches.