Exploiting the Power of Typed Norms in Automatic Inference of Interargument Relations

Recently, the introduction of type formalisms for statically analysing logic programs has become a commonly applied technique. More specifically in termination analysis, typed norms have been introduced as a refined way to measure the sizes of terms and atoms. While the expressiveness of these typed norms makes them practically indispensable for a refined termination analysis - particularly when proving termination of queries with partially instantiated terms -, it was not clear how relations between the sizes of (differently measured) arguments of predicates could be derived, and what sense they would make. We present a technique based on abstract interpretation for computing such relations and indicate its role in termination analysis. The resulting analysis extends the power of some of the more refined automatic termination analysis techniques presented previously. 1 Introduction Types are fulfilling an increasingly important role in state of the art approaches to Logic ..