vanroy@ji.Berkeley.EDU (Peter Van Roy) (09/12/88)
Is it allowable for a program transformation to change the procedural semantics of a program while retaining the declarative semantics? For example, consider the predicate defined by the following two clauses: :-mode(max(input,input,output)). max(A, B, A) :- A>=B. max(A, B, B) :- A=<B. This is a declaratively correct specification of the maximum relation, and it gives two solutions when A=B. Is a program transformation allowed to change these clauses into: max(A, B, A) :- A=:=B. max(A, B, A) :- A>B. max(A, B, B) :- A<B. or into: max(A, B, A) :- A>=B, !. max(A, B, B) :- A=<B. The transformed versions are declaratively equivalent to the original specification, and they give only one solution when A=B. Has a discussion of this question been published anywhere? Peter Van Roy vanroy@ji.Berkeley.edu
ok@quintus.uucp (Richard A. O'Keefe) (09/12/88)
In article <26045@ucbvax.BERKELEY.EDU> vanroy@ji.Berkeley.EDU (Peter Van Roy) writes: >Is it allowable for a program transformation to change the >procedural semantics of a program while retaining the >declarative semantics? It is if and only if the person using the program transformation says it is. For example, in NU Prolog, the ":- pure" declaration is a statement by the programmer that s/he only cares about the declarative semantics. A "recursion editor" such as Alan Bundy proposes (or even my little unfolding toy) would (does) work solely at the declarative level, so would be (is) allowed to do anything that preserves declarative semantics. But an optimising compiler would not be allowed to change the operational semantics (in the absence of :- pure declarations). This is a problem in other languages as well. (For example, "lazy" evaluation is *very* sensitive to the syntactic form of programs.)