Path: utzoo!attcan!uunet!husc6!mailrus!nrl-cmf!ames!zodiac!SUMEX-AIM.STANFORD.EDU!mxh
From: mxh@SUMEX-AIM.STANFORD.EDU (Max Hailperin)
Newsgroups: comp.lang.scheme
Subject: Re: Re^2: Scheme Digest #8, Efficiency of Y
Message-ID: <CMM.0.88.595806617.mxh@sumex-aim.stanford.edu>
Date: 17 Nov 88 21:50:17 GMT
Sender: daemon@zodiac.UUCP
Lines: 38

What I had in mind was something like this:

(letrec ((p (lambda () p)))
   (eqv? p (p)))

This is will evaluate to #t, according to R^3R.

On the other hand, if we rewrite this as

(let ((p (Y (lambda (p) (lambda () p)))))
  (eqv? p (p)))

then it is undefined whether the result will be #t or #f.  For a
straightforward impelementation of Y, it will probably be #f, but for an
optimized one, it would be #t.

The problem is not, as you suggested, from two occurences of (Y (lambda
...)), but from the difference between the procedure as the outside world
knows it vs. as it knows itself.

Now that I've explained myself, let me try to answer your question about the
definition of eqvness of procedures.  The problem with defining it as
alpha-convertability [plus same environment] is two fold:
 1) It is not in keeping with the philosophy as to what a procedure is.  In
    particular, contrary to some other languages, scheme doesn't allow you to
    "reopen" a closure: they are black boxes which can only be applied.
 2) It can lead to inefficiencies of two sorts (one obvious, one less so):
    a) if the implementation doesn't choose to fold together procedures
       which are eqv in your sense, then testing eqvness is slow
    b) if the implementation *does* choose to fold together procedures which
       it can determine are operationally equivalent but *not* eqv in your
       sense, then your eqv test becomes impossible -- so such a compiler
       optimization has to be ruled out, at a possible loss in speed.

2b in particular essentially is a way of saying that you want to
define into the language spec a particular level of
compiler-optimization smarts.  That's unwise.  Moreover, the existing
definition turns out to work well in practice.