Prolog的语义保持变换

程序变换方法在逻辑程序中的应用主要是基于这样的理论结果，即Fold/Unfold变换保持了逻辑程序的最小Herbrand模型语义和答复转换集语义，但是当逻辑程序的实现采用标准Prolog系统的最左计算规则和深度优先查找规则时，变换后的程序未必能保持原程序的语义，此外，程序的语义等价性证明也往往是难以理解和阅读的，为此，首先用与计算SLD－树叶结点有关的答复置换序列算法的方式，引入一个相对易于理解的Prolog语义定义，然后给出有关的语义保持变换规则并加以证明。

Sematics Hold Transformation for Prolog

The application of program transformation method to logic program is mainly based on such theory,namely,Fold/Unfold transformation holds the least Herbrand model semantics and the semantics of answer substitution set of logic program.However,when the leftmost computing rule and depth first searching rule of standard Prolog systems are adopted for implementing logic pragrams,the semantics of original program cannot necessarily be held by transformed program.Moreover,the proof of semantic equivalence of the program is often difficult to understand and to read.By the style of algorithm for computing answer substitution sequence relating to the node of leaves in SLD tree,the author puts forward a semantics definition of Prolog which is not diffcult to understand;and then,gives the rules for semantics hold transformation and offers proof.