Subject: RE: Lambda (was: Refactoring in Tunes) - msg#00037

List: os.tunes

Mail Archive Navigation:
by Date: Prev Next Date Index by Thread: Prev Next Thread Index

Massimo Dentico wrote:
> btanksley@xxxxxxxx wrote:
> >Massimo Dentico wrote:

> > > > btanksley@xxxxxxxx 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

Thread at a glance:

Previous Message by Date:

Re: Lambda (was: Refactoring in Tunes)

btanksley@xxxxxxxx wrote: > > > From: Massimo Dentico [mailto:m.dentico@xxxxxxxx] > > > Massimo Dentico wrote: > > > > btanksley@xxxxxxxx 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

Next Message by Date:

RE: A mathematical foundation of reflexion?

On Mon, 10 Jan 2000 btanksley@xxxxxxxx wrote: > I just wanted to add that > http://www.latrobe.edu.au/www/philosophy/phimvt/j00syn.html introduces not > only a facinating computer language, but uses that language as a notation > for explaining many computer science and mathematics problems in a very > understandable way (including basic category theory). I'm extremely impressed. The thing is well named, it is indeed a Joy. One of the points I was going to make when I joined this group was that reflection is a brilliant idea but it is hopelessly under utilized in the "real" world of programming. Even to the extent that many Scheme implementations seem to bypass macro implementation of features in favour of hard coding the various features that could have been done by scheme macros. As such there must be something "unholy" about the current reflective languages that makes such an obviously tasty feature as reflection so terribly under utilized. The next point of observation I was going to make was that one of the very few languages that its really extensively used as a generated language is Postscript. ie. Most postscript programs are the output of other programs. ie. There is something special about PostScript that bares close inspection for those interested in reflection as a useful daily tool. I think Joy lays bare that special something about Forth and Postscript. The homomorphism between syntatic concatenation and functional composition. If that homomorphism exists, then reasoning about the program becomes very much easier, and if reasoning becomes easier it is much easier to write bug free programs. I haven't enJoy'ed reading a description of a programming language as much as I have read the write up on Joy. I do not think Joy as is a panacea, there are a number of difficiencies in the semantics that make it unusable, but the idea of creating a workable algebra of programs is priceless. John Carter The Cybernetic Entomologist - cyent@xxxxxxxxxx http://www.geocities.com/SoHo/Cafe/5947 "If man realized that the universe, like him, can love and suffer, he would be reconciled." - Camus

Previous Message by Thread:

Re: Lambda (was: Refactoring in Tunes)

Laurent Martelli wrote: > > Massimo> To obtain true portability you need a good virtual machine > Massimo> or a complete metaprogramming environment. Forth has a > Massimo> tiny, quite fast virtual machine that you can easily port > Massimo> *manually* without much effort just in virtue of his size > Massimo> OR you can metacompile it to another target machine > Massimo> (evidence of these facts: the proliferation of Forth > Massimo> implementations). So you can obtain a better compromise > Massimo> between portability and efficiency. > > I'm afraid that the "non-standard library" problem also arise in the > case of VM. But maybe you were thinking of "unportable" libs such > threads. The Forth Virtual Machine is not a VM in traditional sense. The problem of "non-standard library" doesn't arise because to *bootstrap* a Forth environment you don't need library at all. A typical size of a Forth system is few KB and is defined in term of few primitives. You can make this core so little that you can *manually* assemble it and/or port it to another assembly, as I have already pointed up. > Anyway, a complete metaprogramming environment is my goal. Yes, I know and I agree with this choice, of course. > Massimo> Of course, to run OIL on the bare hardware you need to port > Massimo> your interpreter (your virtual machine) to other machines > Massimo> OR to write a compiler for OIL. It's not sufficient to > Massimo> rewrite OIL in OIL. > > Of course. Our plan is to rewrite OIL in OIL, and then write an > OIL2Posix compiler or something like that. We're not interested in > bare hardware (yet). Ok, when you'll interested to reach the bare hardware I suggest you to take a look carefully in this direction. -- Massimo Dentico

Next Message by Thread:

Re: Lambda (was: Refactoring in Tunes)

> Laurent Martelli wrote: > > > > Every one is also free to use OIL :-) (http://perso.cybercable Massimo Dentico wrote: >Another excerpt from "Thoughtful Programming" >- http://www.ultratechnology.com/forth.htm [...] > Chuck wants to make the computer simple and easily comprehended so > that no extra layers of abstraction are needed to get at it or the > problem. Chuck wants to make the solution simple so that it easy > to write and efficient and has no extra layers of unneeded fat. > Chuck seeks a simple efficient abstraction of the actual problem > to the actual computer. The problem I have with this approach is that real-world problems lie in entirely different domains than that of the computer. For example, I'm currently wrapping up a project whose problem statement could have looked like this: "We need a way to store and access information about companies and contacts. We need to be able to create "projects" involving these companies and keep a communication log and to-do lists involving these projects. Furthermore, we need the information to be centralized and accessible over the Internet. And we want to be able to access the data from other people's computers, so it the method of access can't require any special setup other than an Internet connection. Oh, and the solution needs to be easy to use and understand, and reasonably speedy on a Pentium 100. This is a classic "line of business" problem, the kind upon which the vast majority of America's programmers work. (Presumably the same is true for the rest of the world, too.) Computers, on the other hand, do arithmetic, flow control, and bitwise I/O. I don't see any simple abstraction of those concepts to the concepts involved in the problem statement above. > If they could see beyond the illusion to see only the > simple problem and were only faced with mapping it to a simple > computer things stay simple and simple methods work. I don't deny that the computer is simple. It does arithmetic, flow control, and bitwise I/O. But the problems are NOT simple. And that's why abstractions are so crucial. If I had to think about the simple computer's simple manipulation of bytes every time for every single kind of database query I send over the Internet, the proliferation of simple things would grow so huge it would overwhelm me. No, give me abstractions, lots of them, so I can choose the ones that most closely relate to the problem I'm solving. When I want to do arithmetic, then I'll consider giving them up. But my customers don't want to do arithmetic. (They've got calculators for that.) They want to do things that don't relate to the computer at all. Jim