Re: Lambda calculus and it relation to LISP

[Gareth.McCaughan@pobox.com (Gareth McCaughan)]

gnuist wrote:

> I read the following quote in a book on emacs and similar
> things in a book on lisp.
> 
> "The lambda calculus is a mathematical formalism 
> having to do with the way functions instantiate
> their arguments. To some extent it is the theoretical
> basis for Lisp and plenty of other computer languages."
> 
> I am interested in a little concrete elaboration
> of this statement by any mathematicians, logicians
> or practitioners/users of lisp and lisp in emacs.

Lambda calculus, as originally designed, is a formalism
for representing computations. A lambda-calculus
expression is either a variable "x", a lambda abstraction
"\x.E" (where "\" is a lambda and E is any lambda-calculus
expression), or an application "E F" where E and F are
expressions. There are three transformations you're
allowed to do, of which the most important is one that
takes (\x.E)F into whatever you get by substituting E
for every (free) occurrence of x in F.

What this means is that "\x.E" sort-of-means "the
function that maps x to E". E might be something
like "x x" (so that \x.(x x) is the function that
takes any argument and applies it to itself), or
something like "\y.x" (so that \x.(\y x) is the
function that takes any argument and returns the
constant function that always returns it), or
whatever.

The point of all this is that that is, in some sense,
*all* you need; within this system you can model all
of mathematics, or at least all the mathematics
Alonzo Church cared about. You have to "encode"
everything as a function. For instance, here's a
famous way of representing the non-negative integers:

    0 "is" \x.(\f.(\y.y))
    1 "is" \x.(\f.(\y.f y))
    2 "is" \x.(\f.(\y.f (f y)))
    3 "is" \x.(\f.(\y.f (f (f y))))
    etc.

So, we represent n by something that takes a function f
and returns a new function that just applies f n times
to its argument. Then addition is

    \m.\n.\f.\y.(m f) ((n f) y)

and multiplication is

    \m.\n.\f.m (n f)

and so on.

It's often claimed that the lambda calculus is the
theoretical basis for Lisp, or Scheme, or other
languages, but the truth behind this claim amounts
to the following things.

1. Those languages treat functions as first-class objects.
2. Some of those languages use the keyword "lambda"
   for building functions.
3. Some of those languages allow functions to carry around
   their "environment", which sort-of corresponds to how
   lambda abstractions behave in the lambda calculus.
   (Note that this was *not* a feature of the very first
   Lisps. It is also not a feature of Emacs Lisp. The
   key words here are "lexical scoping" versus "dynamic
   scoping".)
4. Er, that's it.

Important features of the lambda calculus that aren't
reflected in any version of Lisp that I know:

1. In the lambda calculus, *everything* is a function.
   We don't need no stinkin' numbers!
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, which is basically
   what "lazy languages" like Haskell do. I don't think
   any Lisp variant is lazy.
3. The lambda calculus has no notion of "object identity".
   Indeed, it has no notion of "objects". When I say
   "objects", I don't mean "instances of classes in a
   system with inheritance and polymorphism and
   encapsulation"; I just mean "things we can compute
   with". The lambda calculus is purely syntactic; two
   expressions are "equal" if you can transform one to
   the other by the standard transformations. No notion
   of identity here.
4. Evaluation in the lambda calculus works by repeated
   textual substitution. You can build toy interpreters
   that way (I think it's done in SICP, but I may be
   misremembering), but you can't really build a practical
   programming language on that foundation. Especially
   not an "impure" one (i.e., one with mutable state),
   which includes every variety of Lisp I know of.

It is likely that some Lisp pioneers have been inspired
by the lambda calculus, with its vision of the power of
functions, but calling it the theoretical basis for Lisp
is in my opinion rather misleading.

The most lambda-calculus-y languages are the lazy pure
functional languages. Some of them are even implemented
(I think) in a way that's reminiscent of the lambda
calculus and its "reduction rules" (the things I called
transformations, earlier).

> This is an interdisciplinary topic and cross-posted.
> Please beware of this and be undaunted in intellectual 
> work just in case some rude individual jumps in and threatens
> the discussion on this thread. This comment is in view
> of a sad incident by a similar character on a valid 
> interdisciplinary thread on comp.lang.lisp and gnu.emacs.help.
> Previously this individual had also posted unbecoming
> comments to Professor Fateman of UC Berkeley who is
> actually a very nice and helpful individual in my experience
> about two years ago from a phone conversation with me.

This sort of remark essentially never has a positive effect.
(Meaning the "rude individual" stuff, not the compliment
to Richard Fateman.)

> I think that it would be exciting and intellectually 
> satisfying to know an answer to this question for many
> of us in the math/logic/lisp/emacs community.

Emacs Lisp is less lambda-y than any other version of Lisp
I am familiar with. (I am not familiar with AutoLisp.)

-- 
Gareth McCaughan  Gareth.McCaughan@pobox.com
.sig under construc