Lambda (was: Refactoring in Tunes)

[btanksley@hifn.com]

> From: Massimo Dentico [mailto:m.dentico@teseo.it]

> Massimo Dentico wrote:

> > btanksley@hifn.com wrote:
> > [...]
> > > the better.  I posted a link to the 'Joy' page a bit 
> > > earlier; take a look
> > > for a study of computation theory completely without 
> > > lambda calculus.

> > A quote from "Overview of the language JOY"
> >         [1 2 3 4]  [dup *]  map
> >                    ^^^^^^^

> > Bill,  this is  a lambda (anonymous function)!  Joy remember me  a
> > little language,  False  (from the same  inventor  of the  Amiga E
> > language, Wouter van Oortmerssen).

I was about to point out to you that anonymous functions have nothing to do
with lambda calculus, when you said:

> The abstract of "An informal tutorial on Joy"

> "composition  of functions.  It does not use  lambda-abstraction of
> expressions  but instead it uses quotation of expressions. A large"

> So, you are right Bill.  I have used the *informal* limited notion
> of lambda as anonymous function,  but technically speaking this is
> a partial point of view.

Right.  However, it's not even a partial point of view -- lambda calculus
don't care whether its functions are named or unnamed.  The important thing
in lambda calculus is the lambda expansion and beta reduction: these are
essentially tools to define new named constants with local scope.

In other words, the lambda calculus is all about _names_, nothing more and
nothing less.

In fact, when lambda was originally used to model procedure calls it wasn't
even close to correct; we've had to add all kinds of complications to the
theory to make it even partially usable, and we've even had to invent new
languages.

> However, further simplification compared
> to lambda  calculus  are truly interesting.

Absolutely.  I only protested because I am truly sick of seeing an inferior
notation treated as though it were the whole of computer science -- it's
taken me years to find a counterexample, but I think that I finally have.
Ecce, a notation which achieves shorter proofs of important theorems without
even using names.

> The idea  of a system
> based on combinators (or Forth),  as a bootstrapping system, float
> around the Tunes project from the long time (see LLL subproject).

I know -- I got the idea from them to a good extent.  I've long envisioned a
language like Joy, and at last I can see it.  Suprisingly, it looks exactly
like I'd expected it to look -- but the author's done _such_ a good job of
continuing the work that I'm simply amazed.

> Massimo Dentico

-Billy