[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Lambda calculus and it relation to LISP
From: |
Gareth McCaughan |
Subject: |
Re: Lambda calculus and it relation to LISP |
Date: |
Mon, 7 Oct 2002 23:48:01 +0100 |
User-agent: |
slrn/0.9.6.3 (FreeBSD) |
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
- Re: Lambda calculus and it relation to LISP, (continued)
- 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, 2002/10/07
- Re: Lambda calculus and it relation to LISP,
Gareth McCaughan <=
- 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