A transformational semantics of static embedded implications of normal logic pro

Abstract

There are mainly two approaches for structuring logic programs. The first one is based on defining some notion of program unit or module and on providing a number of composition operators. The second approach consists in enriching logic programming with a mechanism of abstraction and scoping rules that are frequently found, for instance, in procedural programming. More precisely, this approach has been advocated by Miller and others using implications embedded in the goals of the given program as a structuring mechanism. However, as Giordano, Martelli and Rossi pointed out, we can associate two different visibility rules (static and dynamic) to this kind of structuring mechanism where, obviously, the semantics of the given program depends on the chosen rule. In this paper we consider normal constraint logic programs (with constructive negation á la Drabent as operational semantics) extended with embedded implications with a static visibility rule. This class of programs combines the expressive power of normal programs with the capability to organize and to enhance dinamically their sets of clauses. In particular, first, we introduce an operational semantics based on constructive negation for this class of programs, taking into account the static visibility rule. Then, we present an alternative semantics in terms of a transformation of the given structured program into a flat one. Finally, we prove the adequacy of this transformation by showing that it preserves the computed answers of the given program. Obviously, this transformation semantics can be used as the basis for an implementation of this structuring mechanism. © Springer-Verlag Berlin Heidelberg 2006.