this is an exposition showing that particular design problems in computer architecture can be seen as directly as an application of boolean algebra. there are a number of possible links that one can drawn between these two (very related) topics: my focus here is very specific to deriving combinatory logic from f : 𝔹n → 𝔹m C sorcery Luke Wren x & (x - 1) == 0

or

x & -x == x BNF in ?, the number representation is bitvectors 
     x + 1 = ¬x
    ∑
    take signed numbers, embed in an infinite binary string

    brief review

    0 1 0 0 1 0 1 1
    an 8-bit word

    two's complement

    The use of two's complement goes back to

    is true, then x is a power of two.

    review

    0 0 0 0
    0 0 1 1
    0 1 0 2
    0 1 1 3
    1 0 0 - 4
    1 0 1 - 5
    1 1 0 - 6
    1 1 1 - 7
    n=3
    <expr> = constant | variable
    binary and unary operators
    | <expr> <binop> <expr>
    | <op> <expr>
    <binop> = + | - | * | /
    | << | >> | ∧ | ∨ | xor
    <op> = - |
    | popcount

    first, popcount sticks out here: I think it's shortened from population count and conventionally means counting the number of set bits in a bitvector.

    the encoding of signed arithmetic has footguns but its structure is mostly conventional that's because the encoding is designed well all on their own act exactly as expected: if in diagramming the algebra any more unexpected properties are experessible. in Agda (see why Agda? for a background and primer.)

    assume boolean logic

    supplement type calculus boolean calculus if these terms are meaningless to you, I can recommend this resource but this post is intended as not in practice

    bitvector

    bitvector.agda>
    module bitvector where

open import prelude

BitVector : Nat -> Set
BitVector n = Vec Bool n

_∧ᵇ_ : ∀ {n} → BitVector n → BitVector n → BitVector n
∅ ∧ᵇ ∅ = ∅
(x ∷ xs) ∧ᵇ (y ∷ ys) = (x ∧ y) ∷ (xs ∧ᵇ ys)


_∨ᵇ_ : ∀ {n} → BitVector n → BitVector n → BitVector n
∅ ∨ᵇ ∅ = ∅
(x ∷ xs) ∨ᵇ (y ∷ ys) = (x ∨ y) ∷ (xs ∨ᵇ ys)

    embedding

    (&) : {n : N} -> BitVector n -> BitVector n -> BitVector n
(x , xs) & (y , ys) = (x * y) , (xs & ys)