[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: |
Mon, 7 Oct 2002 02:54:54 -0700 |
Gareth.McCaughan@pobox.com
Conventions: L for lambda; xyz for (xy)z; (Lxy.M) for (Lx.(Ly.M))
N(x/M) for N with every free occurrence of x replaced by M
alpha-conversion: Lx.N -> Ly.N(x/y), provided no free occurrence of
x in N falls within the scope of a bound occurrence of y in N.
beta-reduction: (Lx.N)M -> N(x/M), provided no free occurrence of
x in N falls within the scope of a bound variable of N that's
also free in M.
_ 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.
When's an eta-reduction safe? Lx.Nx -> N, provided no free x in N ?
Was this actually used by Alanzo Church or did he merely mention it?
> _ 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.
What about conversion rules like:
N -> M ==> NK -> MK
N -> M ==> KN -> KM
N -> M ==> Lx.N -> Lx.M ?
_ In particular, if it turns out that you don't need
_ x then you'll never bother reducing any of its bits.
Irreducible wff's are all the same bunch of rascals.
> 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 :-).
Conclusion jumper. Alanzo didn't define a - I know of.
His = was rather complicated as I recall, being effective to
to work just for his numbers. What I know not.
As for 'if', where did that come from? Again just for Church numbers?
> 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).
Doesn't make sense. Are there expressions A,B for which
A(xy) -> x and B(xy) -> y ?
I don't see how 'let' could be a wwf of the L-calculus.
----
-----= 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, (continued)
- 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
- Re: Lambda calculus and it relation to LISP, David Kastrup, 2002/10/07
- Re: Lambda calculus and it relation to LISP, Gareth McCaughan, 2002/10/07
- Re: Lambda calculus and it relation to LISP,
William Elliot <=
- Re: Lambda calculus and it relation to LISP, Gareth McCaughan, 2002/10/07
- Re: Lambda calculus and it relation to LISP, William Elliot, 2002/10/08
Re: Lambda calculus and it relation to LISP, Fred Gilham, 2002/10/05
Re: Lambda calculus and it relation to LISP, Kaz Kylheku, 2002/10/05
Re: Lambda calculus and it relation to LISP, Thaddeus L Olczyk, 2002/10/06
Re: Lambda calculus and it relation to LISP, Alfred Einstead, 2002/10/11