🚀 go-pugleaf

In article <1992Nov10.164456.18062@email.tuwien.ac.at> ulrich@mips.complang.tuwien.ac.at (Ulrich Neumerkel E185/1 +43158801/4477) writes:

   In many textbooks and papers about functional languages it is suggested
   that lazy evaluation allows to implement backtracking by representing
   the sequence of solutions by an appropriate datastructure which is
   generated in a lazy manner. Is seems however, that such an encoding,
   although conceptually elegant, requires space proportional to the
   number of choices already considered.

   [...]

   strangesucc n =	hd [x|x<-[0..];x>n];

   This program should run in constant space and linear time [1].
   However, for the implementations I tried, it turns out that the program
   seems to run in linear space! For a small n as 10000 the program aborts
   due to memory problems. Also a rewriting of the program to encode list
   comprehensions explicitly did not yield the desired result.

   Is there ANY implementation of a lazy functional language to execute
   the program above in an efficient manner (i.e. in constant space)?

There should be no problem with that in principle. For example, the
following program, using a lazy streams library in SML, only requires
constant space (3397288 bytes). Of course, it garbage collects a
lot...

  - Stream.head(Stream.filter(fn x => x > 1000000,Stream.iota()));
  
  [Major collection... 21% used (3397260/15733684), 1920 msec]
  
  [Major collection... 21% used (3397288/15730836), 1910 msec]
  
  [Major collection... 21% used (3397288/15730948), 1920 msec]
  
  [Major collection... 21% used (3397288/15730888), 1920 msec]
  
  [Major collection... 21% used (3397288/15730888), 1910 msec]
  val it = 1000001 : int
  -

In general, I think that backtracking is better expressed using
callcc; is there some equivalent to callcc in lazy languages?

					Thomas.

|> 
|>    strangesucc n =	hd [x|x<-[0..];x>n];
|> 
	....
|> 
|>   - Stream.head(Stream.filter(fn x => x > 1000000,Stream.iota()));
|>   
|>   [Major collection... 21% used (3397260/15733684), 1920 msec]
|>   
|>   [Major collection... 21% used (3397288/15730836), 1910 msec]
|>   
|>   [Major collection... 21% used (3397288/15730948), 1920 msec]
|>   
|>   [Major collection... 21% used (3397288/15730888), 1920 msec]
|>   
|>   [Major collection... 21% used (3397288/15730888), 1910 msec]
|>   val it = 1000001 : int
|>   -

	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 ?

	Joe

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

In article <1992Nov10.164456.18062@email.tuwien.ac.at> ulrich@mips.complang.tuwien.ac.at writes:
>
>strangesucc n =	hd [x|x<-[0..];x>n];
>
>This program should run in constant space and linear time [1].
>However, for the implementations I tried, it turns out that the program
>seems to run in linear space! For a small n as 10000 the program aborts
>due to memory problems. Also a rewriting of the program to encode list comprehensions explicitly did not yield the desired result.
>
>Is there ANY implementation of a lazy functional language to execute
>the program above in an efficient manner (i.e. in constant space)?
>-- 
>Ulrich Neumerkel, ulrich@dec4.wu-wien.ac.at ulrich@mips.complang.tuwien.ac.at
>TU-Wien, Vienna University of Technology, +431 58801 4477 fax +431 5057838
>Institut fuer Computersprachen E185/1 Argentinierstr.8/4, A-1040 Wien Austria


I've tried this on an implementation based on the G-machine. My machine
uses the blackholing technique to avoid space leaks that I describe in [1].
I translate list comprehensions to their equivalent using foldr, map and
concat; for example see [2].
I have no problem with this function: it runs in constant space (262 words
of heap space if you want to compare figures with those give in [1]).

[1] Richard E. Jones. `Tail recursion without space leaks', Journal of 
    Functional Programming 2(1), 73--79, January 1992.
    
[2] Richard Bird & Phil Wadler. `Introduction to Functional Programming', 
    Prentice Hall, 1988. Page 63.


Richard Jones

===============================================================================

Computing Laboratory				email: rej@ukc.ac.uk
University of Kent at Canterbury		Telephone: 0227 764000 ext.7550
Canterbury, CT2 7NF, U.K.			FAX: 0227 762811

===============================================================================

In article <1992Nov10.164456.18062@email.tuwien.ac.at> Ulrich Neumerkel
E185/1 +43158801/4477, ulrich@mips.complang.tuwien.ac.at writes:

>strangesucc n =	hd [x|x<-[0..];x>n];
>
>This program should run in constant space and linear time [1].
>However, for the implementations I tried, it turns out that the program
>seems to run in linear space! For a small n as 10000 the program aborts
>due to memory problems. Also a rewriting of the program to encode list 
>comprehensions explicitly did not yield the desired result.

The following rewrite yields the desired result in constant space
in Haskell B:

main = print (h::Integer)

hd (e:l) = e

g n = n : g (n+1)

f [] n = []
f (x:v) n = if (x>n)
               then (x:f v n)
               else (f v n)

h :: Integer
h = hd (f (g 0) 1000000)

But if you change the function 'main' to:

main = print (hd (f (g 0) 1000000)::Integer)

the program runs in linear space !

>Is there ANY implementation of a lazy functional language to execute
>the program above in an efficient manner (i.e. in constant space)?

Yes, Chalmers LML implementation.


                         John van Groningen