Polynomial-time arithmetic on unary counters

Arithmetic on encUnary, built from Christian Reitwiessner's encodings and machine calculus. Addition concatenates the unary words; multiplication folds addition while keeping a quadratic bound on the accumulator. Fixed powers and fixed polynomials follow by composition. These operations support polynomially bounded counters and list enumeration in reductions.

Main results

• Turing.MultiTapeTM.ComputableTidilyInPolyTime.indexed_polynomial_bound: a uniform polynomial bound over a polynomially bounded range of indices, without computing the selected index.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_add, .unary_sub, .unary_mul: arithmetic on unary naturals.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_min, .unary_max: the smaller and larger of two unary naturals.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_le, .unary_lt, .unary_pair: comparisons and the natural-number pairing function.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_le', .unary_lt': comparisons of computed operands with the intermediate unary encodings fixed for automation.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_pow, .unary_eval: evaluation of a fixed power or polynomial, with input and output in unary.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_to_binary: conversion from unary to the binary encoding encNat.

References

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

The indexed bound is adapted from Cslib/Computability/Probabilistic/Encoding.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bool_toUnary : ComputableTidilyInPolyTime Bool.toNat encBool encUnary

Interpret one Boolean as a unary zero or one.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.polynomiallyBounded {f : ℕ → ℕ} (hf : ComputableTidilyInPolyTime f encUnary encUnary) : Cslib.PolynomiallyBounded f

A unary-output polynomial-time function is polynomially bounded in its unary input.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.indexed_polynomial_bound {f : ℕ → ℕ → ℕ} {count : ℕ → ℕ} (hf : ComputableTidilyInPolyTime (fun (input : ℕ × ℕ) => f input.1 input.2) (encPair encUnary encUnary) encUnary) (hcount : Cslib.PolynomiallyBounded count) : ∃ (c : ℕ) (d : ℕ), ∀ (n i : ℕ), i < count n → f n i ≤ c * (n + 1) ^ d

Efficient unary values share a polynomial bound over a polynomially bounded range of indices. Selecting an index does not require a computable choice.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_add : ComputableTidilyInPolyTime (fun (p : ℕ × ℕ) => p.1 + p.2) (encPair encUnary encUnary) encUnary

Addition of unary naturals, by concatenating their encodings.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_sub : ComputableTidilyInPolyTime (fun (p : ℕ × ℕ) => p.1 - p.2) (encPair encUnary encUnary) encUnary

Truncated subtraction of unary naturals.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_mul : ComputableTidilyInPolyTime (fun (p : ℕ × ℕ) => p.1 * p.2) (encPair encUnary encUnary) encUnary

Multiplication of unary naturals, by repeated addition.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_min : ComputableTidilyInPolyTime (fun (p : ℕ × ℕ) => min p.1 p.2) (encPair encUnary encUnary) encUnary

Take the smaller of two unary naturals.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_max : ComputableTidilyInPolyTime (fun (p : ℕ × ℕ) => max p.1 p.2) (encPair encUnary encUnary) encUnary

Take the larger of two unary naturals.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_le : ComputableTidilyInPolyTime (fun (p : ℕ × ℕ) => decide (p.1 ≤ p.2)) (encPair encUnary encUnary) encBool

Compare unary naturals.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_lt : ComputableTidilyInPolyTime (fun (p : ℕ × ℕ) => decide (p.1 < p.2)) (encPair encUnary encUnary) encBool

Strict comparison of unary naturals.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_le' {α : Type} {input : α ↪ List Bool} {left right : α → ℕ} (hleft : ComputableTidilyInPolyTime left input encUnary) (hright : ComputableTidilyInPolyTime right input encUnary) : ComputableTidilyInPolyTime (fun (a : α) => decide (left a ≤ right a)) input encBool

Compare computed unary values, fixing their intermediate encodings before proof search.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_lt' {α : Type} {input : α ↪ List Bool} {left right : α → ℕ} (hleft : ComputableTidilyInPolyTime left input encUnary) (hright : ComputableTidilyInPolyTime right input encUnary) : ComputableTidilyInPolyTime (fun (a : α) => decide (left a < right a)) input encBool

Strictly compare computed unary values, with both operand encodings fixed.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_beq {α : Type} {input : α ↪ List Bool} {left right : α → ℕ} (hleft : ComputableTidilyInPolyTime left input encUnary) (hright : ComputableTidilyInPolyTime right input encUnary) : ComputableTidilyInPolyTime (fun (a : α) => left a == right a) input encBool

Equality of computed unary counters, fixing the intermediate encoding for proof search.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_pair : ComputableTidilyInPolyTime (fun (p : ℕ × ℕ) => Nat.pair p.1 p.2) (encPair encUnary encUnary) encUnary

The natural-number pairing function, with both arguments and the result in unary.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_pow (d : ℕ) : ComputableTidilyInPolyTime (fun (n : ℕ) => n ^ d) encUnary encUnary

A fixed power of a unary natural.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_eval (p : Polynomial ℕ) : ComputableTidilyInPolyTime (fun (x : ℕ) => Polynomial.eval x p) encUnary encUnary

Evaluate a fixed polynomial on unary naturals, with its result also in unary.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_to_binary : ComputableTidilyInPolyTime (fun (n : ℕ) => n) encUnary encNat

Convert a unary natural to its binary encoding by incrementing a binary counter.

Plain polynomial-time automation

theorem Turing.MultiTapeTM.ComputableInPolyTime.unary_add : ComputableInPolyTime (fun (p : ℕ × ℕ) => p.1 + p.2) (encPair encUnary encUnary) encUnary

Addition of unary naturals, by concatenating their encodings.

theorem Turing.MultiTapeTM.ComputableInPolyTime.unary_eval (p : Polynomial ℕ) : ComputableInPolyTime (fun (x : ℕ) => Polynomial.eval x p) encUnary encUnary

Evaluate a fixed polynomial on unary naturals, with its result also in unary.

theorem Turing.MultiTapeTM.ComputableInPolyTime.unary_mul : ComputableInPolyTime (fun (p : ℕ × ℕ) => p.1 * p.2) (encPair encUnary encUnary) encUnary

Multiplication of unary naturals, by repeated addition.

theorem Turing.MultiTapeTM.ComputableInPolyTime.unary_add' {α : Type} {input : α ↪ List Bool} {left right : α → ℕ} (hleft : ComputableInPolyTime left input encUnary) (hright : ComputableInPolyTime right input encUnary) : ComputableInPolyTime (fun (a : α) => left a + right a) input encUnary

Add two computed unary naturals with the same full input context.

theorem Turing.MultiTapeTM.ComputableInPolyTime.unary_sub' {α : Type} {input : α ↪ List Bool} {left right : α → ℕ} (hleft : ComputableInPolyTime left input encUnary) (hright : ComputableInPolyTime right input encUnary) : ComputableInPolyTime (fun (a : α) => left a - right a) input encUnary

Subtract two computed unary naturals with the same full input context.

theorem Turing.MultiTapeTM.ComputableInPolyTime.unary_mul' {α : Type} {input : α ↪ List Bool} {left right : α → ℕ} (hleft : ComputableInPolyTime left input encUnary) (hright : ComputableInPolyTime right input encUnary) : ComputableInPolyTime (fun (a : α) => left a * right a) input encUnary

Multiply two computed unary naturals with the same full input context.

theorem Turing.MultiTapeTM.ComputableInPolyTime.unary_pow (d : ℕ) : ComputableInPolyTime (fun (n : ℕ) => n ^ d) encUnary encUnary

A fixed power of a unary natural.