Re: Lambda calculus and it relation to LISP

[William Elliot <mars@xx.com>]

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