Path: utzoo!mnetor!tmsoft!torsqnt!news-server.csri.toronto.edu!bonnie.concordia.ca!thunder.mcrcim.mcgill.edu!snorkelwacker.mit.edu!paperboy!think.com!linus!linus!linus!guttman From: guttman@mitre.org (Joshua D. Guttman) Newsgroups: comp.lang.scheme Subject: Re: Notions of program correctness (was Re: Tail-calling ...) Message-ID: Date: 18 Feb 91 20:48:56 GMT References: <9102112032.AA03542@cymbal.reasoning.com.> <908@anaxagoras.ils.nwu.edu> Sender: news@linus.mitre.org (News Service) Organization: Mitre Corporation, Bedford, MA. Lines: 18 In-Reply-To: carlton@husc10.harvard.edu's message of 18 Feb 91 21:04:59 GMT Nntp-Posting-Host: darjeeling.mitre.org If I'm reading the Scheme formal semantics aright, one unappealing, maybe downright wrong, aspect is that it definitely asserts that procedure call (in and of itself) can never lead to memory exhaustion. Thus, a program like: (define (laughable) (1+ (laughable))) should run forever without error on any "correct" implementation, even tho' it is *not* tail-recursive. I myself would advocate taking out all of the memory exhaustion tests from where they are in the current formal semantics, and treating the whole issue of the finiteness of memory at a lower level in modeling the formal behavior of implementations. So I suppose I would advocate saying that proper tail recursion should not change the mathematical *semantics* of a program, tho' it certainly changes something else: call it, perhaps, the pragmatics of the program. Josh