March 1, 2010

Simply adding lambda won't make your rewrites diverge

I've been working on trying to extend a result from my thesis, having to do with strong normalization of a certain higher-order rewrite system, but its proof is very complicated, so I've been working on simplifying it.

Along the way I found a paper by Mitsuhiro Okada from 1989 which proves strong normalization for the combination of STLC with any first-order term-rewriting system. But this paper is hard to read because it has strange notations and concepts and says things like, "If a part s[*/x1, ..., */xn, */y] of t belongs to the cap then the part s[*/x1, ..., */xn, */y] also belongs to the cap." Say what?

I knew I could prove the same result using the Tait-Girard method (the same basic approach Okada takes) in a more straightforward way—at least to me. So I did, and here it is for future reference: "Simply adding lambda won't make your rewrites diverge."

January 7, 2010

Time-saving proposal to improve the reviewing process

Proposal: As an academic reviewer, you should always vote to publish a paper, without reading it, even if it is a tedious waste of time.

The time-saving benefit of this strategy is subtle to grasp but significant. You see, only the reviewers of a paper "must" read it, while everyone else will discard it if it's boring. By voting to publish, you waste no one else's time—but the time you save is your own. If every reviewer did this, the time saved would allow us all to do far more research!

July 7, 2009

Thesis submitted

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.

May 6, 2009

Bon mot

It is important, and difficult too, to be unsnobbish when passing on a sense of taste.

March 17, 2009

Embarrassingly Oblique

I'm writing a thesis; parts of it are a big mess just now & I spend a lot of time stuck and wondering what to do next.

So today I reached for an Oblique Strategy and got this:

Look closely at the most embarrassing details & amplify them.

So that's what I'm doing tonight: making it messier.

September 12, 2008

Formlets; Idioms, arrows and monads

[UPDATE: The broken link to "The Essence of Form Abstraction" has been fixed. Sorry!]

For the first time in three years of research, I'm really proud of a paper that I worked on with my research group: The Essence of Form Abstraction, by Ezra Cooper, Sam Lindley, Philip Wadler and Jeremy Yallop, to be published in APLAS 2008. The paper shows how you can create compositional HTML forms which package up their data in any desired type. It shows an OCaml implementation but we also use the idea in our web-centric language, Links.

Though this is the first good group work that I've contributed to, the others have been doing some great work. In particular, Jeremy, Sam, and Phil did some nice work characterizing the expressive power of idioms, arrows, and monads. They first defined a metalanguage, like Moggi's monadic metalanguage, which can encompass all three notions, in The Arrow Calculus, by Sam Lindley, Philip Wadler and Jeremy Yallop (unarchived). Then they showed the hierarchy of the three, under which idioms are the loosest interface but therefore their language is the strictest to program with, and monads are the strictest interface, therefore their language is the most free, and arrows can be seen as lying in between. The work is described in Idioms are Oblivious, Arrows are Meticulous, Monads are Promiscuous (ibid.), MSFP 2008.

To summarize this, you can see the arrow calculus as a syntax like the do notation of Haskell:

do y <- f x
   z <- g y x
   return (h x y z)

Now to put the result crudely, monads allow expressions like the above, where the value bound at each step can be used in all future steps (this makes them "promiscuous"). The use of arrows restricts this so that the value bound at each step can be used only at the next step, as in:

do y <- f x
   z <- g y x
   return (j x z)  -- y cannot be used here

You can still use arrow operations to manually pass data forward through each step, but this is a nuisance. Hence Lindley, Wadler and Yallop coined the term "meticulous" to describe arrows.

The idiom laws restrict this further so that each value can be used only in a final return clause (the return clause is "oblivious"):

do y <- f x
   z <- k x        -- y cannot be used here
   return (h x y z)

An astute reader will note that return is not required in do syntax. What happens if there is no return clause? Then you can add one:

do y <- f x
   z <- k x

is equivalent to

do y <- f x
   z <- k y x
   result <- q
   return result

But either way the idiom laws require that q cannot depend on y or z.

This shows that the three notions progressively restrict (and fairly naturally) the ways that you can program with them. But, in a familiar appearance of contravariance, the notions are reverse-ordered in how restrictive they are to create. An idiom, being the most restrictive on its user, is least restrictive to its writer. Thus you can model some computational notions as idioms which you could not model as monads. This fact came in handy in our latest paper, where we used idioms to model form abstraction.

I encourage you all to read about idioms, arrows and monads, as it's turning out to be a very nice theory.

September 1, 2008

Discovery! \qedhere

Just made an exciting discovery! The TeX command \qedhere can be used within an AMS proof environment; it forces the proof-tombstone to go on the present line, whereas it would normally go after the end of the \begin{proof}/\end{proof} block, which often puts it outside an itemize or enumerate environment, looking ugly on a line of its own. Of course, the command properly suppresses the tombstone at the end of the proof environment. Ah comfort, O infinite luxury of macros!