[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: |
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.
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! =-----
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 <=
- Re: Lambda calculus and it relation to LISP, Gareth McCaughan, 2002/10/06
- 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