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: Tue, 8 Oct 2002 01:42:05 -0700 Organization: Newsfeeds.com http://www.newsfeeds.com 80,000+ UNCENSORED Newsgroups. Sender: help-gnu-emacs-admin@gnu.org Message-ID: <20021008014135.R82905-100000@agora.rdrop.com> References: <9e8ebeb2.0210041920.2e480123@posting.google.com> <20021006050255.A63895-100000@agora.rdrop.com> <20021007025440.K57236-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 1034066840 14539 127.0.0.1 (8 Oct 2002 08:47:20 GMT) X-Complaints-To: usenet@main.gmane.org NNTP-Posting-Date: Tue, 8 Oct 2002 08:47:20 +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 17yq1N-0003mF-00 for ; Tue, 08 Oct 2002 10:47:17 +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 17yq0H-0006wf-00; Tue, 08 Oct 2002 04:46: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 1034065448 199.26.172.34 (8 Oct 2002 03:24:08 -0500) Original-Lines: 187 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!cyclone.bc.net!news-out.newsfeeds.com!l2!corp.newsgroups.com!agora.rdrop.com!mars Original-Xref: shelby.stanford.edu gnu.emacs.help:105820 comp.lang.lisp:95964 sci.math:550307 sci.logic:61722 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:2367 X-Report-Spam: http://spam.gmane.org/gmane.emacs.help:2367 Gareth.McCaughan@pobox.com retorted: > William Elliot wrote: > _ 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? _ I am not (nor have I claimed to be) an expert on the _ work of Church, although I do know that his first name _ is spelt "Alonzo". Good to know as I'd like to locate a copy of his original work. _ When I say "lambda calculus", I do not necessarily mean "exactly _ what Church wrote about, with no consideration of anything _ developed later". Briefly looking thru Google, I discovered what's become of his work is nearly unrecognizable. > > _ 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 ? _ What about them? Are they allowed or prevented by the normal order of -> reductions? > > 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) _ I'd just like to mention that it was not I who wrote _ the _-quoted material there. Correct, I was hoping you'd know or others in the thread would notice. > > 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. _ I believe that for each of those questions, you either know a good _ answer or believe with some reason that there is no good answer. Not so. _ (I happen to find being addressed in this way rather _ disagreeable, but that's not your problem. :-)) I too felt poorly addressed by an abrupt uninformative response. > 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? _ I would expect = to be quite complicated. I'd expect so too. I remember something vaguely so. _ I have no idea whether Church defined subtraction, I'm not sure he did. Nor dare I vouch he didn't. _ but it's not especially hard (though you'd want to _ take some care about the domain, if working generally _ with only non-negative integers). (Note that "quite _ complicated" and "not especially hard" are consistent; _ I would expect = and - to be roughly equally hard.) I'd expect the usefulness of the expression would be limited to Church numbers. _ I don't understand what you mean by "just for Church _ numbers?" regarding "if"; it would be "just for Church _ booleans", which IIRC are _ T ::= \xy.x _ F ::= \xy.y That I'm beginning to find out. F by the way is Church numeral 0. _ or perhaps the other way around. Then "if" is almost _ trivial: _ if ::= \xyz.xyz _ but you don't actually need an "if", since the boolean _ itself will do the work for you. So you can translate _ "if C then X else Y" into CXY. Yes, I was thinking that. So if ::= Lxyz.xyz is mostly for ease in reading and understanding expressions. > > 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! _ Note, again, that I didn't write any of that. Your comments have been are helpful. > _ (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. _ I never suggested that "let" is a wff of the lambda _ calculus. I don't think the person who wrote the "let" _ stuff did, either. However, expressions using "let" _ are readily translated into ones using "lambda" instead, _ and neat tricks like Y are expressible in the lambda _ calculus even if they're nicer to read when written _ using "let". (For people used to "let", anyway.) Thanks for confirming that. When it comes to lambda calculi I feel like I'm speaking ye olde King's English. -- _ There *were* no computers, I think, when _ Church started working on the lambda calculus. I read his work in the late fifties and was much enamored by it. As I recall, it was published in the late 1930's _ Hmm, OK. At this point what you're talking about really _ isn't "the lambda calculus"; that was one of the points _ I was making (and William Elliot too, I think). It's just _ a notation for functions that happens to use the word _ "lambda". This isn't a problem, by the way, but it's _ worth being aware of it. Indeed. _ The advantage of making anonymous functions is threefold. Yes, one notation I've seen is (x_i)_i or (x_i)_(i in I). For example (2^n)_n or (2^n)_(n in N); also (2^r)_r or to be exact (2^r)_(r in R) is the function f(x) = 2^x _ 1. As you say, it saves a name which would otherwise _ clutter up some namespace or other. _ 2. It's more compact. _ 3. It lets you define the function where it's being used, _ rather than putting it somewhere else and making the _ reader check back for the definition. -- recursion from afar > ((lambda (g n) (g g n)) > (lambda (f n) (if (= 0 n) 1 (* n (f f (- n 1))))) 5) > So it's ok to understand that by thinking about ((lambda (g n) (g g n)) (lambda (f n) ((= 0 n) 1 (* n (f f (- n 1))))) 5) (Lfn.ffn) (Lfn.(=0n)1(*n(ff(-n1)))) 5 Have I decipher 5 correctly as the number of iterations? Well then, what happens with (my conclusion at end) (Lfn.ffn) (Lfn.(=0n)1(*n(ff(-n1)))) 0 ? (Lfn.(=0n)1(*n(ff(-n1)))) (Lfn.(=0n)1(*n(ff(-n1)))) 0 (=00)1(*0((Lfn.(=0n)1(*n(ff(-n1)))) (Lfn.(=0n)1(*n(ff(-n1)))) (-01))) 1 Hm... What about (Lfn.ffn) (Lfn.(=0n)1(*n(ff(-n1)))) 1 ? (Lfn.(=0n)1(*n(ff(-n1)))) (Lfn.(=0n)1(*n(ff(-n1)))) 1 (=01)1(*1((Lfn.(=0n)1(*n(ff(-n1)))) (Lfn.(=0n)1(*n(ff(-n1)))) (-11))) *1((Lfn.(=0n)1(*n(ff(-n1)))) (Lfn.(=0n)1(*n(ff(-n1)))) (-11)) *1((Lfn.(=0n)1(*n(ff(-n1)))) (Lfn.(=0n)1(*n(ff(-n1)))) 0) *11 1 (Lfn.(=0n)1(*n(ff(-n1)))) (Lfn.(=0n)1(*n(ff(-n1)))) 2 (=02)1(*2((Lfn.(=0n)1(*n(ff(-n1)))) (Lfn.(=0n)1(*n(ff(-n1)))) (-21))) *2((Lfn.(=0n)1(*n(ff(-n1)))) (Lfn.(=0n)1(*n(ff(-n1)))) (-21)) *2((Lfn.(=0n)1(*n(ff(-n1)))) (Lfn.(=0n)1(*n(ff(-n1)))) 1) *2(*11) Ah, the factorial function, 5! in the case of the orginal example. ---- -----= 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! =-----