Re: Lambda calculus and it relation to LISP

[Gareth.McCaughan@pobox.com (Gareth McCaughan)]

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