( Collapse )
Other stuff about yesterday: Dan Licata gave an interesting talk at the ConCert group meeting, about engaging in all sorts of shenanigans at the constructor and kind levels of a lambda-cubist sort of dependent type theory. Went to hot dogs, went through a proof of the Friedberg-Muchnik theorem with tom7, which states that there exist recursively enumerable sets A and B such that A is not turing-reducible to B (i.e. A is not recursive even given an oracle for membership in B) and B is not turing-reducible to A. This is a really weird thing, since it means, at some level, that there are "problems" that are "easier than" the halting problem, yet still undecidable. In fact there is a very powerful theorem due to Sacks that says for any countable partial order P, there is a collection X of R.E. sets such that P is isomorphic to (X, ≤T) where ≤T is the turing-reducibility relation. This means there is no "easiest impossible problem" nor is there any "hardest still-not-turing-complete" problem, and it means you can find countably many different problems none of which help you solve any of the others.
I've made it about of a third of the way through Harold Bloom's "Genius". He kind of
can't keep Shakespeare's dick out of his mouthreveres Shakespeare like a god among men, and spits bile about anyone who made the unfortunate choice of ever badmouthing the Bard, but his enthusiasm for literature and poetry in general is infectious. I'm much more curious about Rilke, Goethe, Kafka, Montaigne, and Emerson now.