home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #26 / NN_1992_26.iso / spool / comp / lang / function / 1354 < prev    next >
Encoding:
Text File  |  1992-11-12  |  2.1 KB  |  47 lines
  1. Newsgroups: comp.lang.functional
  2. Path: sparky!uunet!mcsun!sunic!sics.se!bjornl
  3. From: bjornl@sics.se (Bj|rn Lisper)
  4. Subject: Re: Is efficient backtracking feasible in functional languages?
  5. In-Reply-To: joe@erix.ericsson.se's message of Wed, 11 Nov 1992 17:17:42 GMT
  6. Message-ID: <BJORNL.92Nov12145318@rama.sics.se>
  7. Sender: news@sics.se
  8. Organization: Swedish Institute of Computer Science, Kista
  9. References: <1992Nov10.164456.18062@email.tuwien.ac.at> <TMB.92Nov11104119@arolla.idiap.ch>
  10.     <1992Nov11.171742.18783@eua.ericsson.se>
  11. Date: Thu, 12 Nov 1992 13:53:18 GMT
  12. Lines: 33
  13.  
  14. In article <1992Nov11.171742.18783@eua.ericsson.se> joe@erix.ericsson.se
  15. (Joe Armstrong) writes:
  16. >|> 
  17. >|>    strangesucc n =    hd [x|x<-[0..];x>n];
  18. >|> 
  19.        ....
  20.  
  21. >    Wonderfull  !!
  22. >    This is the kind of stuff that gives FP a bad name :-)
  23. >    Is their a transformation system which can prove that
  24. >    strangesucc x == x + 1 ?
  25.  
  26. Was strangesucc a function from natural numbers or integers? In the latter
  27. case "strangesucc x == x + 1" is false for x < 0. For natural numbers, quite
  28. intricate knowledge about them is required to prove the equality: we must
  29. know that n+1 is the least natural number such that n < n+1, for instance,
  30. we must know that this number will, for all n, eventually show up in the
  31. list defined by [x|x<-[0..]], and we must know that it is the first such
  32. number that shows up. The latter two facts must be proved by induction, I
  33. think, ultimately using the Peano axioms for natural numbers. The proof also
  34. implies a proof of termination for the function. So, my answer is "not
  35. without theorem proving capabilities".
  36.  
  37. A more general data flow analysis should, however, at least be able to find
  38. that at most two elements in the list [x|x<-[0..]] need to be stored
  39. simultaneously. This is since only one element is returned, every element in
  40. the list can be computed using only the previous element, and the
  41. termination test involves only the element to be returned and the argument
  42. to the function. So a smart compiler should throw away the "internal" list
  43. [x|x<-[0..]] completely and allocate two registers instead.  Apparently
  44. compilers today aren't that smart.
  45.  
  46. Bjorn Lisper
  47.