[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Lambda calculus and it relation to LISP
From: |
William Elliot |
Subject: |
Re: Lambda calculus and it relation to LISP |
Date: |
Tue, 8 Oct 2002 01:42:05 -0700 |
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! =-----
- Re: Lambda calculus and it relation to LISP, (continued)
- Re: Lambda calculus and it relation to LISP, William Elliot, 2002/10/07
- Re: Lambda calculus and it relation to LISP, Barb Knox, 2002/10/07
- Re: Lambda calculus and it relation to LISP, William Elliot, 2002/10/07
- Re: Lambda calculus and it relation to LISP, Christian Lemburg, 2002/10/07
- Re: Lambda calculus and it relation to LISP, ozan s yigit, 2002/10/07
- Re: Lambda calculus and it relation to LISP, Barb Knox, 2002/10/07
- Re: Lambda calculus and it relation to LISP, David Kastrup, 2002/10/07
- Re: Lambda calculus and it relation to LISP, Gareth McCaughan, 2002/10/07
- Re: Lambda calculus and it relation to LISP, William Elliot, 2002/10/07
- Re: Lambda calculus and it relation to LISP, Gareth McCaughan, 2002/10/07
- Re: Lambda calculus and it relation to LISP,
William Elliot <=
- Re: Lambda calculus and it relation to LISP, Fred Gilham, 2002/10/05
- Re: Lambda calculus and it relation to LISP, Kaz Kylheku, 2002/10/05
- Re: Lambda calculus and it relation to LISP, Thaddeus L Olczyk, 2002/10/06
- Re: Lambda calculus and it relation to LISP, Alfred Einstead, 2002/10/11