Binary sign-magnitude integers

encIntBin encodes an integer by a sign bit, true for negative integers, followed by the binary digits of its magnitude (Turing.MultiTapeTM.encNat), least significant first. The magnitude is not framed: the sign is a single leading bit, the digits are the rest of the word, and the magnitude is the tail of the code, so the binary natural arithmetic applies to it directly. A negative integer has a nonzero magnitude, so zero has the single code [false]. An integer z occupies Nat.size z.natAbs + 1 bits. The unary integers Turing.MultiTapeTM.encInt index tape positions; this encoding carries values whose magnitude is exponential in their length.

Main definitions

• Turing.MultiTapeTM.encIntBin: integers as a sign bit followed by a binary magnitude.

Main results

• Turing.MultiTapeTM.length_encIntBin: the code of z has Nat.size z.natAbs + 1 bits.
• Turing.MultiTapeTM.encIntBin_natCast, Turing.MultiTapeTM.encIntBin_negSucc: the codes of nonnegative and negative integers.

def Turing.MultiTapeTM.encIntBin : ℤ ↪ List Bool

Integers in binary sign-magnitude form: the bit z < 0 followed by the binary digits of the magnitude z.natAbs, least significant first. Zero is encoded as [false] only.

@[simp]

theorem Turing.MultiTapeTM.encIntBin_apply (z : ℤ) : encIntBin z = decide (z < 0) :: z.natAbs.bits

theorem Turing.MultiTapeTM.length_encIntBin (z : ℤ) : (encIntBin z).length = z.natAbs.size + 1

The code of an integer has one sign bit and the binary length of its magnitude.

theorem Turing.MultiTapeTM.encIntBin_natCast (n : ℕ) : encIntBin ↑n = false :: n.bits

theorem Turing.MultiTapeTM.encIntBin_zero : encIntBin 0 = [false]

theorem Turing.MultiTapeTM.encIntBin_negSucc (n : ℕ) : encIntBin (Int.negSucc n) = true :: (n + 1).bits