Lambda (was: Refactoring in Tunes)
Massimo Dentico
m.dentico@teseo.it
Tue, 11 Jan 2000 20:30:43 +0100
btanksley@hifn.com wrote:
>
> > 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.
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"
is beta-reduction.
> 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.
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
> notation
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
Chuck Moore).
> > 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 ...
> -Billy
As usual, sorry for my horrible english.
Best regards,
--
Massimo Dentico