Michael Hanus wrote:

...

E.g., in Haskell you can always replace equals by equals without changing the meaning of a program. In your example `g 0' is equal to bottom so it should be possible to replace it by any other bottom without any change in meaning. But if I define h x = h x and evaluate `f (g 0) (h 0)' I will no longer get 0.

So this definitions of non-linear patterns is not an option for a language that claims to be "referentially transparent" (whatever that means :).

I agree and the question is about "whatever that means"...

Term rewriting systems (TRS) are based on replacing equals by equals and that could be also considered as "referentially transparent".

Yes, but a TRS has a different semantics than Haskell. In TRS you manipulate terms, in Haskell you manipulate (the extension) of functions (OK, OK, there's stuff that looks like constructors, but it's all encodable as lambda terms).

Nevertheless, TRSs usually allow non-linear left-hand sides (but often come with other restrictions like termination). BTW, (g 0) and (h 0) are not considered as equal since there are no rules/equations to transform one into the other.

But in Haskell they are equal since their denotations are equal.

However, I agree that there are good reasons (mainly, operational simplicity) to allow only linear patterns and constructor-based rules in a real programming language, since non-linear patterns or non-constructor-based rules require other and more advanced operational principles. I only wanted to remark that there is no simple way to translate non-linear pattterns into linear patterns in the general case.

I think we are in agreement, I just wanted to point out that if you've decided on the particular "functional style" semantics that Haskell has, then you cannot have the kind of non-linear patterns that you exemplified. -- -- Lennart

On 20-Mar-2001, Jerzy Karczmarczuk wrote:

Logic languages which allow for nonlinear patterns use unification, which is usually much more costly than simple pattern compiling.

That's true, but the exceptions are important. If you have sufficient compile-time mode information, then unification need not be more costly than simple pattern matching.

What is the status of the referential transparency of Prolog or Mercury?

As Michael Hanus said, Prolog is not referentially transparent because it has a large variety of builtins that violate referential transparency. For Mercury, the short answer is that yes, Mercury is referentially transparent. Still, I guess you want the long answer ;-) Mercury's declarative semantics are referentially transparent. Modifying some Mercury program by replacing equals with equals always preserves the program's declarative semantics. However, such transformations do not necessarily preserve the operational semantics; the transformed program may not terminate when the original does, or may compute the set of solutions in a different order. The same is true for pure Prolog. Haskell's denotational semantics is referentially transparent. AFAIK Haskell doesn't have a standard operational semantics, but the typical operational semantics used are also referentially transparent. However, if you use a more detailed operational semantics, e.g. one which takes into account the fact that machines have finite memory, then the same kind of thing applies to Haskell too: replacing equals with equals may not preserve the operational semantics, because the transformed program may run out of memory when the original didn't. -- Fergus Henderson | "I have always known that the pursuit | of excellence is a lethal habit" WWW: http://www.cs.mu.oz.au/~fjh | -- the last words of T. S. Garp.