Total decoding of binary signed integers

Read a sign bit and a binary magnitude. Missing data is zero, surplus high zero bits are ignored, and negative zero is normalized to zero. This reuses the existing natural-number decoder and sign/magnitude arithmetic. The roundtrip applies to every canonical encIntBin word; total decoding alone is not a canonical-input validator.

Main definitions

• Turing.MultiTapeTM.decodeIntBin: total sign/magnitude decoding.

Main results

• Turing.MultiTapeTM.decodeIntBin_encIntBin: exact roundtrip.
• Turing.MultiTapeTM.computableInPolyTime_decodeIntBin: the complete plain decoding contract.

def Turing.MultiTapeTM.decodeIntBin (word : List Bool) : ℤ

Decode any sign/magnitude word; malformed and negative-zero words still decode totally.

theorem Turing.MultiTapeTM.decodeIntBin_encIntBin (z : ℤ) : decodeIntBin (encIntBin z) = z

Every canonical signed binary word decodes to its original integer.

theorem Turing.MultiTapeTM.computableInPolyTime_decodeIntBin : ComputableInPolyTime decodeIntBin encBits encIntBin

Binary sign/magnitude decoding is uniformly plain polynomial time on arbitrary words.