🚀 go-pugleaf

In article <1992Nov11.171742.18783@eua.ericsson.se> joe@erix.ericsson.se
(Joe Armstrong) writes:
>|> 
>|>    strangesucc n =	hd [x|x<-[0..];x>n];
>|> 
	   ....

>	Wonderfull  !!
>	This is the kind of stuff that gives FP a bad name :-)
>	Is their a transformation system which can prove that
>	strangesucc x == x + 1 ?

Was strangesucc a function from natural numbers or integers? In the latter
case "strangesucc x == x + 1" is false for x < 0. For natural numbers, quite
intricate knowledge about them is required to prove the equality: we must
know that n+1 is the least natural number such that n < n+1, for instance,
we must know that this number will, for all n, eventually show up in the
list defined by [x|x<-[0..]], and we must know that it is the first such
number that shows up. The latter two facts must be proved by induction, I
think, ultimately using the Peano axioms for natural numbers. The proof also
implies a proof of termination for the function. So, my answer is "not
without theorem proving capabilities".

A more general data flow analysis should, however, at least be able to find
that at most two elements in the list [x|x<-[0..]] need to be stored
simultaneously. This is since only one element is returned, every element in
the list can be computed using only the previous element, and the
termination test involves only the element to be returned and the argument
to the function. So a smart compiler should throw away the "internal" list
[x|x<-[0..]] completely and allocate two registers instead.  Apparently
compilers today aren't that smart.

Bjorn Lisper