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”
of bit vectors
and may be specified in a bit-wise manner as the bit vector
such that for all
, iff
.

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