8 Nov 2003 raph   » (Master)

How much resolution is enough?

Faithful readers of this blog will have already noted my fascination with high resolution displays. Desktops seem stuck at 100dpi dot matrix quality for the moment, but the portable space is heating up nicely. For one, it looks like the recent release of the Toshiba e805 is a harbinger of the next major rev of the Pocket PC platform. And if 200dpi isn't good enough, Sharp has started showing a prototype of a 300 dpi model.

Just how much resolution is enough? Are pixels going to keep getting smaller, or is there some natural resolution beyond which there isn't a noticeable improvement? I've just submitted the manuscript for my paper on this topic, which I'll present at the EI04 conference in San Jose next January. The quick answer is that, for desktops and laptops, this natural resolution is around 170 dpi, and about 240 for handhelds. Devices within striking range of these targets are available now, but not yet mainstream.

Attacks on the GPL

I'm not sure people realize how seriously the GPL is under attack these days. Yeah, SCO is trash-talking it, but I think this could ultimately be good for us, as they're on the verge of becoming thoroughly discredited, even to the point where shill reporters won't be able to repeat their baloney with a straight face.

I find the official policy of the BSA more disturbing. Of course one expects the BSA to lobby for the benefit of the proprietary software industry, but don't forget that IBM and Novell (the proud new owner of SuSE) are also members in good standing. (Thanks to this Groklaw article for the heads-up)

Take a look at this paragraph in particular:

2. Ensure that government funded research is available to all. Government plays an important role in financing basic software research. When public funds are used to support software research and development, such funding should be made equally available to all developers, regardless of the development model chosen to do the research. The innovations that result from this work should be licensed in ways that take into account both the desirability of building a commons of knowledge and the desirability of applying basic research advances to commercialized products. The dissemination of results broadly in this manner has contributed to a virtuous cycle of innovation in which government funding for basic research advances the set of knowledge available to the public by spurring advances in commercial products. These commercial products in turn generate growth and tax revenue necessary to fund future rounds of public research.

Unless I'm totally misreading it, it's saying that government-funded computer science research projects should not release GPL software, preferring BSD-like licensing if it's going to be released freely. I'm not sure how close this kind of trade-association policy is to becoming the law of the land (not that such things ever happen here in America), but I consider it highly alarming. At the very least, I consider it plausible that this lobbying is having a chilling effect on American government funding of GPL'ed projects. At least other countries seem to be starting to see the light.

Is ZF set theory a hack?

It's hard to believe, but apparently some offhand comments made here have inspired a serious paper comparing various axiomatizations for the foundations of mathematics, primarily in terms of the complexity needed to represent these axioms. Check out "Is ZF a hack?" on Freek Wiedijk's notes page.

I don't think there is a One True Axiomatization for mathematics. In fact, I think the lesson we should take away from Gödel's incompleteness theorems is that, in a very real formal sense, such a thing is impossible.

But, if we can't have that, what can we use? As I've written before, I think the answer is a variant of Postel's Law: be conservative in what axioms you require, but liberal in what axioms you're compatible with.

In that case, you'll use ZFC if you want to prove things about hairy infinite objects, but probably a weaker axiomatization such as Z2 or HOL for most everyday work.

Actually, what I think is needed is a system of polymorphic axioms that express basic concepts such as finite data structures and functions, that can be linked with any of the popular primitive axiom-sets. Finite data structures are fairly straightforward (although I did manage to make an embarrassing typo in the formulation for pair in ZFC - it should be (a + b) * (a + b) + b). Functions are going to be harder. Among other things, I'll need to deal with partiality in some reasonable way. But I think that good engineering solutions are possible.

Such an axiom system wouldn't justify better from a philosophical perspective, but I do think it would be a serious improvement in one practical sense: making formal theorems as portable as possible. I think ordinary mathematicians don't worry about this too much, because it usually goes without saying that ordinary, everyday mathematics can be ported (at least in principle) to any appropriate formal framework, so it isn't actually necessary to do it. Things are different, though, if you're trying to stitch together a world-wide repository of formal proofs.

Paul Krugman

Oh, and berend, if I had to pick an entry for the Krugman Gotcha Contest, it would probably be this piece saying that Microsoft's monopoly is not so dangerous after all. Does it surprise you that I don't agree with everything the man has ever written? And yes, I've also been disappointed at the level of sloppiness in some of his columns, if for no other reason than the ammunition it gives to his detractors.

But I find that he has a lot to say. Even when I don't agree with him, I find that he writes thoughtfully, and in such a way as to provoke thoughtful discussion. I'm not sure I see the point of the more vicious Krugman detractors (of whom Luskin seems to be staking out a leadership role). It seems to me that their central point is that we should disagree with everything that Krugman has ever written because he's been wrong a few times. That's one big giant ad hominem attack, and I have little patience for such nonsense.

Latest blog entries     Older blog entries

New Advogato Features

New HTML Parser: The long-awaited libxml2 based HTML parser code is live. It needs further work but already handles most markup better than the original parser.

Keep up with the latest Advogato features by reading the Advogato status blog.

If you're a C programmer with some spare time, take a look at the mod_virgule project page and help us with one of the tasks on the ToDo list!