Jason (jcreed) wrote,

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.
Tags: math, recursion theory, social

  • (no subject)

    Something that's bugged me for a long time is this: How many paths, starting at the origin, taking N steps either up, down, left or right, end up at…

  • (no subject)

    Still sad that SAC seems to end up being as complicated as it is. Surely there's some deeper duality between…

  • (no subject)

    I had already been meaning to dig into JaneSt's "Incremental" library, which bills itself as a practical implementation (in ocaml) of the ideas in…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded