I'd wondered before why "recursion," a thing defined in terms of its lesser selves, is the word that it is.
I learned today from this NY Times article about handwriting that the root of "cursive" is the Latin currere, "to run."
Recursion, then, is just running again.
So I've been rather busy. The first bit of news is, I submitted a thesis. Warning: it has not been examined and may be full of errors, inaccuracies, omissions, or ill-advised conclusions.
The thesis turned out better than I'd hoped, in the sense that all four major pillars of the work were also accepted to conferences (the papers are "Links: Web Programming without Tiers," "The Essence of Form Abstraction," "A Located Lambda Calculus," and "The Script-writer's Dream: How to Write Great SQL in Your Own Language and Be Sure It Will Succeed").
The night I printed it, I was elated, walking to the printer to collect my final copy, knowing I had done it—created some programming language features, written a 180-page thesis, persevered. In a couple of months I'll defend it, warts and all, and then perhaps I'll be completely finished. But it's downhill from here. I think.
Update: The final version has now been submitted, and the above link points to the latest version.
Had a good time today puzzling over Gerhard Gentzen's 1934 paper, "Untersuchungen über das logische Schließen. I." ("Investigations into logical reasoning"). I wanted to determine that this was really what I thought it was: the paper where he introduced cut-elimination and the subformula property, which I'm examining now in my research.
I was looking at the German version and I don't know anything about German. But Google Translate and the BeoLingus online DE-EN dictionary came to the rescue. (Phil tells me he has a translation, but where's the fun in that?)
The result was satisfying:
Eine nähere Untersuchung der besonderen Eigenschaften des natürlich Kalküls fürte mich schließlich zu einem sehr allgemeinen Satz, den ich im folgenden "Hauptsatz" nennen will. Der Hauptsatz besagt, dass sich jeder rein logische Beweis auf eine bestimmte, übrigens keineswegs eindeutige, Normalform bringen lässt.
which I render,
A closer examination of the special properties of the natural calculus led me to a general theorem that I have called the `fundamental theorem'. The fundamental theorem says that any purely logical proof can be brought to a certain (incidentally, non-obvious) normal form.
And much later, after introducing the natural deduction calculi for classical (NK) and intuitionistic logic (NJ), as well as the respective sequent calculi (LJ and LK), we get to this understated result:
Hauptsatz: Jede LJ- bzw. LK-Herleitung läßt sich in eine LJ- bzw. LK-Herleitung mit der gleichen Endsequenz umwandeln, in welcher die als
Schnittbezeichnete Schlußfigur nicht vorkommt.Every LJ- (resp. LK-)derivation can convert to a LJ- (resp., LK-)derivation with the same end sequent, in which the rule called ``snip'' does not appear.
Instead of the usual name "cut," I've merrily translated the German "Schnitt" as "snip," because it pleases me--I like direct, etymological, native translations of this kind. (OED traces the English "snip" to Low German "schnipp," not terribly far off; "cut" has, of course, OE origin.)
(Sadly, I can't remember where I got the PDF of this original. The browsable online version linked above is from Gentzen's own alma mater, Göttingen University.)
(Miscellanea: Fans of typographic history will appreciate the printer's use of letter spacing for emphasis, a practice unknown in English but apparently traditional in German, according to Wikipedia. It could be used roughly wherever we use italics in English.)
I was surprised to find that these classic papers are available online:
It's interesting to read Church's papers to see how he's approaching the project. Initially, he's trying to clarify the notion of a free variable in logic, or rather to chuck it out in favor of a clear discipline for binding variables. Because he's looking at foundational issues in logic, he's at great pains to identify his assumptions.
A minor historical fact: alpha- and beta-conversion are defined in these early Church papers, but not with those names; they're identified as I-conversion and II-conversion (there is a conversion rule III, which looks like the reverse of beta-conversion).