Lambda (was: Refactoring in Tunes)

[btanksley@hifn.com]

Massimo Dentico wrote:
> btanksley@hifn.com wrote:
> >Massimo Dentico wrote:

> > > > btanksley@hifn.com wrote:
> > > > > for a study of computation theory completely without
> > > > > lambda calculus.

> > 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.

Hmm.  I agree that the lambda keyword is used in programming languages to
avoid that, yes.  The usual meaning of the word "notation" is a mathematical
device, which has to include the theory.  Lambda theory is about modelling
function calls via variable substitution (okay, that's an
oversimplification, but that's the basic idea).

> > 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.

This is true -- and it's mainly true because we haven't had many other
methods.  Note, however, than Abstract State Machines have long been a very
powerful model of program execution.  Of course, ASMs can't replace lambda
calculus for reasoning about most compilers, because most compilers are
designed around lambda calculus.

> > > 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 ...

Directly inferior to combinator theory, arrow theory, and a few others.
When I say "directly inferior", I mean that both of those models can express
a strict superset of computation operations, almost always with more ease.
In the few cases where the computation operations are easier in
lambda-calculus than they are in the other systems, the operation isn't a
computation, but rather a syntactic transformation.

Indirectly inferior to abstract state machines -- in the sense that ASMs can
express the same basic operations conveniently and provably, but model the
actual behavior of a computer much better.

Lambda is a very old calculus which was inadequate from the day it was
invented (it can't correctly model ANY function calls, not even Lisp's), yet
simply because it's old all theories are compared to it.

Lambda calculus makes proofs HARD and programming almost impossible --
languages built around it have to either dilute it with other mechanisms
until it's not lambda calculus anymore (as Lisp does), or restrict the
language strongly until it's useless for any practical purposes.

> > treated as though it were the whole of computer science

> I have never asserted this.

True.  I apologise for implying otherwise.

I was complaining more about other people, some of them on this list, who
have committed just this sin ;-).

> 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).

I enjoyed Baker's paper -- I'd be amused to build an experimental
generational garbage collector for Joy which used linear logic at its lowest
generation.  (In other words, an operation in Joy would either be
"linear-safe" or "linear-unsafe"; an unsafe operation would be responsible
for moving its arguments into the GC pool, while safe ones would simply
allocate and deallocate as needed.)

> > 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).

True.  Chuck gave us the practice without the theory; others (including
Baker) have established the theory; and now Joy has reconnected the theory
with the practice, and showed that the result echoes throughout the rest of
computer science.

> > > 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 ...

I would be very happy to work on such a project (although in C or Joy rather
than in assembler).  Before I even start thinking about that, though, I
would like to study Joy a while more -- I'm very familiar with Forth, and
there are a lot of Forth conventions which Joy ignores.  I would like to
investigate which ones would improve Joy and which ones would be bad for it.
I'd also like to think about designing a new Forth based on the ideas Joy
has revealed -- but like Forth, it would have no GC (and so a number of cool
things from Joy would not survive the transition).

> As usual, sorry for my horrible english.

Your English is quite impressive -- I am not a quarter as expressive in any
foreign tongue (currently only Latin and ancient Greek).

> Massimo Dentico

-Billy