Re: Lambda calculus and it relation to LISP

[William Elliot]

Gareth.McCaughan@pobox.com retorted:
> William Elliot wrote:
>  _ Alpha-conversion (rename a variable) and eta-reduction
>  _ (turn \x.(f x) into f, when that's safe). The one I
>  _ mentioned above is beta-reduction. Yes, the proviso
>  _ you quote is correct. I was simplifying.
> When's an eta-reduction safe?  Lx.Nx -> N, provided no free x in N ?
> Was this actually used by Alanzo Church or did he merely mention it?
 _ I am not (nor have I claimed to be) an expert on the
 _ work of Church, although I do know that his first name
 _ is spelt "Alonzo".
Good to know as I'd like to locate a copy of his original work.

 _ When I say "lambda calculus", I do not necessarily mean "exactly
 _ what Church wrote about, with no consideration of anything
 _ developed later".
Briefly looking thru Google, I discovered what's become of his work is
nearly unrecognizable.

> >  _ Important features of the lambda calculus
> >  _ 1. In the lambda calculus, *everything* is a function.
> >  _ 2. In so far as the lambda calculus has a preferred "order
> >  _    of evaluation", it's "normal order", which amounts to
> >  _    evaluating things as you need them.
> > What's this normal order?
>  _ Always reduce the leftmost thing available.
>  _ In particular, when you have an application "f x", you
>  _ always prefer to reduce things in f before things in f.
> What about conversion rules like:
>       N -> M ==> NK -> MK
>       N -> M ==> KN -> KM
>       N -> M ==> Lx.N -> Lx.M ?
 _ What about them?
Are they allowed or prevented by the normal order of -> reductions?

> > Other questions:
> >  _ ((lambda (g n) (g g n))
> >  _  (lambda (f n) (if (= 0 n) 1 (* n (f f (- n 1))))) 5)
> >
> > (Lgn.ggn)(Lfn.if(=0n)1 (*n(ff(-n1))))5)
 _ I'd just like to mention that it was not I who wrote
 _ the _-quoted material there.
Correct, I was hoping you'd know or others in the thread would notice.

> > What's the lambda formula for
> >     = as in =0n
> >     if as in if(=0n)1
> >     - as in -n1 ?
>  _ I believe you know the answers to all these questions :-).
> Conclusion jumper.
 _ I believe that for each of those questions, you either know a good
 _ answer or believe with some reason that there is no good answer.
Not so.

 _ (I happen to find being addressed in this way rather
 _ disagreeable, but that's not your problem. :-))
I too felt poorly addressed by an abrupt uninformative response.

>                     Alanzo didn't define a - I know of.
> His = was rather complicated as I recall, being effective to
>       to work just for his numbers.  What I know not.
> As for 'if', where did that come from?  Again just for Church numbers?
 _ I would expect = to be quite complicated.
I'd expect so too.  I remember something vaguely so.

 _ I have no idea whether Church defined subtraction,
I'm not sure he did.  Nor dare I vouch he didn't.

 _ but it's not especially hard (though you'd want to
 _ take some care about the domain, if working generally
 _ with only non-negative integers). (Note that "quite
 _ complicated" and "not especially hard" are consistent;
 _ I would expect = and - to be roughly equally hard.)
I'd expect the usefulness of the expression would be limited
to Church numbers.

 _ I don't understand what you mean by "just for Church
 _ numbers?" regarding "if"; it would be "just for Church
 _ booleans", which IIRC are
 _   T ::= \xy.x
 _   F ::= \xy.y
That I'm beginning to find out.  F by the way is Church numeral 0.

 _ or perhaps the other way around. Then "if" is almost
 _ trivial:
 _   if ::= \xyz.xyz
 _ but you don't actually need an "if", since the boolean
 _ itself will do the work for you. So you can translate
 _ "if C then X else Y" into CXY.
Yes, I was thinking that.  So if ::= Lxyz.xyz is mostly for
        ease in reading and understanding expressions.

> > and finally, let as in
> > (let ((f (lambda (f n)
> >             (if (= 0 n) 1 (* n (f f (- n 1))))))
> >       (n 5))
> >    (f f n))
> >  _ Recursion without a function actually calling itself!
 _ Note, again, that I didn't write any of that.
Your comments have been are helpful.

>  _ (let ((x y)) E) === ((lambda (x) E) y).
> Doesn't make sense.  Are there expressions A,B for which
>       A(xy) -> x and B(xy) -> y ?
> I don't see how 'let' could be a wwf of the L-calculus.
 _ I never suggested that "let" is a wff of the lambda
 _ calculus. I don't think the person who wrote the "let"
 _ stuff did, either. However, expressions using "let"
 _ are readily translated into ones using "lambda" instead,
 _ and neat tricks like Y are expressible in the lambda
 _ calculus even if they're nicer to read when written
 _ using "let". (For people used to "let", anyway.)
Thanks for confirming that.  When it comes to lambda calculi I feel like
I'm speaking ye olde King's English.

--
 _ There *were* no computers, I think, when
 _ Church started working on the lambda calculus.
I read his work in the late fifties and was much enamored by it.
As I recall, it was published in the late 1930's

 _ Hmm, OK. At this point what you're talking about really
 _ isn't "the lambda calculus"; that was one of the points
 _ I was making (and William Elliot too, I think). It's just
 _ a notation for functions that happens to use the word
 _ "lambda". This isn't a problem, by the way, but it's
 _ worth being aware of it.
Indeed.

 _ The advantage of making anonymous functions is threefold.
Yes, one notation I've seen is (x_i)_i or (x_i)_(i in I).
For example (2^n)_n or (2^n)_(n in N);
        also (2^r)_r or to be exact (2^r)_(r in R)
is the function f(x) = 2^x

 _ 1. As you say, it saves a name which would otherwise
 _    clutter up some namespace or other.
 _ 2. It's more compact.
 _ 3. It lets you define the function where it's being used,
 _    rather than putting it somewhere else and making the
 _    reader check back for the definition.

-- recursion from afar
>   ((lambda (g n) (g g n))
>    (lambda (f n) (if (= 0 n) 1 (* n (f f (- n 1))))) 5)
>
So it's ok to understand that by thinking about
((lambda (g n) (g g n))
(lambda (f n) ((= 0 n) 1 (* n (f f (- n 1))))) 5)

(Lfn.ffn) (Lfn.(=0n)1(*n(ff(-n1)))) 5

Have I decipher 5 correctly as the number of iterations?
Well then, what happens with (my conclusion at end)
(Lfn.ffn) (Lfn.(=0n)1(*n(ff(-n1)))) 0 ?

(Lfn.(=0n)1(*n(ff(-n1)))) (Lfn.(=0n)1(*n(ff(-n1)))) 0
(=00)1(*0((Lfn.(=0n)1(*n(ff(-n1)))) (Lfn.(=0n)1(*n(ff(-n1)))) (-01)))
1

Hm... What about
(Lfn.ffn) (Lfn.(=0n)1(*n(ff(-n1)))) 1 ?

(Lfn.(=0n)1(*n(ff(-n1)))) (Lfn.(=0n)1(*n(ff(-n1)))) 1
(=01)1(*1((Lfn.(=0n)1(*n(ff(-n1)))) (Lfn.(=0n)1(*n(ff(-n1)))) (-11)))
*1((Lfn.(=0n)1(*n(ff(-n1)))) (Lfn.(=0n)1(*n(ff(-n1)))) (-11))
*1((Lfn.(=0n)1(*n(ff(-n1)))) (Lfn.(=0n)1(*n(ff(-n1)))) 0)
*11
1

(Lfn.(=0n)1(*n(ff(-n1)))) (Lfn.(=0n)1(*n(ff(-n1)))) 2
(=02)1(*2((Lfn.(=0n)1(*n(ff(-n1)))) (Lfn.(=0n)1(*n(ff(-n1)))) (-21)))
*2((Lfn.(=0n)1(*n(ff(-n1)))) (Lfn.(=0n)1(*n(ff(-n1)))) (-21))
*2((Lfn.(=0n)1(*n(ff(-n1)))) (Lfn.(=0n)1(*n(ff(-n1)))) 1)
*2(*11)

Ah, the factorial function, 5! in the case of the orginal example.

----





-----= Posted via Newsfeeds.Com, Uncensored Usenet News =-----
http://www.newsfeeds.com - The #1 Newsgroup Service in the World!
-----==  Over 80,000 Newsgroups - 16 Different Servers! =-----