home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #16 / NN_1992_16.iso / spool / comp / lang / function / 928 < prev    next >
Encoding:
Internet Message Format  |  1992-07-21  |  4.2 KB
  1. Path: sparky!uunet!mcsun!uknet!edcastle!dcs.ed.ac.uk!smk
  2. From: smk@dcs.ed.ac.uk (Stefan Kahrs)
  3. Newsgroups: comp.lang.functional
  4. Subject: Re: Lazy languages considered questionable
  5. Message-ID: <SMK.92Jul21164155@scarp.dcs.ed.ac.uk>
  6. Date: 21 Jul 92 15:41:55 GMT
  7. References: <BrFpJ9.2Ky@news.cso.uiuc.edu> <1992Jul20.190137.10410@mnemosyne.cs.du.edu>
  8.     <1992Jul20.213929.10686@m.cs.uiuc.edu>
  9.     <1992Jul21.093354.16474@doc.ic.ac.uk>
  10. Sender: nnews@dcs.ed.ac.uk
  11. Distribution: comp
  12. Organization: University of Edinburgh, LFCS
  13. Lines: 93
  14. In-reply-to: sjv@doc.ic.ac.uk's message of 21 Jul 92 09:33:54 GMT
  15.  
  16. VM=Vance Morrison
  17. SV=Steve Vickers
  18.  
  19. VM   >The bottom line is that if you REALLY want to abstract order of 
  20. VM   >evaluation away, you have to use a STRONGLY NORMALIZING language
  21. VM   >(they do exist, take type theory for example).   Now order of evaluation
  22. VM   >truely doesn't matter since any evaluation order terminates.  
  23.  
  24. SV   On the face of it, evaluation order is related more closely to the
  25. SV   Church-Rosser property than to strong normalization.
  26.  
  27. An addition to Steve Vickers' remark:
  28. Take Standard ML without side-effects, but with exceptions:
  29. if you evaluate with different strategies, you can get _different_
  30. results, because an exception-raising expression can be dropped in a
  31. non-strict evaluation.
  32.  
  33. ---
  34.  
  35. But the Church-Rosser (CR) does not give you the whole story.
  36. The CR property is a property of the full
  37. (non-deterministic) evaluation relation,
  38. but when we deal with strategies,
  39. we deal with subrelations of the evaluation.
  40. Although in principle we are _interested_ in the full evaluation
  41. relation, we actually _deal_ only with this particular subrelation.
  42.  
  43. If our evaluation relation is CR, our strategy cannot go "wrong".
  44. "But does it go right?" is a different thing.
  45. Note that the question can mean different things, for example:
  46.  
  47.       -    Suppose t and u are equal wrt. forward/backward evaluation.
  48.     Does the strategy F find a common reduct, i.e. are there
  49.     numbers m and n, such F^m(t) and F^n(u) are identical?
  50.  
  51.       -    Suppose t has a normal form u.
  52.     Does the strategy F find it,
  53.     i.e. is there a number n such that F^n(t)=u?
  54.  
  55. Notice that the first property is very strong
  56. and implies the second one (in Barendregt's Lambda-Calculus book
  57. the first property is called CR [for strategies],
  58. the second one "normalising").
  59.  
  60. Leftmost-outermost evaluation for lambda-calculus is normalising, but it
  61. does not have the stronger CR-property.
  62.  
  63. As long as we are only interested in normal forms, the "normalising"
  64. property is quite sufficient. But:
  65. An unfortunate property of functional languages with pattern
  66. matching is that their definitions are more like term rewriting rules.
  67. For term rewriting systems, even of this particular form,
  68. leftmost-outermost reduction is _not_ normalising.
  69. Example:
  70.  
  71.     myand False x = False
  72.     myand x False = False
  73.     myand True True = True
  74.  
  75. For the above definition (in Miranda),
  76. the term (myand undef False) is obviously equal to False,
  77. but it does not evaluate to it. Switching the first two
  78. equations makes it defined in Miranda.
  79.  
  80. The example shows that evaluation order does matter in lazy languages
  81. (I bet in Haskell happens the same), their evaluation strategy
  82. is _not_ normalising.
  83. That doesn't mean that there is no such strategy (indeed there is),
  84. but it is much harder to implement it efficiently.
  85.  
  86. Of course one can claim that definitons like the one above are
  87. only syntactic sugar for certain nested case-expressions,
  88. and that for those everything is fine, but this misses the point:
  89. As a programmer, I think of the equations I write down as equations
  90. and not as nested case-expressions, and I would like to be able to
  91. manipulate them as I usually manipulate equations.
  92. In other words: I would like the semantics to keep the promises
  93. the syntax makes.
  94.  
  95. I don't have this in strict languages, but -- as I pointed out --
  96. I don't have it either in lazy languages.
  97.  
  98.  
  99.  
  100.  
  101.  
  102. --
  103. Stefan Kahrs                       JANET:    smk@uk.ac.ed.dcs
  104. LFCS, Dept. of Computer Science    Internet: smk@dcs.ed.ac.uk
  105. University of Edinburgh            UUCP:     ..!mcsun!uknet!dcs!smk
  106. Edinburgh                          ARPA:     smk%dcs.ed.ac.uk@nsfnet-relay.ac.uk
  107. EH9 3JZ                            Tel:      (44)-31-650-5139
  108. SCOTLAND                           Fax:      (44)-31-667-7209
  109.