Lambda (was: Refactoring in Tunes)
btanksley@hifn.com
btanksley@hifn.com
Tue, 11 Jan 2000 09:44:42 -0800
> 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