BIT predicate

The BIT predicate was first introduced in 1937 by Wilhelm Ackermann to define the Ackermann coding, which encodes hereditarily finite sets as natural numbers. The BIT predicate can be used to perform membership tests for the encoded sets.[1][2]

In mathematical notation, the BIT predicate can be described as

${\displaystyle {\text{BIT}}(i,j)=\lfloor i\mathbin {/} 2^{j}\rfloor {\bmod {2}}}$

where ${\displaystyle \lfloor \cdot \rfloor }$ is the floor function and mod is the modulo function.

The BIT predicate is primitive recursive.[3]

In programming languages such as C, C++, Java, or Python that provide a right shift operator >> and a bitwise Boolean and operator &, the BIT predicate BIT(i, j) can be implemented by the expression (i>>j)&1. Here the bits of i are numbered from the low-order bits to high-order bits in the binary representation of i, with the ones bit being numbered as bit 0. The subexpression i>>j shifts these bits so that bit j is shifted to position 0, and the subexpression &1 masks off the remaining bits, leaving only the bit in position 0. The value of the expression is 1 or 0, respectively as the value of BIT(i, j) is false or true.[4]

For a set represented as a bit array, the BIT predicate can be used to test set membership. For instance, subsets of the non-negative integers ${\displaystyle \{0,1,\ldots \}}$ may be represented by a bit array with a one in position ${\displaystyle i}$ when ${\displaystyle i}$ is a member of the subset, and a zero in that position when it is not a member. When such a bit array is interpreted as a binary number, the set ${\displaystyle \{i,j,k,\dots \}}$ for ${\displaystyle i,j,k,\dots }$ all distinct is represented as the binary number ${\displaystyle 2^{i}+2^{j}+2^{k}+\cdots }$. If ${\displaystyle S}$ is a set, represented in this way, and ${\displaystyle i}$ is a number that may or may not be an element of ${\displaystyle S}$, then BIT${\displaystyle (S,i)}$ returns a nonzero value when ${\displaystyle i}$ is a member and zero when it is not.

The same technique may be used to encode subsets of any sequence ${\displaystyle x_{0},x_{1},\dots }$ of distinct values, using powers of two whose exponents are the positions of the elements in this sequence, rather than their values. Ackermann's encoding of the hereditarily finite sets is an example of this technique, for the recursively-generated sequence of hereditarily finite sets.