PRESERVATION OF STRONGER EQUIVALENCE IN UNFOLD FOLD LOGIC PROGRAM TRANSFORMATION

被引:18
作者
KAWAMURA, T
KANAMORI, T
机构
[1] Mitsubishi Electric Corporation, Central Research Laboratory, Amagasaki, Hyogo, 661
关键词
D O I
10.1016/0304-3975(90)90065-P
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
This paper shows that Tamaki-Sato's unfold/fold transformation of Prolog programs preserves equivalence in a stronger sense that of the usual least Herbrand model semantics, which Tamaki and Sato originally showed. Conventionally, the semantics of Prolog program is defined by the least Herbrand model. However, the least Herbrand model does not always characterize what answer substitutions are returned. This paper proves that any program obtained from an initial program by applying Tamaki-Sato's transformation returns the same answer substitutions as the initial program for any given top-level goal. © 1990.
引用
收藏
页码:139 / 156
页数:18
相关论文
共 11 条
[1]   TRANSFORMATION SYSTEM FOR DEVELOPING RECURSIVE PROGRAMS [J].
BURSTALL, RM ;
DARLINGTON, J .
JOURNAL OF THE ACM, 1977, 24 (01) :44-67
[2]  
KANAMORI T, 1988, ICOT TR403 TECHN REP
[3]  
KANAMORI T, 1986, ICOT TR178 TECHN REP
[4]  
KANAMORI T, 1987, 4TH P INT C LOG PROG, P744
[5]  
KANAMORI T, 1986, US JAPAN WORKSHOP LO
[6]  
KAWAMURA T, 1988, 5TH P INT C GEN COMP, P413
[7]   SYNTHESIS - DREAMS -]PROGRAMS [J].
MANNA, Z ;
WALDINGER, R .
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1979, 5 (04) :294-328
[8]  
TAMAKI, 1986, TR8604 IB U DEP INF
[9]  
TAMAKI, 1987, PROGRAM TRANSFORMATI, P39
[10]  
TAMAKI H, 1984, 2ND P INT LOG PROGR, P127