Completeness of Some Transformation Strategies for Avoiding Unnecessary Logical Variables
Pascal Van Hentenryck · 1994
An unnecessary variable of a logic clause is a variable which either occurs more than once in the body or it doesnot occurin the head.Unnecessary variables oftencause inefficiency, because during program execution they generate redundant computations andcreate useless intermediate structures. In order to eliminate the unnecessary variables from a given program. we may apply transformation strategies based on the application of the unfold/fold rules. Some of these strategies have been presented in a previous paper of ours [17]. can be formulated as follows: given a set R of transformation rules. we say that a strategy S is complete w.r.t. R iff for any given program P, if P can be transformed into an equivalent program Q without unnecessary variables by an arbitrary use of the rules in R. then P can be transformed into an equivalent program (possibly different from ϱ without unnecessary variables by using the strategy S.