Proving Operational Termination of Declarative Programs in General Logics
Salvador Lucas, José Meseguer · 2014
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 for Term Rewriting Systems 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 λ-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.