3  Logical Operations

In this chapter, we define and analyze the four basic logical operations: the unary “not”, or complement, and the binary “and”, “inclusive or” and “exclusive or”. These are commonly known as bit-wise operations, as each one may be computed by performing a certain computation on each bit of its argument (in the unary case) or each pair of corresponding bits of its arguments (for binary operations). For example, the logical “and” $ x \;\verb!&!\; y$ of bit vectors $ x$ and $ y$ may be specified in a bit-wise manner as the bit vector $ z$ such that for all $ k \in \mathbb{N}$, $ z[k] = 1$ iff $ x[k] = y[k] = 1$.

In the context of our formalization, however, the logical operations are more naturally defined as arithmetic functions: the complement is constructed as an arithmetic difference and the binary operations are defined by recursive formulas, which facilitate inductive proofs of their relevant properties. Among these are the bit-wise characterizations, as represented by Lemmas 3.1.14 and 3.2.5.


David Russinoff 2017-08-01