Path: utzoo!utgpu!news-server.csri.toronto.edu!bonnie.concordia.ca!thunder.mcrcim.mcgill.edu!snorkelwacker.mit.edu!usc!elroy.jpl.nasa.gov!swrinde!zaphod.mps.ohio-state.edu!casbah.acns.nwu.edu!ils.nwu.edu!krulwich
From: krulwich@ils.nwu.edu (Bruce Krulwich)
Newsgroups: comp.lang.scheme
Subject: Notions of program correctness (was Re: Tail-calling ...)
Message-ID: <908@anaxagoras.ils.nwu.edu>
Date: 18 Feb 91 18:14:34 GMT
References: <9102112032.AA03542@cymbal.reasoning.com.> <harlan.666514120@copper> <CARLTON.91Feb15122042@husc10.harvard.edu> <HANCHE.91Feb17002434@hufsa.imf.unit.no>
Sender: news@ils.nwu.edu
Reply-To: krulwich@ils.nwu.edu (Bruce Krulwich)
Organization: Institute for the Learning Sciences, Northwestern University, Evanston, IL 60201
Lines: 41
In-reply-to: hanche@imf.unit.no (Harald Hanche-Olsen)

[A discussion was started about tail call optimization effecting the
"correctness" of a program.  It was pointed out that tail call optimization 
doesn't effect what programs will run, only how efficient they will be.  In
response to this...]

hanche@imf (Harald Hanche-Olsen) writes:
>On a machine with infinite memory, optimizing tail recursion does not
>change the meaning of programs.  However, in Scheme you can write a
>loop using a tail call and the loop can execute millions of times
>without running out of memory if it can do it once.  I'd say that
>whether or not the program runs out of memory changes its meaning,
>whether the semantics say so or not ...

In Scheme you can write a program that uses CONS that will run out of memory
on a machine with a 5-byte heap.  Does that mean that no program that uses
CONS can be assumed to work across Scheme implementations?  Also, in Scheme
it is possible to write a recursive (non-tail) function that will run out of
memory on some implementations.  Does that mean that any recursive
(non-tail) function in Scheme doesn't have the same meaning across
implementations?

The R3RS semantics (and presumably the more recent ones) include the notion
that CONS may run out of memory, and it seems that the other relevent areas
do too (e.g., tieval), although I'm not comfortable enough with the
semantics notation to say for sure.  Given these semantics, the "meaning" of
programs seems to be constant across machines with varying amounts of
memory.  It would seem to me that the same notion should apply to languages
which may stack-handle all calls.

The conclusion that I draw from this is that the handling of tail-recursion
is an efficiency issue but not a program correctness/validity issue.  

This is not to say, of course, that Scheme implementations aren't required
to be tail-recursive, or that tail-call optimization isn't a virtually
necessary aspect of a Scheme or LISP system from a pragmatic point of view.


Bruce Krulwich
Institute for the Learning Sciences