Lambda (was: Refactoring in Tunes)
Tue, 11 Jan 2000 20:30:43 +0100
> > From: Massimo Dentico [mailto:firstname.lastname@example.org]
> > Massimo Dentico wrote:
> > > email@example.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.
I have written lambda, in the sense of lamda *notation*,
*not* lamda calculus, this is the limited point of view.
Lamda *notation* is used exactly to avoid naming functions.
> 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.
I know, Bill. I have cited them in the thread about refactoring,
writing that "Extract Method" is lambda-abstraction and "Inline Method"
> 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
mmm .. much research in the field of compiler theory (but not only)
is based on lambda calculus because we need a mathematical base
to reason rigorously about program transformations.
> > However, further simplification compared
> > to lambda calculus are truly interesting.
> Absolutely. I only protested because I am truly sick of seeing an inferior
Inferior to what and *when*? See later ...
> treated as though it were the whole of computer science
I have never asserted this. As a counterexample I want to cite my interest
for the work of Brian Rice (related to Category Theory) and even for combinators
(that I have discovered as an interesting subject through Forth, in the paper
of Henry Baker).
> 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.
This is the normal course of the science, when we find a counterexample
we can object to the theory. So, now I suppose for a moment that Joy show
that combinators are very superior to lamdas from different point of views:
this is a recent discovery (or re-discovery). Up to now combinators have
been seen as an interesting and elegant mathematical tools, but not
*pratical*. *Now* we know that this is not true (not really *now*,
at least from the article of Henry Baker, if not since the old good
> > 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.
.. and what about rewriting (probably only a core of) Joy in assembly
with the usual technique of Forth? A merging with Retro/Forth OS of Tom
Novelli? What about the utility of such project as an infrastructure
for the Tunes project? A tiny, consistent, understandable, fast environment
with strong mathematical basis to experiment new ideas (or old ideas with
new point of views). It's only a very modest proposal ...
As usual, sorry for my horrible english.