On September 27 (10:11 +0200), Bjorn Lisper wrote with possible deletions:
| Adrian Hey <[EMAIL PROTECTED]>:
| >The issue I'm thinking about is equational reasoning and program
| >transformation. For a lazy (non-strict) language, transformations
| >are constrained so that a function definition which is non-strict
| >in an argument is never transformed into one which is strict in the
| >same argument. (Or so I believe, please correct me if I'm wrong).
| [...]
| Note that if we want the transformations to preserve the semantics of the
| language w.r.t. termination we will have to deal with bottom in equations
| also in strict languages, since also strict languages contain certain
| operations with nonstrict semantics (e.g., conditionals). Of course, we can
| consider a coarser semantics without the bottom, where we do not distinguish
| functions w.r.t. termination properties, and then have a different set of
| equalities: a good example is x - x = 0 which is valid if bottom is
| discarded but not valid if it is included. (I believe it may be this kind of
| discrepancy which has lead you to think that nonstrict languages do not
| permit equational reasoning.)
|
| [...]
| >Doesn't having to treat _|_ as a value spoil equational reasoning?
|
| No, see above.
I think that Dave Turner's ``Elementary Strong Functional
Programming'' explains this point quite well. Find it in the
Proceedings of Functional Programming Languages in Education (FPLE),
Nijmegen, Netherlands, December 1995, LNCS 1022.
Best wishes,
--Torsten
--
| Torsten Grust [EMAIL PROTECTED] |
| http://www.fmi.uni-konstanz.de/~grust/ |
| Database Research Group, University of Konstanz (Lake Constance/Germany) |
