sold

You can change

    appV fn x = atomically $ readTVar x >>= writeTVar x . fn

to

    appV fn x = atomically $ modifyTVar x fn

The function getValue need not be in IO monad. You can simplify it using fromMaybe in Data.Maybe.

Sometimes you check "head l" and "tail l"; it's more idiomatic to use pattern matching. For example, you can change:

    setCommand handle cmd db = do
        appV (conv k v) db
        hPutStrLn handle $ "OK"
        where k = (head cmd)
              v = (unwords (tail cmd))
    ....
    case (head cmd) of
        ("get") -> getCommand handle (unwords (tail cmd)) db
        ("set") -> setCommand handle (tail cmd) db

to something like this:

    setCommand handle key val db = do
        appV (conv key val) db
        hPutStrLn handle "OK"
    ...
    case cmd of
      "get":key     -> getCommand handle (unwords key) db
      "set":key:val -> setCommand handle key (unwords val) db

Also consider using hlint, it often gives good advice.

EFF

I think you are missing the point.

OP presented a linear time algorithm. You did not. The point of algorithms is solving problems where the input can change - here it's n, the size of the board. Your solution, as stated, works only for a specific n. It's not an algorithm, at least by common definitions.

You could adapt the solution to handle some finite number of possible inputs with:

n_queens_answer = [ ... array of answers...]; for (int i = 0; i < n_queens_answer[n].length; i++) { place_queen(n_queens_answer[n][i]);

This is also missing the point - obviously every finite function can be written with a lookup table. The point of algorithms is solving problems with potentially infinitely many possible inputs. In fact, time complexity terms such as "linear time" usually mean asymptotic complexity, where the time for any finite number of inputs is irrelevant. Every algorithm could be said to take linear time - even constant time - if you limit allowed length of the input! That's not useful. Even though real world computers have limited memory, the asymptotic behavior, theoretically irrelevant to practice, usually agrees with reality.

In the case of n-queens, finding a pattern that solves the problem for arbitrary n does solve the puzzle. That might be disappointing or contradict intuition, but that's how computer science works. We want an asymptotically fast algorithm that outputs a correct answer, it does not matter that the answer is dull.

Dailymail is rather not a reputable source.

It's different. It's like you were listening to one music genre all your life and there's suddenly something new.

If, say, Python was the only language with "for(each)" loops, you'd see many blog posts about that too. After I saw this, the old style of iterating by index feels so antiquated. Haskell gives the same feeling many times. It has unique features when it comes to abstraction and I feel they are the right way to program.

Retype. Somehow I feel more connected to the words when I type them by myself.

I am a non-native speaker. 95% of my contact with English is via a computer.

There's the google effect: I press Ctrl+T, type tr(anslate.google.com) -> enter and type the word to get an instant translation. In the old times I had very restricted access to the Internet. I used a paper dictionary and bothered to write the word down so I won't forget. I can express myself without a dictionary, but often I _know_ there is a better word and instead of attempting to recall it for a minute I can get it within seconds. My skills worsen as this lookup became a habit. It is a muscle reflex, with paper dictionaries I had to decide to spend the time to research.

I should counteract this, but the world is busy and I keep finding other things to do. In the older times, workers were forced to use their muscles. Now they have robots and physical strength became less important. The same thing happens with foreign languages, basic arithmetic etc. On the one hand, I can focus on high-level tasks; on the other, with no low-level practice I am effectively becoming disabled. Simultaneously and bit ironically, I am a programmer and I love when a task can be done without human intervention.

reddit account: http://www.reddit.com/user/AaronSw

Each hat is independently red-blue 50/50.

Indeed, this is the solution. (One can also note that for for the original puzzle of two prisoners, guessing parity reduces to checking whether their hats are the same or different.)

Conversely, they can use a negation of their result. In this case they win given TH and HT and lose given TT and HH.

Here is a bit harder version of the puzzle, with 100 players instead of 2.

100 prisoners are given either a blue or a red hat, at random. Each prisoner is told colors of every hat except their own, and has to make a guess about his hat with absolutely no communication. They win only if they all guess correctly. They can agree on a strategy beforehand. What is the optimal probability of success?

A counterpoint - The Relativity of Wrong, famous essay by Asimov. http://chem.tufts.edu/answersinscience/relativityofwrong.htm

On a higher level, there's Typeclassopedia http://www.haskell.org/haskellwiki/Typeclassopedia.

> For reference: P <= BPP <= NP

No, BPP is not known to be in NP. It is known to be in Sigma_2 and Pi_2.

No. P/poly is uncountable (contains every unary language) and NP, NEXP, R etc. are countable.

A tweet by The Onion:

[In Focus] Google Shuts Down Gmail To Show Its Immense Power http://onion.com/UxyLs8

I don't consider Godel's theorem to be philosophy. Its status is similar to Cantor's theorem stating that reals are uncountable. Surely is inspired by philosophy and has philosophical consequences, but it is a part of mathematics. Trivia: Godel used the Chinese remainder theorem in his proof http://mathoverflow.net/questions/19857/has-decidability-got.... I acknowledge that philosophy can be inspiration for mathematics, but this is rather unsatiating, as very many things can be.

In the meantime, I found a very good defense of philosophy here: http://www.ditext.com/russell/rus15.html

Let's look at this question:

What "truth" has mathematics itself produced from that search which is well-defined, non-trivial, and correct?

Is it a loaded question? I think it isn't, and it has a lot of valid answers. Here are some recent ones: http://en.wikipedia.org/wiki/List_of_unsolved_problems_in_ma.... Why the corresponding question for philosophers should be loaded? Are they exempt from settling things?

You might try a functional language such as Haskell. It allows you to feel denotational semantics (common in mathematics), rather than operational semantics (common in imperative programming).

I'm afraid you are overstating the importance of alphabets. For example, try this: http://nedhardy.com/2012/04/25/learn-korean-in-15-minutes-ye... It's not really hard to learn alphabets.

I feel the traditional notation achieves a good tradeoff between clarity and conciseness. I don't want to write the string "integral(sin(x),0,1,x)" on paper - 22 symbols - traditional notation is much more concise. I hate to write parens in (a+b)/c; traditional fractions are clearer. On the other extreme, think about programming in APL.

Also see http://terrytao.wordpress.com/career-advice/there%E2%80%99s-...

As the post says, he gained access to both decrypted and encrypted version. Then (p XOR k) XOR p = k.

What do you mean by "transfinite proofs"? Let's look at Cantor's proof. It is:

For every set A and function f : A -> P(A) there exists y in P(A) such that for all x, f(x) /= y.

Proof: Define y = {a: a is not in f(a)}. If f(x) = y, then f(x) = {a: a is not in f(a)}, but this implies x is in f(x) <=> x is not in f(x), contradiction.

It does not mention infinity anywhere! It only says that there cannot be a surjection between one set and the other. We could call this situation "transfinite" but this is only a name; under the hood, this is a normal proof of properties of functions, using very natural reasoning rules. That's why I disagreed - there's nothing special in Cantor's proof from a formal viewpoint, possible concerns are of psychological/historical nature, which are not relevant to a machine.

It is true that changing foundations might require rewriting the prover. However, humans also need time to adjust to a new formal system. For example, it takes a lot of effort to get a good grasp of intuitionistic logic. This might be a concern, but ZFC is a very well-grounded common framework for mathematicians, and this is extremely unlikely to change. Perhaps calculus of constructions, as a version of lambda calculus, is closer to computation, and this is why it was chosen in Coq. I'm not sure. Mizar (another theorem-proving environment) is based on an extension of ZFC. [ZFC is untyped - everything is a set, while CoC has a rich type system.]

Small nitpick: It's not like proofs involving unique choice + excluded middle cannot be expressed in Coq; they can, but as the system is inconsistent, they have no value, as everything is provable.

In my opinion CLRS is too verbose and formal, unless you are a complete beginner. I don't know Sedgewick's book. I can recommend Kleinberg/Tardos, Dasgupta/Papadimitriou/Vazirani and Manber's "Introduction to algorithms: a creative approach".

I have to strongly disagree with your first paragraph. Proofs by humans are finite objects, even if they speak about properties of infinite sets. This difference does not make proofs for computers more difficult than for humans. You can encode cardinality theorems easily in interactive theorem provers.

Formally, a proof is a sequence of assertions, where each one is an axiom or follows from previous ones. Humans are better at proofs because they have good and well-developed intuition; it's bit like coding in assembly vs coding in a high level language. The fact that you deal with infinite objects is not relevant.

Finite fields, essential to error-correcting codes, are based on properties of primes. This forms the basics of efficient data transfer, whether Internet, CDs or communication with spacecrafts. The book "Number Theory in Science and Communication" mentions that finite fields were used in verification of the fourth prediction of general relativity. See that book for more examples.

Here's one from http://mathoverflow.net/questions/2556: There is a gamma ray telescope design using mod p quadratic residues to construct a mask. Gamma rays cannot be focused, so this design uses a redundant array of detectors separated from the mask to reconstruct directional information.

Cicidas have a cyclic life spanning a prime number of years. It is supposed that this is because a predator has harder job aligning with the cycle. http://en.wikipedia.org/wiki/Predator_satiation

I believe that the Möbius function is important in advanced physics: http://en.wikipedia.org/wiki/Mobius_function#Physics

There's a legend that generals used the Chinese remainer theorem to count soldiers.

Elementary number theory was a motivating factor and foundation for development of the whole mathematics - algebra, analysis, even logic. Did you know that proving Godel's incompleteness theorem requires using primes? http://mathoverflow.net/questions/19857/has-decidability-got... Transcendence of pi also needs primes. http://mathoverflow.net/questions/21367/proof-that-pi-is-tra.... I did not realize that earlier. Usage of primes is often invisible. Even if there was no cryptography or ECCs, it would be silly to demand practical applications from this subject - it is a foundation for almost everything in mathematics, sometimes rather concealed.

Whether ABC (or a similar conjecture) is proven has practically no cryptographic impact. This is because you can already write and execute algorithms (whose correctness depends on unsolved conjectures) without proving the conjectures. See http://math.stackexchange.com/questions/69540/would-a-proof-...

Direct link to the PDF: http://terrytao.files.wordpress.com/2012/11/blog-book.pdf

Older collections:

1. http://terrytao.wordpress.com/books/whats-new-2007/

2. http://terrytao.wordpress.com/books/poincares-legacies-cours...

3. http://terrytao.wordpress.com/books/an-epsilon-of-room-pages...

4. http://terrytao.wordpress.com/books/compactness-and-contradi...

5. http://terrytao.wordpress.com/books/hilberts-fifth-problem-a...

The downloadable versions are labelled "drafts" but are of very high quality.

see also http://mathlesstraveled.com/2012/10/05/factorization-diagram... and http://mathlesstraveled.com/2012/11/05/more-factorization-di...

Yes, completely safe