[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Lambda calculus and it relation to LISP
From: |
Gareth McCaughan |
Subject: |
Re: Lambda calculus and it relation to LISP |
Date: |
Sun, 6 Oct 2002 20:22:54 +0100 |
User-agent: |
slrn/0.9.6.3 (FreeBSD) |
William Elliot wrote:
[I said:]
> _ There are three transformations you're allowed to do, of which the
> _ most important is one that takes (Lx.E)F into whatever you get by
> _ substituting E for every (free) occurrence of x in F.
> Provided no free variable of F falls within the scope of a
> bound variable of E. What are the other two transformations?
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.
> _ The point of all this is that that is, in some sense,
> _ *all* you need; within this system you can model all
> _ of mathematics, or at least all the mathematics
> _ Alonzo Church cared about. You have to "encode"
> _ everything as a function. For instance, here's a
> _ famous way of representing the non-negative integers:
> _ 0 "is" Lx.(Lf.(Ly.y))
> _ 1 "is" Lx.(Lf.(Ly.f y))
> _ 2 "is" Lx.(Lf.(Ly.f (f y)))
> _ 3 "is" Lx.(Lf.(Ly.f (f (f y))))
> _ etc.
> What?? Maybe this is add 0, add 1, etc.
Argle. I'm not quite sure what I was thinking when
I wrote those down. No, it's not add-0, add-1, etc;
it's just a mangled version of what I actually meant.
What I actually meant, coincidentally enough, is ...
> 0 = (Lfx.x)
> 1 = (Lfx.fx)
> 2 = (Lfx.f(fx))
> 3 = (Lfx.f(f(fx)))
... what you wrote.
> _ 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. In particular, if it turns out that
you don't need x then you'll never bother reducing
any of its bits.
> 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)
>
> 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 :-).
> 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!
(let ((x y)) E) === ((lambda (x) E) y).
--
Gareth McCaughan Gareth.McCaughan@pobox.com
.sig under construc
- Re: Lambda calculus and it relation to LISP, (continued)
Re: Lambda calculus and it relation to LISP, Charles Matthews, 2002/10/05
Re: Lambda calculus and it relation to LISP, Gareth McCaughan, 2002/10/05
- Re: Lambda calculus and it relation to LISP, William Elliot, 2002/10/06
- Re: Lambda calculus and it relation to LISP,
Gareth McCaughan <=
- Re: Lambda calculus and it relation to LISP, gnuist, 2002/10/07
- 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, David Kastrup, 2002/10/07
- 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