Re: Lambda calculus and it relation to LISP

[Gareth McCaughan]

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