Búsqueda avanzada

Using Well-Founded Relations for Proving Operational Termination

In this paper, we study *operational termination*, a proof theoretical notion for capturing the termination behavior of computational systems. We prove that operational termination can be characterized at different levels by means of well-founded relations on specific formulas which can be obtained from the considered system. We show how to obtain such well-founded relations from logical models which can be automatically generated using existing tools.

Directions of Operational Termination (Trabajo original)

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.

The 2D Dependency Pair Framework for conditional rewrite systems (Trabajo ya publicado)

Different termination properties of conditional term rewriting systems have been recently described emphasizing the bidimensional nature of the termination behavior of conditional rewriting. The absence of infinite sequences of rewriting steps (termination in the usual sense), provides the horizontal dimension. The absence of infinitely many attempts to launch the subsidiary processes that are required to check the rule’s condition and perform a single rewriting step has been called V-termination and provides the vertical dimension. We have characterized these properties by means of appropriate notions of dependency pairs and dependency chains. In this paper we introduce a 2D Dependency Pair Framework for automatically proving and disproving all these termination properties. Our implementation of the framework as part of the termination tool MU-TERM and the benchmarks obtained so far suggest that the 2D Dependency Pair Framework is currently the most powerful technique for proving operational termination of conditional term rewriting systems.

Use of logical models for proving operational termination in general logics (Tutorial)

A declarative programming language is based on some logic 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 S of L and executing a program is proving goals G in the inference system I(S) associated to S as a particularization of the inference system of the logic. The usual soundness assumption for L implies that every model M of S also satisfies G. 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 I(S). Proving operational termination of declarative programs often involves two main ingredients: (i) the generation of logical models M to abstract the program execution (i.e., the provability of specific goals in I(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 M. 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.