free variable

Almost a year ago, I posted a short note about how to set Polytonic Greek in the LaTeX typesetting system, inspired by my difficulties in typesetting a chapter epigraph for my dissertation, and included with it a challenge to my readers: namely, say something clever about the (unattributed) quote I had included as an example:

οὐ γὰρ μήποτε τοῦτο δαμῇ εἶναι μὴ ἐόντα·
ἀλλὰ σὺ τῆσδ’ ἀφ’ ὁδοῦ διζήσιός εἶργε νόημα

Today, someone did. Congratulations are due to D Jagannathan, who had something clever to say both about the quote itself — which is from the work of the presocratic philosopher Parmenides of Elea — and about the perils of using LaTeX to set texts in non-Latin alphabets. Fine work!

One (imperfect) way to render the quote into English, given by John Burnet in 1892, is “For this shall never be proved, that the things that are not are; and do thou restrain thy thought from this way of inquiry.” Parmenides is either my favorite or second-favorite presocratic, and I like this quote for two reasons: first, it is remarkably Tractarian for something written around two-and-a-half millennia before Wittgenstein destroyed positivism; second, it could be read to describe logic programming or mechanical proof search.

While I was unable to resist one of the basest impulses of computer scientists (viz., quoting philosophers in an effort to distance oneself from the fact that one is essentially in an engineering discipline; see also here), this quote at least was plausibly connected to the chapter it headed. I was, however, able to resist the temptation to include this quote in its original language in the final version of my dissertation. (Indeed, the only moment of weakness I had with regard to non-English languages was in the dedication, where it seems a little indulgence is justifiable.)

One of the perils of computing is this: one encounters a problem that has some unappealing solutions (or partial solutions) and one or more obvious workarounds. Nevertheless, one is compelled to think about the possibility of an elegant, general solution to a class of similar problems. That happened to me this morning, and I wrote it up at Chapeau.

I enjoyed this comment by Marc Hamann in a discussion of MIT’s switch away from SICP for undergraduate computer science education; the whole comment is thought-provoking, but this excerpt is especially delightful:

Somewhat more facetiously, I have to suggest that maybe they are just being merciful to their students, since it seems that many people, seduced by the excitement of SICP, go on to suffer miserably in their career as API and framework plumbers, wishing that being a programmer was actually the elegant and rational process that Abelson and Sussman had made it out to be.

SICP, if read carefully and properly, presents almost an entire undergraduate computer science curriculum in a semester. It’s a shame that MIT EECS students won’t be drinking from that firehose any more. Furthermore, I have long believed that Scheme is unbeatable as a language for teaching computer scientists rather than programmers. (Although “unbeatable” implies a partial ordering: I’d guess it’s possible to argue that Haskell or an ML-family language is equally suitable.)

I was glad to see Ulf Wiger’s slides and talk from his DAMP 2009 tutorial on Erlang programming for multicore processors. I would have been very interested in attending DAMP, but it conflicted with the last day of VMCAI (and thus with my paper), so I wasn’t able to go in person.

Just in case you’re interested, I’ve posted a “web version” of my dissertation. (This version is different from what one might get on microfilm from UMI: the formatting is somewhat nicer, it is single-spaced, and it is designed to be printed two-sided.)

It seems impossible that I haven’t already linked to Jean-Yves Girard’s pseudonymous masterwork “Mustard Watches: An Integrated Approach to Time and Food,” but it looks like I haven’t. Enjoy.

I just won a months-old argument with a colleague. (I had, in fact forgotten that the argument had happened in the first place.) The specific term at the center of the argument and the identity of the colleague aren’t important, but the concession, which took the following form, was downright awesome: “We disagreed about the meaning of term X, but I have decided you are right because Patrick Cousot defined it the same way in his talk.”

Now that’s vindication.

Unfortunately, these videos of talks about the LLVM compiler infrastructure and virtual machine were released at precisely the moment when I have the least amount of free time in recent memory. (But you might be able to enjoy them now).

Ack

I recommend to everyone — but especially to my friends finishing dissertations, and doubly especially to those in Computer Science — Olin Shivers’ amazing acknowledgments section from the scsh manual, which I first encountered as a young Scheme nerd a long time ago. (Philip Greenspun’s gloss on Prof. Shivers’ acknowledgments is pretty delightful as well; scroll ahead to the second block quotation and prepare to be amazed.)

Irrationality

Speaking of acknowledgments, I make brief and jocular reference to the “preface paradox” in the draft preface of my dissertation. This is one of my favorite paradoxes (originally due to David C. Makinson). The basic idea is that a writer believes every individual claim in a manuscript is true (or else he or she would not have committed them to paper); however, some writers claim that their work inevitably will be found to contain some errors. As a consequence, writers are in the curious position of believing the conjunction of every claim in a book and believing the negation of the conjunction of every claim in a book. Whether or not this is irrational is — I guess — an open question with a few plausible solutions.

I’m not sure if these one-star Amazon customer reviews for The Little Schemer are amusing or just depressing, but I am sure that each reveals more about the reviewer than the reviewed.

Here’s a shout-out to the Sable group at McGill. They’ve just released a new version of the Soot compiler framework, which I’ve used extensively in my dissertation work. If you need to analyze or transform Java source or bytecode, I can’t recommend it highly enough.

Benjamin Pierce developed a graduate PL theory course based on TAPL. This isn’t that surprising, since TAPL is an excellent text and I suspect Pierce knows it rather well. The exciting part is that he taught the course with Coq, which is a pretty cool development. His report on the experience, “Using a Proof Assistant to Teach Programming Language Foundations, or Lambda, the Ultimate TA,” looks worth reading.

I like the general idea: interactive development in a proof assistant does for novice proof-writers what interactive development in a conventional programming language does for novice programmers. I also recall being a frustrated undergrad in my first class with a proof component precisely because it wasn’t always clear — before one handed in the assignment, that is — what constituted a good proof and what didn’t. However, Pierce rightly points out that teaching students to write formal, machine-checked proofs doesn’t necessarily help them to write informal proofs. (Also, Coq error messages aren’t always helpful feedback — but they’re at least as good as the worst feedback students get from a human on paper proofs.) I’m delighted to see this development, though — I’ve been thinking about the possible didactic benefits of proof assistants since I took non-classical logic early in grad school, and it will be interesting to see how Pierce’s work plays out in the larger CS pedagogy scene.

Rob O’Callahan on rounding:

Unfortunately both [rounding towards zero and rounding away from zero] can get us into all kinds of trouble when we’re rounding values for use in graphics.

There’s a new version of Teyjus, an implementation of λ-Prolog.

Ott looks interesting.

I recently had occasion to visit this Wikipedia article about Alice ML. Alice ML extends Standard ML with a bunch of useful features, like future, typesafe persistence, and so on.

To motivate future, the wikipedia article author presents the recursive Fibonacci function:

fib 0 = 0
   | fib 1 = 1
   | fib n = fib(n-1) + fib(n-2);

The article then states that “[f]or large values of n, fib n will take a long time to compute.” No kidding; it’s exponential with n. However, Alice ML, according to the Wikipedia article, has a solution for this problem — and it’s not the one you learned in CS1. With future, the article informs us, it is possible to spawn a new thread to compute the nth Fibonacci number, thus saving time if the continuation of fib n does not need the result of fib n immediately.

The article neglects to mention that even Standard ML provides a mechanism to dramatically speed this function’s execution: the humble accumulator, whose straightforward application admits an implementation of fib that is linear with n.

Dyna is a declarative language for writing weighted dynamic programs. It compiles supplied rules into C++ classes — here’s an example of Dijkstra’s algorithm. Although it seems to be targeted to natural-language processing, I can think of several applications in artificial language processing as well.

(If you really want to nerd out with the declarative programming, please see this implementation of Dijkstra’s algorithm in the interactive fiction language Inform.)

Would you believe that Visual Basic for Applications runs in an environment that features dynamic code generation and behind-the-scenes vtable munging of C++ objects? Until I read this article, I wouldn’t have either. To be fair, what reasonable person would assume that a much-maligned macro language would be a playground for so much fun technology? Note that the dynamic compilation is strictly on PPC — the Windows version of the interpreter/VM is “tens of thousands of lines of IA-32 assembly that directly implements all of the opcodes.” Sounds like a threaded interpreter to me (as well as a maintenance nightmare).

[via daringfireball]

whether Java 1.5 annotations are (from a compiler/program transformation perspective) the best thing to be added to Java in a very long time or a hideous addition to the long list of ways in which the Java platform design violates the end-to-end argument. Time will tell, I suppose.

I’m currently listening to Sonata no. 31 in A♭: II Allegro Molto from the album “Beethoven Piano Sonatas Nos 28-32” by Vladimir Ashkenazy

Thanks, Guido.