From mboxrd@z Thu Jan 1 00:00:00 1970 Path: main.gmane.org!not-for-mail From: Gareth.McCaughan@pobox.com (Gareth McCaughan) Newsgroups: gmane.emacs.help Subject: Re: Lambda calculus and it relation to LISP Date: Mon, 7 Oct 2002 23:48:01 +0100 Organization: International Pedant Conspiracy Sender: help-gnu-emacs-admin@gnu.org Message-ID: References: <9e8ebeb2.0210041920.2e480123@posting.google.com> <20021006050255.A63895-100000@agora.rdrop.com> <20021007025440.K57236-100000@agora.rdrop.com> Reply-To: Gareth.McCaughan@pobox.com NNTP-Posting-Host: localhost.gmane.org X-Trace: main.gmane.org 1034031583 1512 127.0.0.1 (7 Oct 2002 22:59:43 GMT) X-Complaints-To: usenet@main.gmane.org NNTP-Posting-Date: Mon, 7 Oct 2002 22:59:43 +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 17ygqh-0000O2-00 for ; Tue, 08 Oct 2002 00:59:39 +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 17ygne-0003gY-00; Mon, 07 Oct 2002 18:56:30 -0400 Original-Path: shelby.stanford.edu!newsfeed.stanford.edu!news.tele.dk!small.news.tele.dk!195.25.12.36!oleane.net!oleane!freenix!proxad.net!proxad.net!newspeer1-gui.server.ntli.net!ntli.net!newsfep1-win.server.ntli.net.POSTED!53ab2750!not-for-mail Original-Newsgroups: gnu.emacs.help,comp.lang.lisp,sci.math,sci.logic User-Agent: slrn/0.9.6.3 (FreeBSD) Original-Lines: 118 Original-NNTP-Posting-Host: 62.253.132.109 Original-X-Complaints-To: abuse@ntlworld.com Original-X-Trace: newsfep1-win.server.ntli.net 1034031203 62.253.132.109 (Mon, 07 Oct 2002 23:53:23 BST) Original-NNTP-Posting-Date: Mon, 07 Oct 2002 23:53:23 BST Original-Xref: shelby.stanford.edu gnu.emacs.help:105804 comp.lang.lisp:95920 sci.math:550229 sci.logic:61696 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:2351 X-Report-Spam: http://spam.gmane.org/gmane.emacs.help:2351 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". When I say "lambda calculus", I do not necessarily mean "exactly what Church wrote about, with no consideration of anything developed later". > > _ 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? > > 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. > > 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. The obvious conclusion, when someone alternates between saying "that's obviously wrong, you mean X" and "what does Y mean?" (with Y usually being something rather elementary) is that the latter question is not sincere, but is intended to be a lightly veiled disagreement, a suggestion that Y is really nonsense, or an attempt to make the reader reconsider. Maybe I should be more explicit: 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. (I happen to find being addressed in this way rather disagreeable, but that's not your problem. :-)) > 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 have no idea whether Church defined subtraction, 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 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 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. > > 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. > _ (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.) -- Gareth McCaughan Gareth.McCaughan@pobox.com .sig under construc