Use of Logical Models for Proving Operational Termination in General Logics

Abstract

A declarative programming language is based on some logic $\mathcal{L}$ and its operational semantics is given by a proof calculus which is often presented in a natural deduction style by means of inference rules. Declarative programs are theories $\mathcal{S}$ of $\mathcal{L}$ and executing a program is proving goals $\varphi$ in the inference system $\mathcal{I}(\mathcal{S})$ associated to $\mathcal{S}$ as a particularization of the inference system of the logic. The usual soundness assumption for $\mathcal{L}$ implies that every model $\mathcal{A}$ of $\mathcal{S}$ also satisfies $\varphi$. In this setting, the operational termination of a declarative program is quite naturally defined as the absence of infinite proof trees in the inference system $\mathcal{I}(\mathcal{S})$. Proving operational termination of declarative programs often involves two main ingredients: (i) the generation of logical models $\mathcal{A}$ to abstract the program execution (i.e., the provability of specific goals in $\mathcal{I}(\mathcal{S})$), and (ii) the use of well-founded relations to guarantee the absence of infinite branches in proof trees and hence of infinite proof trees, possibly taking into account the information about provability encoded by $\mathcal{A}$. In this paper we show how to deal with (i) and (ii) in a uniform way. The main point is the synthesis of logical models where well-foundedness is a side requirement for some specific predicate symbols.

Partially supported by the EU (FEDER), Spanish MINECO TIN 2013-45732-C4-1-P and TIN2015-69175-C4-1-R, and GV PROMETEOII/2015/013.