Re: [math-fun] Is algebra necessary?
Carl Hewitt & I discussed this eta-tail recursion connection with Steele & Sussman re Scheme back in the 1970's when Steele & Sussman were pushing to make tail recursion a requirement for Scheme & other Lisp's (Maclisp at the time was _not_ tail recursive, nor was the Lisp Machine Lisp). I haven't checked recently, but I think that even Steele wasn't able to get tail-recursion into the Common Lisp standard. I think this discussion was prompted by Steve Ward's undergraduate course at MIT on lambda calculus circa 1975?? BTW, I found it very interesting that someone (Church??) had discovered that axiom eta was _independent_ of the other lambda calculus axioms. That alerted me that something important was going on. Perhaps I need to make some revisions to Wikipedia. If I could get through their gatekeeper... At 05:51 PM 8/2/2012, Mike Stay wrote:
On Thu, Aug 2, 2012 at 5:17 PM, Henry Baker <hbaker1@pipeline.com> wrote:
I.e., tail recursion. If bar is a function of one variable, wrapping a lambda(x) around it is useless & wastes stack space.
In Common Lisp:
#'(lambda (x) (bar x))
<=>
#'bar
Hmm. Bar is also in tail position here: (lambda (x) (bar (* x x))) and eta doesn't immediately apply, but I guess you could rewrite it as lambda(x).(bar o * o delta)(x) (where o is composition). That's interesting. Do you know of a paper that talks about that? Googling "tail recursion" "eta equivalence" turned up nothing.
At 04:58 PM 8/2/2012, Mike Stay wrote:
On Thu, Aug 2, 2012 at 4:44 PM, Henry Baker <hbaker1@pipeline.com> wrote:
Eta (I think this is the name?). Tail recursion. You can replace recursion by iteration in certain contexts.
Eta is extensionality, i.e. any term T of type X is eta-equivalent to (lambda x.T(x)) when x is not free in T and x has type X. -- Mike Stay - metaweta@gmail.com http://www.cs.auckland.ac.nz/~mike http://reperiendi.wordpress.com
-- Mike Stay - metaweta@gmail.com http://www.cs.auckland.ac.nz/~mike http://reperiendi.wordpress.com
On Thu, Aug 2, 2012 at 7:00 PM, Henry Baker <hbaker1@pipeline.com> wrote:
Carl Hewitt & I discussed this eta-tail recursion connection with Steele & Sussman
I'll have to ask him about it; I see him at a weekly meeting about object capabilities from time to time.
re Scheme back in the 1970's when Steele & Sussman were pushing to make tail recursion a requirement for Scheme & other Lisp's (Maclisp at the time was _not_ tail recursive, nor was the Lisp Machine Lisp). I haven't checked recently, but I think that even Steele wasn't able to get tail-recursion into the Common Lisp standard.
Apparently not: http://www.lispworks.com/documentation/HyperSpec/Body/03_bbc.htm
I think this discussion was prompted by Steve Ward's undergraduate course at MIT on lambda calculus circa 1975??
BTW, I found it very interesting that someone (Church??) had discovered that axiom eta was _independent_ of the other lambda calculus axioms. That alerted me that something important was going on.
I don't know about *independence*, but eta is *adjoint* to beta: http://www.paultaylor.eu/ASD/foufct/cattype.html -- Mike Stay - metaweta@gmail.com http://www.cs.auckland.ac.nz/~mike http://reperiendi.wordpress.com
participants (2)
-
Henry Baker -
Mike Stay