Directions of Operational Termination

Abstract

A theory S in a logic supplied with an inference system is operationally terminating if no goal has an infinite well-formed proof tree. Well-formed proof trees are those which an interpreter would incrementally build when trying to solve a condition at a time from left to right. For this reason, infinite well-formed proof trees have a unique infinite branch which is called the spine. This paper introduces the notion of a directed proof tree for S and a set of formulas ?, which we call a direction. Intuitively, a direction ? is intended to collect formulas that are infinitely often used in the spine of an infinite well-formed proof tree (which is then called ?-directed) due to the repeated use of some specific inference rules. Then we introduce the notion of ?-directed operational termination of a theory as the absence of ?-directed proof trees. This new notion permits the definition of different termination properties which can be useful to distinguish different computational behaviors. It also gives a new characterization of operational termination of a (finite) theory S as the conjunction of the ?-directed operational termination of S for each direction ? in a (finite) set of directions.