🚀 go-pugleaf

VM=Vance Morrison
SV=Steve Vickers

VM   >The bottom line is that if you REALLY want to abstract order of 
VM   >evaluation away, you have to use a STRONGLY NORMALIZING language
VM   >(they do exist, take type theory for example).   Now order of evaluation
VM   >truely doesn't matter since any evaluation order terminates.  

SV   On the face of it, evaluation order is related more closely to the
SV   Church-Rosser property than to strong normalization.

An addition to Steve Vickers' remark:
Take Standard ML without side-effects, but with exceptions:
if you evaluate with different strategies, you can get _different_
results, because an exception-raising expression can be dropped in a
non-strict evaluation.

---

But the Church-Rosser (CR) does not give you the whole story.
The CR property is a property of the full
(non-deterministic) evaluation relation,
but when we deal with strategies,
we deal with subrelations of the evaluation.
Although in principle we are _interested_ in the full evaluation
relation, we actually _deal_ only with this particular subrelation.

If our evaluation relation is CR, our strategy cannot go "wrong".
"But does it go right?" is a different thing.
Note that the question can mean different things, for example:

      -	Suppose t and u are equal wrt. forward/backward evaluation.
	Does the strategy F find a common reduct, i.e. are there
	numbers m and n, such F^m(t) and F^n(u) are identical?

      -	Suppose t has a normal form u.
	Does the strategy F find it,
	i.e. is there a number n such that F^n(t)=u?

Notice that the first property is very strong
and implies the second one (in Barendregt's Lambda-Calculus book
the first property is called CR [for strategies],
the second one "normalising").

Leftmost-outermost evaluation for lambda-calculus is normalising, but it
does not have the stronger CR-property.

As long as we are only interested in normal forms, the "normalising"
property is quite sufficient. But:
An unfortunate property of functional languages with pattern
matching is that their definitions are more like term rewriting rules.
For term rewriting systems, even of this particular form,
leftmost-outermost reduction is _not_ normalising.
Example:

	myand False x = False
	myand x False = False
	myand True True = True

For the above definition (in Miranda),
the term (myand undef False) is obviously equal to False,
but it does not evaluate to it. Switching the first two
equations makes it defined in Miranda.

The example shows that evaluation order does matter in lazy languages
(I bet in Haskell happens the same), their evaluation strategy
is _not_ normalising.
That doesn't mean that there is no such strategy (indeed there is),
but it is much harder to implement it efficiently.

Of course one can claim that definitons like the one above are
only syntactic sugar for certain nested case-expressions,
and that for those everything is fine, but this misses the point:
As a programmer, I think of the equations I write down as equations
and not as nested case-expressions, and I would like to be able to
manipulate them as I usually manipulate equations.
In other words: I would like the semantics to keep the promises
the syntax makes.

I don't have this in strict languages, but -- as I pointed out --
I don't have it either in lazy languages.





--
Stefan Kahrs	                   JANET:    smk@uk.ac.ed.dcs
LFCS, Dept. of Computer Science    Internet: smk@dcs.ed.ac.uk
University of Edinburgh            UUCP:     ..!mcsun!uknet!dcs!smk
Edinburgh                          ARPA:     smk%dcs.ed.ac.uk@nsfnet-relay.ac.uk
EH9 3JZ                            Tel:      (44)-31-650-5139
SCOTLAND                           Fax:      (44)-31-667-7209