[Top][All Lists]

[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/ (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

  if ::= \

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
.sig under construc

reply via email to

[Prev in Thread] Current Thread [Next in Thread]