Re: Lambda calculus and it relation to LISP

[William Elliot <mars@xx.com>]

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.
What??  Maybe this is add 0, add 1, 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

By your definition Lx.(Lf.(Ly.f y))
	+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! =-----