Today is election day...

...so maybe I can post about a couple unusual things today. First: go vote! If you live in Pennsylvania, are eligible to vote, are registered with a political party, and haven't voted already. (Not sure what segment of my huge readership that applies to.) Yesterday I heard Barack Obama speak at the Petersen Events Center. The content of the speech wasn't all that exciting (since it's all been said before), but I was very impressed by the fact that he made the effort for a last-minute, late-night stop in Pittsburgh. You could see on his face just how tired he was, but also that he knew the stakes, and was determined to keep standing up. It somewhat reminded me of kibadachi practice.

Second: over the weekend I met an old friend from college, Ben Schmidt, who now studies American history at Princeton. Later I was looking at his website, and saw that he has a very interesting paper about using a variation of Google's PageRank algorithm to rank PhD programs:

Ranking Doctoral Programs by Placement: A New Method
Benjamin M. Schmidt and Matthew M. Chingos
Forthcoming in PS: Political Science & Politics

Most existing rankings of graduate programs rely on some measure of faculty quality, whether it be reputation (as in the National Research Council and US News rankings), honors (prizes, membership in learned societies, etc.), or research quality and quantity (as in citation studies and publication counts). We propose a ranking that focuses instead on the success of a program’s graduates. By using stochastic matrices, it is possible to create a system in which programs essentially “vote” for each other by hiring graduates of other programs as professors in their own department. This system allows us to create an objective, results-oriented measure that is well suited to measure the quality of departments whose graduates aspire to academic positions. The rankings correlate well with reputational ranking systems, and include a per capita measure that recognizes the accomplishments of smaller but high quality programs.

a paper

Focusing on binding and computation
Dan Licata, Noam Zeilberger, and Robert Harper
To appear at LICS 08

Variable binding is a prevalent feature of the syntax and proof theory of many logical systems. In this paper, we define a programming language that provides intrinsic support for both representing and computing with binding. This language is extracted as the Curry-Howard interpretation of a focused sequent calculus with two kinds of implication, of opposite polarity. The representational arrow extends systems of definitional reflection with a notion of scoped inference rules, which are used to represent binding. On the other hand, the usual computational arrow classifies recursive functions defined by pattern-matching. Unlike many previous approaches, both kinds of implication are connectives in a single logic, which serves as a rich logical framework capable of representing inference rules that mix binding and computation.

Comments appreciated!

just wait a second...

An article of faith is that the undecidability of the halting problem makes it impossible to restrict to terminating programs and still have a general-purpose programming language. On the other hand, another article of faith is that we'd be in big trouble if we allowed non-terminating proofs in mathematics (e.g., "Trust me, I have a proof of the Riemann Hypothesis, just wait a second..."). Why the double standard? Do we shackle ourselves by using a fragment of mathematics that disallows (we hope) non-terminating proofs? Or have we been too hasty to accept non-terminating programs? The latter stance is embraced in total functional programming. But I think the former is also not super crazy. With a more interactive notion of proof, potential non-termination would not be so dangerous.

Z: "I have a proof of the Riemann Hypothesis, can you add it to the Book?"

E: "Of course, but first can you tell me how you handle this tricky case?"

E presents tricky case to Z

Z: "Sure, no problem, this case is easily handled by, um, some math, er, ..."

Z stalls

E waits patiently, but keeps the Book firmly shut

In some sense, terminating proofs are just a time-saving mechanism for referees. It would indeed be a shame if Z wasted all of E's time with this pseudoproof of RH. On the other hand, E could be doing other things at the same time, such as drinking coffee, or running SETI@Home.