Proving Operational Termination of Declarative Programs in General Logics

Abstract

A declarative program P is a *theory* in a given computational logic L, so that *computation* with such a program is efficiently implemented as *deduction* in L. That is why *inference systems* are crucial: they both (i) *define* the logical semantics of a language in its underlying logic L, and (ii) *specify* the *execution* of programs in a correct implementation. The notion of *operational termination* (OT) of a declarative program P identifies termination with *absence of infinite inference* with P. We further develop the OT notion for declarative programs in general logics with schematic inference systems and characterize OT in terms of *chains of proof jumps*. We also generalize the dependency pair framework to an arbitrary schematic logic L, so that methods for proving declarative programs OT become available for a very wide range of declarative languages. We illustrate the usefulness of the general OT methods we propose by three case studies in three logics: that of Conditional Term Rewriting Systems, the Typed Lambda Calculus, and Membership Rewriting Logic. In particular, we show how various programs that could not be proved terminating with existing methods can be proved OT with the methods presented here.