More on Unfold/Fold Transformations of Normal Programs: Preservation of Fitting's Semantics

Laurent Fribourg; Annalisa Bossi; Franco Turini; Sandro Etalle

doi:10.1007/3-540-58792-6_20

More on Unfold/Fold Transformations of Normal Programs: Preservation of Fitting's Semantics

Laurent Fribourg (Editor), Annalisa Bossi, Franco Turini (Editor), Sandro Etalle

Research output: Contribution to conference › Paper › peer-review

3 Citations (Scopus)

151 Downloads (Pure)

Abstract

The unfold/fold transformation system defined by Tamaki and Sato was meant for definite programs. It transforms a program into an equivalent one in the sense of both the least Herbrand model semantics and the Computed Answer Substitution semantics. Seki extended the method to normal programs and specialized it in order to preserve also the finite failure set. The resulting system is correct wrt nearly all the declarative semantics for normal programs. An exception is Fitting's model semantics. In this paper we consider a slight variation of Seki's method and we study its correctness wrt Fitting's semantics. We define an applicability condition for the fold operation and we show that it ensures the preservation of the considered semantics through the transformation.

Original language	Undefined
Pages	311-331
Number of pages	21
DOIs	https://doi.org/10.1007/3-540-58792-6_20
Publication status	Published - 1994
Event	4th Int. Workshop on Meta Programming in Logic (META) - Pisa, Italy Duration: 1 Jan 1994 → 1 Jan 1994

Workshop

Workshop	4th Int. Workshop on Meta Programming in Logic (META)
Period	1/01/94 → 1/01/94

Keywords

EWI-1178
IR-56280

Access to Document

10.1007/3-540-58792-6_20

bossi94more

Cite this

@conference{3d2fcaba7f5c41eb83668bb098ed06b6,

title = "More on Unfold/Fold Transformations of Normal Programs: Preservation of Fitting's Semantics",

abstract = "The unfold/fold transformation system defined by Tamaki and Sato was meant for definite programs. It transforms a program into an equivalent one in the sense of both the least Herbrand model semantics and the Computed Answer Substitution semantics. Seki extended the method to normal programs and specialized it in order to preserve also the finite failure set. The resulting system is correct wrt nearly all the declarative semantics for normal programs. An exception is Fitting's model semantics. In this paper we consider a slight variation of Seki's method and we study its correctness wrt Fitting's semantics. We define an applicability condition for the fold operation and we show that it ensures the preservation of the considered semantics through the transformation.",

keywords = "EWI-1178, IR-56280",

author = "Laurent Fribourg and Annalisa Bossi and Franco Turini and Sandro Etalle",

note = "Imported from DIES; 4th Int. Workshop on Meta Programming in Logic (META) ; Conference date: 01-01-1994 Through 01-01-1994",

year = "1994",

doi = "10.1007/3-540-58792-6_20",

language = "Undefined",

pages = "311--331",

}

TY - CONF

T1 - More on Unfold/Fold Transformations of Normal Programs: Preservation of Fitting's Semantics

AU - Bossi, Annalisa

AU - Etalle, Sandro

A2 - Fribourg, Laurent

A2 - Turini, Franco

N1 - Imported from DIES

PY - 1994

Y1 - 1994

N2 - The unfold/fold transformation system defined by Tamaki and Sato was meant for definite programs. It transforms a program into an equivalent one in the sense of both the least Herbrand model semantics and the Computed Answer Substitution semantics. Seki extended the method to normal programs and specialized it in order to preserve also the finite failure set. The resulting system is correct wrt nearly all the declarative semantics for normal programs. An exception is Fitting's model semantics. In this paper we consider a slight variation of Seki's method and we study its correctness wrt Fitting's semantics. We define an applicability condition for the fold operation and we show that it ensures the preservation of the considered semantics through the transformation.

AB - The unfold/fold transformation system defined by Tamaki and Sato was meant for definite programs. It transforms a program into an equivalent one in the sense of both the least Herbrand model semantics and the Computed Answer Substitution semantics. Seki extended the method to normal programs and specialized it in order to preserve also the finite failure set. The resulting system is correct wrt nearly all the declarative semantics for normal programs. An exception is Fitting's model semantics. In this paper we consider a slight variation of Seki's method and we study its correctness wrt Fitting's semantics. We define an applicability condition for the fold operation and we show that it ensures the preservation of the considered semantics through the transformation.

KW - EWI-1178

KW - IR-56280

U2 - 10.1007/3-540-58792-6_20

DO - 10.1007/3-540-58792-6_20

M3 - Paper

SP - 311

EP - 331

T2 - 4th Int. Workshop on Meta Programming in Logic (META)

Y2 - 1 January 1994 through 1 January 1994

ER -