The Apology of Socrates is one of the most famous works of literature from classical Greece. Socrates stands accused of two charges: impiety and corrupting the youth. The arguments of his accusers are lost to history, but the Apology recounts Socrates’s defense against them. Translating literature across languages is always a dicey affair, and crossing millennia makes it all the more fraught. But in the Apology translators face a less obvious problem: stigmatization of terms by their association with certain dialects.

Socrates calls on his dimótis (δημότης) Crito and some others to serve as character witnesses, and this term is a problem for translators. No-one translates it right. They either use a circumlocution like “man of the same district as myself”, something awkward like “fellow-burgher”, or invent the word “demesman” to create a term in English just to translate dimótis into. Well, respectable English, that is. Because English already has a word for dimótis. The problem is no-one in the rarefied high halls of the ivory tower would ever use it because it’s associated with stigmatized dialects and thereby become stigmatized itself.

Crito was Socrates’s homie.

Right now I’m very irate at C++’s STL because its random_shuffle algorithm has a landmine associated with it. I was using it with a vector, which I’ll refer to as v. The call which shuffles v’s contents is random_shuffle(v.begin(), v.end(), rfunc), where rfunc is a function object which, in the case of int-indexable vectors, accepts a single int n and returns a random int in the range [0, n). What’s the obvious way to get a random int in some range? uniform_int_distribution, of course. And boom, there goes the dynamite because uniform_int_distribution(0, n) generates a random int in the range [0, n], not [0, n).

Besides the need to use uniform_int_distribution(0, n-1) being counter-intuitive, some other attributes make this bug frustrating. While random_shuffle requires rfunc’s return value to be in [0, n), it doesn’t check that it is, even when debugging is enabled — instead, it’s our old friend undefined behavior, no compiler diagnostic provided. vector bears some blame too, as it’s happy to silently munge data pointed to by an out-of-range iterator even with debugging enabled, optimization off, warnings enabled — and again, undefined behavior, no compiler diagnostic provided. If 0 is a valid value of a vector element (naturally, for me it was), then the effect of the bug when v.size() is less than v.capacity() is to get a shuffled vector in which one of its elements has been replaced by 0, and the downstream effects of that can easily be too subtle to notice (naturally, for me it was). So, you only get crashes when v.size() == v.capacity() and something in v.data corrupts and gets corrupted by whatever’s just past it in memory — which is a freakin’ rare occurrence!

How do you debug this kind of thing? Since it’s an intermittent bug which any given run of the program is highly unlikely to trigger, turn on core dumps so that when it eventually does occur, you have the dump of the program state available to debug right there. Turn on debugging so you can get the most out of your corefiles. Stick in code which lets you track what you need to track. Here, this shim function is instructive: int f() { int rand_val = uid(rand_eng); return rand_val; }. You need to remove -O to prevent calls to f() from being replaced by calls to uid(rand_eng) and use -O0 to prevent the transient variable rand_val from disappearing. (volatile probably would work also.)

Don’t forget that this is terrible API design, though. We have a library which has a generator of random ints and a consumer of random ints, and their conventions are different enough that the obvious way to combine them is buggy, yet similar enough that they’ll never trigger compiler warnings (much less errors). That’s not a good API choice, that’s a trap for API users! It’s good to have obvious ways to perform the operations API users will want to perform provided they work correctly. Since API design is hard, often you can’t do that. In those cases where you can’t make an obvious use that works, don’t introduce the obvious use in the first place — it’s far worse than having no obvious use at all, because if you make an obvious way to perform an operation, people will perform the operation that way, simply because it’s the obvious way. It should never be wrong. That there are so many ways to perform unsafe operations that are not obvious, not caught by C++ compilers, and not caught at runtime is the thing I dislike most about this programming language. Today I learned one more way to do it, and I should be well beyond that point.

Recently I had a discussion with some friends about the probability that a certain card was among the first n cards dealt from a shuffled deck of m cards. Here I’m going to only cover the specific case of a deck consisting of the 13 spades, and the chance that the ace is one of the first two cards dealt — n=2 and m=13. We came up with four ways to perform this elementary probability calculation.

Combinatorics: There are ₁₂C₁ ways to have the ace and one other spade, without regard to order. There are ₁₃C₂ ways to deal two spades. So the probability is ₁₂C₁/₁₃C₂ = 12/78 = 2/13.

Trickery: The chance the first card isn’t the ace is 12/13. The chance that the second card, dealt from the remaining 12 cards, also isn’t the ace is 11/12. So the chance that neither is the ace is (12/13)⋅(11/12) = 11/13. Thus the chance that one of the first two cards is the ace is 1 − 11/13 = 2/13.

Conditional probability: The chance that the first card is the ace is 1/13 and the chance it isn’t is 12/13. If we represent the event of the first card being the ace as 1 and the event the second card is the ace as 2, then that is P(1) = 1/13 and P(~1) = 12/13. Now, P(2|~1) = 1/12. ∴ P(1 or 2) = P(1) + P(2|~1)⋅P(~1) = 1/13 + (1/12)⋅(12/13) = 1/13 + 1/13 = 2/13.

Unconditional probability: P(1 or 2) = P(1) + P(2) − P(1 and 2) = 1/13 + 1/13 − 0 = 2/13.

They all generalize into dealing n cards out of m, but the one using unconditional probability not only is the simplest, it generalizes the most cleanly. But most of us found it the least satisfying solution. Maybe because it was too simple?

This post dissects a very short yet fascinating and enigmatic proof that can be found in the Logic module of the standard library of the Lean proof verifier:

theorem iff_not_self : ¬(a ↔ ¬a)
  | H => let f h := H.1 h h
         f (H.2 f)

OK, the fact being proved isn’t enigmatic — it’s stating that a proposition’s truth value is never the same as its own negation’s — but the proof thereof sure is. If that looks to you like some incomprehensible formal logic circling to eat its own tail, that’s because it kinda is.

However, it’s written extremely densely, which inhibits comprehension — which is sad, because the way it works is very interesting. It’s quite the rabbit hole, though, so let’s take our trusty spade and start digging. The very first thing we encounter is that Lean implicitly converts the ¬(a ↔ ¬a) into (a ↔ ¬a) → False. This is because Lean uses dependent type theory to represent logical statements and their proofs, so we need to discuss how these kinds of theories are used with formal logic.

(more…)