Polynomial-time operations on signed unary integers

Operations on Christian Reitwiessner's encIntUnary: the sign bit is followed by n unary bits for Int.ofNat n or Int.negSucc n. In the negative case the magnitude is n + 1. Natural inputs and outputs use encUnary, so these rules support polynomially bounded tape positions and their indices in a computation tableau.

Main results

• Turing.MultiTapeTM.ComputableInPolyTime.int_natCast, .int_negSucc: constructing signed integers from unary naturals.
• Turing.MultiTapeTM.ComputableInPolyTime.int_natCast_sub: the signed difference of unary naturals.
• Turing.MultiTapeTM.ComputableInPolyTime.int_succ, .int_pred, .int_pos, .int_neg: unit shifts and sign tests.
• Turing.MultiTapeTM.ComputableInPolyTime.int_toNat, .int_natAbs, .int_equivNat: nonnegative truncation, absolute value and the standard numbering of integers, in unary.
• Turing.MultiTapeTM.ComputableInPolyTime.int_sub: subtraction of signed unary integers.
• Turing.MultiTapeTM.ComputableInPolyTime.int_sub_sign, .int_abs_le_nat: fixed tape moves and membership in a unary-bounded window.
• Turing.MultiTapeTM.ComputableInPolyTime.int_abs_le_nat': window membership for computed positions and bounds.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach

theorem Turing.MultiTapeTM.ComputableInPolyTime.int_natCast : ComputableInPolyTime (fun (n : ℕ) => ↑n) encUnary encIntUnary

Interpret a unary natural as a nonnegative signed integer.

theorem Turing.MultiTapeTM.ComputableInPolyTime.int_negSucc : ComputableInPolyTime Int.negSucc encUnary encIntUnary

Construct -(n + 1) from a unary natural n.

theorem Turing.MultiTapeTM.ComputableInPolyTime.int_natCast_sub : ComputableInPolyTime (fun (p : ℕ × ℕ) => ↑p.1 - ↑p.2) (encPair encUnary encUnary) encIntUnary

Subtract unary naturals without truncating at zero.

theorem Turing.MultiTapeTM.ComputableInPolyTime.int_succ : ComputableInPolyTime (fun (z : ℤ) => z + 1) encIntUnary encIntUnary

Shift a signed unary integer one cell to the right.

theorem Turing.MultiTapeTM.ComputableInPolyTime.int_pred : ComputableInPolyTime (fun (z : ℤ) => z - 1) encIntUnary encIntUnary

Shift a signed unary integer one cell to the left.

theorem Turing.MultiTapeTM.ComputableInPolyTime.int_pos : ComputableInPolyTime (fun (z : ℤ) => decide (0 < z)) encIntUnary encBool

Test whether a signed unary integer is positive.

theorem Turing.MultiTapeTM.ComputableInPolyTime.int_neg : ComputableInPolyTime (fun (z : ℤ) => decide (z < 0)) encIntUnary encBool

Test whether a signed unary integer is negative.

theorem Turing.MultiTapeTM.ComputableInPolyTime.int_toNat : ComputableInPolyTime Int.toNat encIntUnary encUnary

Truncate a signed integer at zero and return the result in unary.

theorem Turing.MultiTapeTM.ComputableInPolyTime.int_natAbs : ComputableInPolyTime Int.natAbs encIntUnary encUnary

Return the magnitude in unary, accounting for the offset in negative encodings.

theorem Turing.MultiTapeTM.ComputableInPolyTime.int_sub : ComputableInPolyTime (fun (p : ℤ × ℤ) => p.1 - p.2) (encPair encIntUnary encIntUnary) encIntUnary

Subtract two signed unary integers.

theorem Turing.MultiTapeTM.ComputableInPolyTime.int_sub_sign (direction : SignType) : ComputableInPolyTime (fun (z : ℤ) => z - ↑direction) encIntUnary encIntUnary

Subtract a fixed tape direction from a signed unary position.

theorem Turing.MultiTapeTM.ComputableInPolyTime.int_abs_le_nat : ComputableInPolyTime (fun (p : ℤ × ℕ) => decide (|p.1| ≤ ↑p.2)) (encPair encIntUnary encUnary) encBool

Compare a signed unary position's magnitude with a unary window bound.

theorem Turing.MultiTapeTM.ComputableInPolyTime.int_abs_le_nat' {α : Type} {input : α ↪ List Bool} {position : α → ℤ} {bound : α → ℕ} (hposition : ComputableInPolyTime position input encIntUnary) (hbound : ComputableInPolyTime bound input encUnary) : ComputableInPolyTime (fun (a : α) => decide (|position a| ≤ ↑(bound a))) input encBool

Test window membership after computing the signed position and unary bound.

theorem Turing.MultiTapeTM.ComputableInPolyTime.int_equivNat : ComputableInPolyTime (⇑Equiv.intEquivNat) encIntUnary encUnary

Number signed integers by 0, -1, 1, -2, …, returning the index in unary.