From mboxrd@z Thu Jan 1 00:00:00 1970 Path: main.gmane.org!not-for-mail From: William Elliot Newsgroups: gmane.emacs.help Subject: Re: Lambda calculus and it relation to LISP Date: Mon, 7 Oct 2002 02:54:54 -0700 Organization: Newsfeeds.com http://www.newsfeeds.com 80,000+ UNCENSORED Newsgroups. Sender: help-gnu-emacs-admin@gnu.org Message-ID: <20021007025440.K57236-100000@agora.rdrop.com> References: <9e8ebeb2.0210041920.2e480123@posting.google.com> <20021006050255.A63895-100000@agora.rdrop.com> NNTP-Posting-Host: localhost.gmane.org Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Trace: main.gmane.org 1033984590 28184 127.0.0.1 (7 Oct 2002 09:56:30 GMT) X-Complaints-To: usenet@main.gmane.org NNTP-Posting-Date: Mon, 7 Oct 2002 09:56:30 +0000 (UTC) Return-path: Original-Received: from monty-python.gnu.org ([199.232.76.173]) by main.gmane.org with esmtp (Exim 3.35 #1 (Debian)) id 17yUcl-0007K9-00 for ; Mon, 07 Oct 2002 11:56:27 +0200 Original-Received: from localhost ([127.0.0.1] helo=monty-python.gnu.org) by monty-python.gnu.org with esmtp (Exim 4.10) id 17yUcT-0007rB-00; Mon, 07 Oct 2002 05:56:09 -0400 Original-Newsgroups: gnu.emacs.help,comp.lang.lisp,sci.math,sci.logic X-X-Sender: In-Reply-To: Original-NNTP-Posting-Host: 199.26.172.34 Original-X-Trace: corp.newsgroups.com 1033983420 199.26.172.34 (7 Oct 2002 04:37:00 -0500) Original-Lines: 75 X-Comments: This message was posted through Newsfeeds.com X-Comments2: IMPORTANT: Newsfeeds.com does not condone, nor support, spam or any illegal or copyrighted postings. X-Comments3: IMPORTANT: Under NO circumstances will postings containing illegal or copyrighted material through this service be tolerated!! X-Report: Please report illegal or inappropriate use to X-Abuse-Info: Please be sure to forward a copy of ALL headers, INCLUDING the body (DO NOT SEND ATTACHMENTS) Original-Path: shelby.stanford.edu!newsfeed.stanford.edu!news-spur1.maxwell.syr.edu!news.maxwell.syr.edu!l-out.nntp.be!corp.newsgroups.com!agora.rdrop.com!mars Original-Xref: shelby.stanford.edu gnu.emacs.help:105777 comp.lang.lisp:95841 sci.math:550050 sci.logic:61647 Original-To: help-gnu-emacs@gnu.org Errors-To: help-gnu-emacs-admin@gnu.org X-BeenThere: help-gnu-emacs@gnu.org X-Mailman-Version: 2.0.11 Precedence: bulk List-Help: List-Post: List-Subscribe: , List-Id: Users list for the GNU Emacs text editor List-Unsubscribe: , List-Archive: Xref: main.gmane.org gmane.emacs.help:2323 X-Report-Spam: http://spam.gmane.org/gmane.emacs.help:2323 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! =-----