On the Boolean type

(This is a reprint of a 2003 article, with corrections)

Poring over the code of an open-source program, I felt uneasy upon stumbling over this fragment:

inline bool
Tuner::FftCalc::isPeak(int i, double *buf) throw()
{
    if (buf[i] > buf[i - 1] && buf[i] > buf[i + 1])
        return true;
    return false;
}

I do not think it is pertinent to denounce the author: when in doubt, abstain; I will only reflect on the why and not on the who, nor on issues of programmer quality in open-source projects.

C++ is one of the languages in the Algol genus. As such, it shares with its relatives the delineating trait of having block-structured syntactic (otherwise called static) scope: variables declared local to a scope don't survive its ending. This is the main characteristic that defines block-structured, or Algol-like languages.

There is another characteristic inherited from Algol by these languages, one designed into it purposefully and from the start: the presence of a fully functional, bona fide, Boolean data type (see EWD1298, "Under the spell of Leibniz's Dream", p. 6, for a discussion of the genesis of the Boolean type). Not only does it sport operators giving rise to the full two-valued Boolean algebra, but Boolean expressions are first-class citizens that can be assigned to variables, passed to procedures and functions and returned from those.

Aside: Minimally, modern programming languages embody three algebraic structures: the Boolean algebra B, the integer field Z/2^NZ modulo some power of two (N = 64 is now fashionable) and the free monoid Σ^* over some alphabet (Σ = Unicode is now fashionable). The floating-point numbers, also usually present, don't seem to fit into any recognizable algebra, since they are not associative, not Archimedean and not even closed (cf IEEE 754 denormalized numbers).

Bearing this in mind, I will start by rewriting the program fragment (simplifying it in the process to eliminate details extraneous to this exercise) to make explicit the fact that the condition being tested is not a predicate, but a Boolean value:

bool isPeak(int i, double *buf)
{
    bool condition;
    
    condition = buf[i] > buf[i - 1] && buf[i] > buf[i + 1];
    if (condition)
        return true;
    return false;
}

The formal justification for the next transformation is somewhat convoluted, but essentially reduces to the fact that wp."return; S".P = wp."return".P, for any statement S and predicate P (for the notation wp, see the Wikipedia entry on predicate transformers); that is, instructions after a return are unreachable. Hence, after the conditional, ¬condition holds, and I can now restore its alternative branch:

bool isPeak(int i, double *buf)
{
    bool condition;
    
    condition = buf[i] > buf[i - 1] && buf[i] > buf[i + 1];
    if (condition)
        return true;
    else
        return false;
}

I can then reify the return value the same way I did with the condition, by introducing a variable, say, result:

bool isPeak(int i, double *buf)
{
    bool condition, result;
    
    condition = buf[i] > buf[i - 1] && buf[i] > buf[i + 1];
    if (condition)
        result = true;
    else
        result = false;
    return result;
}

Note that in the process I have taken outside the conditional the repeated return result statements.

The program has now a regular structure, that allows me to reconstruct the predicates satisfied after the execution of every statement:

bool isPeak(int i, double *buf)
{
    bool condition, result;
    
    condition = buf[i] > buf[i - 1] && buf[i] > buf[i + 1];
    if (condition)
        // condition
        result = true;
        // condition ∧ result
    else
        // ¬condition
        result = false;
        // ¬condition ∧ ¬result
    // (condition ∧ result) ∨ (¬condition ∧ ¬result)
    return result;
}

I will now massage the last predicate to reveal the, admittedly obvious, relationship between condition and result:

  (condition ∧ result) ∨ (¬condition ∧ ¬result)
≡ { Golden Rule }
  condition ∧ result ≡ ¬condition ∧ ¬result ≡ condition ∧ result ∧ ¬condition ∧ ¬result
≡ { Contradiction }
  condition ∧ result ≡ ¬condition ∧ ¬result ≡ false
≡ { Definition of ¬ }
  condition ∧ result ≡ ¬(¬condition ∧ ¬result)
≡ { DeMorgan }
  condition ∧ result ≡ ¬¬(condition ∨ result)
≡ { Involution }
  condition ∧ result ≡ condition ∨ result
≡ { Golden Rule }
  condition ≡ result

Thus the conditional reduces to the assignment statement, the minimal program that ensures that the two variables have the same value:

bool isPeak(int i, double *buf)
{
    bool condition, result;
    
    condition = buf[i] > buf[i - 1] && buf[i] > buf[i + 1];
    // condition ≡ condition
    result = condition;
    // condition ≡ result
    return result;
}

We see that the introduced variables served far more than as mere pedagogical devices: they permitted the restructuring of the program into a shape amenable to formal reasoning, according to the motto "name thy unknowns". That rôle fulfilled, I can eliminate them:

bool isPeak(int i, double *buf)
{
    return buf[i] > buf[i - 1] && buf[i] > buf[i + 1];
}

This is the function that the programmer should have written in the first place. Why didn't he?

I must by necessity speculate on the reasons of this widespread mental block. One plausible cause is that even if programmers might be somewhat familiar with predicate logic, they are not accustomed to manipulate Boolean objects in an algebraic, calculational fashion. Another one could be exposure to premature (and irrelevant!) operational considerations: thinking that the "computer" must "conditionally jump" to evaluate a "Boolean condition", believing that the conditional statement is "compiled to conditional jumps", et cœtera.

Aside: I shouldn't have cared, but out of curiosity I've compiled all seven versions of the program using GCC 3.1 (a mediocre compiler in terms of generated code, since it doesn't recognize that if (P) { S; return; } Q; can always be transformed to if (P) { S; return; } else Q;). With a suitable optimization level, every version but the first, longer by two instructions, compiled to exactly the same PPC code. The lesson one can derive from this is that broken symmetry is always costly, not only in terms of reduced expressive and reasoning power, but also in terms of lost efficiency.