Lambda the Ultimate

Carl Hewitt is speaking tomorrow at Stanford's CSLI CogLunch on the history of logic programming.

A paper is here, so LtU readers can offer their perspectives on the argument.

[Chicken-users] macro systems and chicken (long), Alex Shinn, Apr 2008.

There seems to be a lot of confusion in the Chicken
community, and the Lisp community in general, about the
different macro systems, so I thought provide some
background information and discussion of the eggs available
in Chicken and their uses.

A very nice post that provides a historical overview and implementations of a hygienic (swap! a b) macro in different macro systems: syntactic closures, reverse syntactic closures, explicit renaming, syntax-case, and syntax-rules.

I didn't know syntactic closures before, and find their interface and implementation simple and easy to understand. Any reasons why they aren't used more in Scheme?

Back in 2003, Martin Berger conducted a fairly lengthy interview with Robin Milner. The transcript includes some interesting tidbits on the development of ML, CCS, and the pi-calculus. Among other things, you'll find a recounting of how Milner and David Park came up with the idea of bisimulation, a discussion of the rationale behind some of the design decisions Milner and his colleagues made in creating the pi-calculus, and Milner's thoughts on how theory should influence programming languages:

I do care that languages should be informed by theories...I actually think the best way forward for us now is to look at concurrent calculi as modelling theories for modelling interactions, whether they occur in programs or in outside programs...Languages should emerge from that. They should be treated as a part of a modelling theory. Up to now I don't think we had sufficient incentive to make sure that our languages are close to scientific models. It's only with the onset of computation as a global phenomenon that modelling those interactions becomes so scientifically important that it is bound to have its effect on programming languages.

From the introduction:

Seen in outline, the history of LC and CL splits into three main periods: first, several years of intensive and very fruitful study in the 1920s and ’30s; next, a middle period of nearly 30 years of relative quiet; then in the late 1960s an upsurge of activity stimulated by developments in higher-order function theory, by connections with programming languages, and by new technical discoveries. The fruits of the first period included the first-ever proof that predicate logic is undecidable. The results of the second attracted very little non-specialist interest, but included completeness, cut-elimination and standardization theorems (for example) that found many uses later. The achievements of the third, from the 1960s onward, included constructions and analyses of models, development of polymorphic type systems, deep analyses of the reduction process, and many others probably well known to the reader. The high level of activity of this period continues today.

Beware: This is a long paper (but less than you might expect it to be by looking at the page count: about half the pages are dedicated to the bibliography).

In the announcement on the TYPES Forum the authors invited comments, suggestions and additional information on the topics of the paper, namely the development of lambda-calculi and combinatory logic from the prehistory (Frege, Peano and Russell) to the end of 20th century.

Paul McJones alerts us that the ACM posted PDF versions of some books in its Classic Books Series, which are available to anyone who creates a free ACM Web Account.

Among the currently available books, LtU readers are likely to be particularly interested in Hoare and Jones's Essays in computing science, Adele Goldberg and David Robson's Smalltalk-80: the language and its implementation, and Dahl, Dijkstra, and Hoare's Structured programming.

Long time readers will also know that I highly recommend Papert's Mindstorms: children, computers, and powerful ideas to anyone interested with the effect computers might have on education. Papert's Logo remains to this day the best children oriented programming language, but even if you disagree with me about this, his book is a must read.

Lemonodor has the story, and the links, starting with Dan Weinreb's blog post. Yes, Dan Weinreb has a blog, so if you weren't paying attention, now is the time to check it out!

For me, the take home message is from Paul Graham: If the Lisp machines were so gratuitously, baroquely complex, I should really find the time to learn more about them...

Happy new year, everyone!

A short audio presentation (Avi speaks for less than ten minutes, I guess), about the lessons the Ruby community should learn from Smalltalk. It's mainly about turtles-all-the-way-down, but Self (fast VMs), GemStone (transactional distributed persistence), Seaside (web frameworks) are also mentioned briefly.

Davide Sangiorgi, On the origins of Bisimulation, Coinduction, and Fixed Points.

The origins of bisimulation and bisimilarity are examined, in the three fields where they have been independently discovered: Computer Science, Philosophical Logic (precisely, Modal Logic), Set Theory.

Bisimulation and bisimilarity are coinductive notions, and as such are intimately related to fixed points, in particular greatest fixed points. Therefore also the appearance of coinduction and fixed points are discussed, though in this case only within Computer Science. The paper ends with some historical remarks on the main fixed-point theorems (such as Knaster-Tarski) that underpin the fixed-point theory presented.

There is a wealth of interesting information in this paper. Alas, it is not very easy to read, and the exposition can be improved. So this is not for beginners or outsiders, but if you are familiar with the topic the historical discussion will be of interest.

Solomon Feferman. Gödel, Nagel, minds and machines. Ernest Nagel Lecture, Columbia University, Sept. 27, 2007.

Just fifty years ago, Ernest Nagel and Kurt Goedel became involved in a serious imbroglio about the possible inclusion of Goedel’s original work on incompleteness in the book, Goedel’s Proof, then being written by Nagel with James R. Newman. What led to the conflict were some unprecedented demands that Goedel made over the use of his material and his involvement in the contents of the book - demands that resulted in an explosive reaction on Nagel’s part. In the end the proposal came to naught. But the story is of interest because of what was basically at issue, namely their provocative related but contrasting views on the possible significance of Goedel’s theorems for minds vs. machines in the development of mathematics.

This is not directly PLT related, and more philosophical than what we usually discuss on LtU, but I think it will be of interest to some members of the community.

While the historical details are interesting, I am not sure I agree with the analysis. It would be interesting to here what others make of this.

To make this item slightly more relevant to LtU, let me point out that both the LC and category theory are mentioned (although they are really discussed only in the references).

R6RS has been ratified, with approximately 2/3rds of voters in favour.