Lambda (was: Refactoring in Tunes)

[Massimo Dentico]

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