Trackmap.net changelog

Back in 1996 when the web was young I started a website to host my collection of railway track diagrams. It eventually became trackmap.net. It has updated in fits and starts – the last time it did so was in early 2006 – but I still plan to get time to do updates in the future, such as the maps from this summer's Frankfurt trip.

Despite the irregular updates, trackmap.net was probably my main claim to Internet fame, until I wrote xcftools (which, incidentally exists solely because I needed it for producing track maps easier). Up until now, I have updated a static recent changes page whenever I did something – but seriously, nobody is going to look at that very often to see if there's any news, what with the multi-year hiatuses.

But perhaps some readers would find it useful to subscribe to an RSS/Atom feed for updates to trackmap.net and have their feed reader check it quietly for them? That sounds like a plan. So here is what I'll do: Every time I update trackmap.net (or its subsites) in the future, I'll post about it on this very blog, with the label "trackmap.net".

The label search page becomes the new changelog page, and the feed for new updates is here (Atom) or here (RSS). (Note: These feeds will show only posts related to track maps. If you select the Blogger-provided feed link in the navigation bar, you will get my full blog feed where I blather about various other topics at irregular intervals).

Old changes are still at http://dk.trackmap.net/news.

This posting serves to populate the trackmap.dk labels such that the links just given will not be empty.

Java 5.0 type inference is underspecified

Here's a program that will make your brain hurt:

class C<E> { }
class G<X,Y,Z> { }
class P { }
class Q { }

public class Test {
   static void foo(Object o) {
      System.out.print("Object ");
   }
   static <T> void foo(G<? extends T, ? extends T, ? extends T> g) {
      System.out.print("G ");
   }
   static public void main(String[] args) {
      foo(new G<C<? super P>, C<P>, C<Q>>());
      foo(new G<C<? super P>, C<Q>, C<P>>());
      foo(new G<C<P>, C<? super P>, C<Q>>());
      foo(new G<C<Q>, C<? super P>, C<P>>());
      foo(new G<C<P>, C<Q>, C<? super P>>());
      foo(new G<C<Q>, C<P>, C<? super P>>());
      System.out.println();
   }
}

Quick, what does it print? No cheating!

For what it's worth, Sun's reference javac, version 1.5.0₀₇ produces a .class file that prints

G G G G G G 

whereas Eclipse SDK 3.2.1 creates one that prints

Object Object G G Object Object 

Normally this would lead one to point at one of the compilers and shout BUG! – but after several hours of close reading the Java Language Specification I have come to the conclusion that both behaviors adhere to the letter of the specification. In other words, it is entirely up to the whims of the compiler which of the foos gets called in each of the six calls.

This is somewhat remarkable. Sun has otherwise gone to great pains specifying exactly what a Java program is supposed to mean, modulo the a few clearly defined areas where the virtual machine – not the compiler! – is explicitly given discretion. But here is a completely straightforward single-threaded program where (so I assert) the language underspecifies which method is supposed to be called.

Such nondeterminism makes it hard to do static analysis of Java source code. What happens?

Broadly speaking, generics happen. The half of generics that gets all of the press is parameterized types, but the really hairy stuff only begins to happen when we consider parameterized methods, too. The reason for this is the the programmer always needs to write down the type parameter explicitly in order to instantiate a generic type – but the designers of Java's generics decided that explicit type arguments should not be necessary for calling a generic method. It is possible to give type parameters explicitly in the code, but in the common case, the compiler must try to infer appropriate type arguments given the types of the ordinary arguments.

And this is fairly hard. In fact, because subtyping gets into play, it is so hard that the language makes no claim that the compiler can always find appropriate type arguments when you want to call a parameterized method. The language specification itself remarks, in the middle of the 16 pages of extremely technical definition of how the type inference works:

[...] type inference does not affect soundness in any way. If the types inferred are nonsensical, the invocation will yield a type error. The type inference algorithm should be viewed as a heuristic, designed to perfdorm well in practice. If it fails to infer the desired result, explicit type paramneters may be used instead.

Still, however, one would expect the inference to be deterministic such that one would not risk changing the behavior of a program just by recompiling with a new version of the compiler. But perhaps "perfdorm" and "paramneters" is a hint that this section has not received the most thorough of proofreadings before it went to press.

In the example program above, the type inference eventually computes that T should be instantiated to the "least containing invocation" of an unordered set of the three types C<? super P>, C<P>, and C<Q>. I now quote:

[...] lci, the least containing invocation is defined

lci(S) = lci(e₁, ..., e_n) where e_i in S, 1≤i≤n
lci(e₁, ..., e_n) = lci(lci(e₁, e₂), e₃, ..., e_n)
lci(G<X₁, ..., X_n>, G<Y₁, ..., Y_n>) = G<lcta(X₁, Y₁),..., lcta(X_n, Y_n)>

where lcta() is the the least containing type argument function defined (assuming U and V are type expressions) as:

lcta(U, V) = U if U = V, ? extends lub(U, V) otherwise
lcta(U, ? extends V) = ? extends lub(U, V)
lcta(U, ? super V) = ? super glb(U, V)
lcta(? extends U, ? extends V) = ? extends lub(U, V)
lcta(? extends U, ? super V) = U if U = V, ? otherwise
lcta(? super U, ? super V) = ? super glb(U, V)

[The Java Language Specification, third edition, p. 465]. Read the definition of lci carefully. The first line says that we arrange our three types in some unspecified order. The second line says to combine two types at a time using a two-argument version of lci. And the two-argument lci in the third line just distribute lcta over all the type arguments. (We know from earlier in the type inference that all arguments to lci are instances of the same parameterized type).

This would be a nice and standard construction if only lcta (and by extension the two-argument lci) were commutative and associative. It is indeed commutative – it has to be, for the cases given in the definition only make sense if we understand implicitly that we are to take their commutative closure. But it is manifestly not associative. To wit:

(? super P) lcta (P lcta Q) = (? super P) lcta (? extends Object) = ?

whereas

((? super P) lcta P) lcta Q = (? super P) lcta Q = (? super P & Q)

In the former case, the parameterized foo is not applicable to the call with T = C<?>. Therefore, compile-time overload resolution decides on the less specific but viable foo(Object) instead. But when T is C<? super P & Q>, the parameterized call is applicable.

How clever of javac always to choose the evaluation order that reaches the better result! In fact, I suspect it of cheating and using a smarter multi-argument lcta computation for each type-argument position, instead of selecting on a common order of all lci arguments. Extending the example program to test this hypothesis is left an exercise for the reader.

(Also left for the reader is to figure out the exact meaning and properties of ? super P & Q, a possibility not hinted at anywhere in the JLS except for the two occurrences of "? super glb(U,B)" in the definition of lcta).

Does P equal NP? This is not an answer.

A preprint by Sten-Åke Tärnlund, purporting to prove that P≠NP, is making its rounds on the internets. I noticed it through a blog post by Bruce Schneier; he quite sensibly notes that "these sorts of papers make the rounds regularly, and [Schneier's] advice is to not pay attention to any of them."

Still, someone has to try to pick such papers apart, if only to make sure that they are as worthless as statistics suggest. I'll volunteer for this one. (This mini-review was originally intended to be a comment to Schneier's posting, but grew a bit too large for that. Also, I want to use markup that plain-text comments cannot contain).

It is not easy to figure out what the author is getting at, because the paper is pithy to the point of sloppiness. Take, for example:

Definition 8 p(a) for c·|a|^q some c q ∈ N any a ∈ L.

By comparison with other similarly terse definitions, this apparently means

Definition 8. Let p(a) abbreviate c·|a|^q for some c and q in N, and any list a.

But what are the scope of the quantifiers on c and q? Are they constant throughout the paper or can they depend on something? What can they depend on? It makes no sense in context to let them depend on a ... Complexity theory has no lenity for those who fail to be rigorous about order and scope of quantifiers.

Formally, the paper begins to go wrong no later than Definition 13, where T(s,a,u) is defined to mean something that involve the "truth" symbol ⊨ (or |= if your font, like mine, has no native Unicode glyph for this symbol), which is not in the language of B – but in the remainder of the paper T(s,a,u) is treated as if it was a formula of B, and bogosity ensues.

Of course, a formal error does not mean that the idea behind the paper is flawed. But it does not bode well – one would think that an author who is smart enough to solve an open problem as famous and long-standing as this would be more careful. Indeed, a true flaw shows up:

As far as I understand it, the main argument in the paper goes somewhat like this: Assume that you give me a Turing machine that purports to solve SAT (i.e., decide whether a propositional formula is a tautology) in polynomial time. Then I'll try to run a sufficiently large "pigeonhole formula" PF_m through your machine. I already know that this formula is a tautology, but if your machine tells me that in polynomial time, I can extract a short proof of the formula from what the machine does. This contradicts a theorem by Haken which says that proofs (in a certain restricted form) of the pigeonhole formula are always long. Therefore, your machine either does not solve SAT or does not do it in polynomial time.

What first meets the eye here is that the paper appears to redefine SAT. The SAT we all know and love is about propositional formulas (i.e., expressions built from Boolean variables and the Boolean operators not, and, or and so forth). However, PF_m which the paper tries to use the SAT solver on is not propositional. It is defined only informally here, but for it to have any relation to Haken's theorem, it needs to contain non-Boolean variables and equality operators. Those belong to predicate calculus, not propositional logic. However, this is not in itself damning, because satisfiability in the pure first-order theory of equality is easily seen to be in NP. A valid proof that this is outside P would also solve the P=NP question.

Correction (2008-11-09): It turns out that there are indeed purely propositional formalizations of the pigeonhole principle, and the paper must be referring to one of those. I had in mind a formula such as "(a=1 or a=2) and (b=1 or b=2) and (c=1 or c=2) implies a=b or a=c or b=c". What I did not notice (and, in my defence, the paper never writes out an example of its PF_m) was that we can just expand, say, "a=b" to "(a=1 and b=1) or (a=2 and b=2)", in which case we can take things like b=2 as propositional variables.

The true fallacy here, however, is the tacit assumption (partly concealed as Definitions 13 and 14) that if we have a Turing machine that recognizes tautologies, then a short proof that this machine answers yes for a given formula corresponds to a short proof that the formula is indeed a tautology. But this is not necessarily true; it is at least conceivable that there is a fast Turing machine that recognizes tautologies but that we cannot prove that this is what it does. In that case, a trace of the Turing machine's action does not correspond to any proof that the formula is a tautology, much less a short one. And even if the machine provably recognizes tautologies, we cannot necessarily extract a short proof in a particular formalism from a short run of the machine.

There is various additional smoke and mirrors, including the central proposition which is stated thus:

Theorem 1 SAT ∉ P is true in a simply consistent extension B' of theory B.

Does this mean simply that there is some consistent extension of B in which SAT is not in P, or that SAT∉P is true in every consistent extension of B? I cannot tell. In the former case, the proposition says nothing about the standard model for B (i.e. Turing machines modeled with the standard integers, which are not necessarily a model for the extension). In the latter case, why bother speaking about extensions in the first place?

In conclusion, Schneier is right, and this can safely be ignored.