Polynomial-time enumeration of tape windows

The existing Turing.windowList enumerates -T, …, T from left to right. With the bound in unary and the positions in signed unary, the same list is computable in polynomial time.

Main results

• Turing.computableInPolyTime_windowList.
• Turing.MultiTapeTM.ComputableInPolyTime.moveInputPosNat: total input-head movement, including clipping when the supplied position exceeds the input boundary.

References

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

theorem Turing.computableInPolyTime_windowList : MultiTapeTM.ComputableInPolyTime windowList MultiTapeTM.encUnary (MultiTapeTM.encList MultiTapeTM.encIntUnary)

Enumerate all tape positions within a unary distance of the origin, in signed unary.

theorem Turing.MultiTapeTM.ComputableInPolyTime.moveInputPosNat (direction : SignType) : ComputableInPolyTime (fun (p : ℕ × ℕ) => Turing.moveInputPosNat p.1 p.2 direction) (encPair encUnary encUnary) encUnary

Move and clamp a unary input-head position, including positions outside the input boundary.