help-gnu-emacs
[Top][All Lists]

## Re: Lambda calculus and it relation to LISP

 From: William Elliot Subject: Re: Lambda calculus and it relation to LISP Date: Sun, 6 Oct 2002 05:03:09 -0700

```Gareth.McCaughan@pobox.com
Using L for lambda and convention (Lxy.M) for (Lx.(Ly.M))
and = for transform or converts to.

wwf:  variables
wwf N,M ==> wwf (Lx.N), (NM)

_ 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?

_ 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.

0 = (Lfx.x)
1 = (Lfx.fx)
2 = (Lfx.f(fx))
3 = (Lfx.f(f(fx)))
...
0f = I                          0fx = x
1f = (Lx.fx)            1fx = fx
2f = (Lx.f(f(x))        2fx = f(f(x))
3f = (Lx.f(f(f(x)))     3fx = f(f(f(x)))
...

_ So, we represent n by something that takes a function f
_ and returns a new function that just applies f n times
_ to its argument. Then addition is
_     Lm.Ln.Lf.Ly.(m f) ((n f) y)
Ok.  By my definition for 1.
+11 = Lf.Ly.(1f)(1fy) = Lf.Ly.f(f(y)) = 2

+11 = Lf.Ly.(1f)(1fy) = something complicated

_ and multiplication is
_     Lm.Ln.Lf.m (n f)
Ok

Lnfx.nf(fx) successor function.
Lmn.nm exponetation m^n

_ 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?

_ 3. The lambda calculus is purely syntactic; two
_    expressions are "equal" if you can transform one to
_    the other by the standard transformations.
_ 4. Evaluation in the lambda calculus works by repeated textual
_ substitution.

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 ?
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!

----

-----= 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! =-----

```