Directions of Operational Termination





Publicado en

Actas de las XVIII Jornadas de Programación y Lenguajes (PROLE 2018)

Licencia Creative Commons


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.


Acerca de Lucas, Salvador

Palabras clave

General Logics, Operational Termination, Program Termination
Página completa del ítem
Notificar un error en este artículo
Mostrar cita
Mostrar cita en BibTeX
Descargar cita en BibTeX