D. Tweed wrote:
>I'm as excited about the possibility of a limited form of compile time
>evaluation via rewrite rules but I'm a getting a bit worried that no-one
>has made any examples where there's an laziness to consider: I really
>wouldn't want semantic differences depending on the degree of optimization
>I compile with.
Simple compiler optimizations (hence the rewrite rules) can affect the
termination. Consider the following example:
Rule1 m+1 > m ==> True
if m > n then 3 else 5
where
m = n+1
n = _|_
Without optimizations this program will produce _|_ but
with optimizations it will produce 3.
Any time an optimization rule produces a constant or a term in weak
head normal form, the termination is affected. This may be
acceptable, however, because one will get only "more defined" answers.
A nastier consequence is that the language may be no longer confluent.
Consider the following variant of the above example:
Rule1 m+1 > m ==> True
if m > n then 3 else 5
where
m = n+1
n = m+1
Without optimizations this program will produce _|_ but
with optimizations it will produce either 3 or 5 !
These issues are discussed in a paper by Zena Ariola and myself [1].
I am of the opinion that such optimizations should be allowed.
Arvind
[1] Properties of First-Order functional languages with sharing.
Zena Ariola & Arvind
Journal of Theoretical Computer Science, 146 (1-2):69-108, July 1995