Word and list operations with counters, in logarithmic space

Counter programs (Turing.CounterProgram) for operations that need a counter of logarithmic length, so that they are not finite-state transductions:

• the first k bits of a word, and the word without its first k bits, with k in unary after the framed word (shiftProgram);
• the list 0, …, n - 1 of a unary n (rangeProgram), with a nested counting loop;
• the element at a unary index of a list (lookupProgram), skipping framed elements with a position counter guarded by the length of the list encoding.

Each program reads the length n of the framed first component and the unary second component into registers (headerCode), and keeps its registers below the input length, so it computes its function in logarithmic space by Turing.CounterProgram.computableInLogSpace_of_reachesOut. None of this uses logarithmic-space composition, apart from the fun_prop forms at the end. The rules of LogSpace/Words are imported publicly, so that fun_prop has the full rule set.

Main definitions

• Turing.CounterProgram.Words.shiftProgram: emitting a shifted segment of a framed word.
• Turing.CounterProgram.Words.rangeProgram: enumerating 0, …, n - 1.
• Turing.CounterProgram.Words.lookupProgram: list lookup at a unary index.

Main results

• Turing.CounterProgram.Words.reachesOut_header: the run of the header, for programs built on it.
• Turing.MultiTapeTM.ComputableInLogSpace.bitsTake, Turing.MultiTapeTM.ComputableInLogSpace.bitsDrop: taking and dropping bits.
• Turing.MultiTapeTM.ComputableInLogSpace.range: the list 0, …, n - 1.
• Turing.MultiTapeTM.ComputableInLogSpace.getElem?: list lookup at a unary index.
• Turing.MultiTapeTM.ComputableInLogSpace.bitsTake', .bitsDrop', .getElem?': the same on computed arguments, in the form used by fun_prop, with which range is also registered.

References

• M. Sipser, Introduction to the Theory of Computation, Section 8.5

The input frame w ++ replicate k true

Reading the header: the length of the framed word and the unary count

def Turing.CounterProgram.Words.headerCode : List Instr

The header code: label 0 and 1 count the framed word into register 0, labels 2 and 3 count the unary tail into register 1; it exits at label 4.

theorem Turing.CounterProgram.Words.reachesOut_header {P : CounterProgram} {w : List Bool} {k B : ℕ} (hP : P.CodeAt 0 headerCode) (hB : 2 * w.length + 1 + k ≤ B) : P.ReachesOut (MultiTapeTM.frame w ++ List.replicate k true) (P.Active B) (0, [0, 0, 0, 0]) (4, [w.length, k, 0, 0]) []

The run of headerCode: from the initial registers it stores the length of the framed word in register 0 and the unary count in register 1, and exits at label 4, without emitting.

Emitting bits of the framed word

def Turing.CounterProgram.Words.emitCode : List Instr

The body emitting the bit at index reg 2 + reg 3 · reg 1, if any, then continuing at 7. With reg 3 = 0 this is the bit at the loop index; with reg 3 = 1 it is offset by k.

def Turing.CounterProgram.Words.shiftProgram (o : ℕ) (bound : Expr) : CounterProgram

A program emitting w[i + o·k] for i below the bound of its loop, where o ∈ {0, 1} is the initial value of register 3, set by the instruction at label 4.

Enumerating 0, …, n - 1

def Turing.CounterProgram.Words.rangeProgram : CounterProgram

The program enumerating 0, …, n - 1 in unary, as a list: labels 0 and 1 count the unary input into register 0; the loop at 2 runs register 1 over the elements, and the inner loop at 5 writes the framed unary digits of each element with register 2.

Looking up an element of a list

def Turing.CounterProgram.Words.lookupProgram : CounterProgram

The program looking up the element at a unary index in a list: the header reads the length n of the list encoding and the index k; the loop at 4 skips k framed elements with register 2 as the position, guarded by reg 2 < n; if an element remains, the code at 11 writes true and copies the element's digits.

theorem Turing.MultiTapeTM.ComputableInLogSpace.bitsTake : ComputableInLogSpace (fun (p : List Bool × ℕ) => List.take p.2 p.1) (encPair encBits encUnary) encBits

The first k bits of a word, with k in unary, in logarithmic space.

theorem Turing.MultiTapeTM.ComputableInLogSpace.bitsDrop : ComputableInLogSpace (fun (p : List Bool × ℕ) => List.drop p.2 p.1) (encPair encBits encUnary) encBits

A word without its first k bits, with k in unary, in logarithmic space.

theorem Turing.MultiTapeTM.ComputableInLogSpace.range : ComputableInLogSpace List.range encUnary (encList encUnary)

The list 0, …, n - 1, in unary, in logarithmic space.

theorem Turing.MultiTapeTM.ComputableInLogSpace.getElem? {α : Type} (enc : α ↪ List Bool) : ComputableInLogSpace (fun (p : List α × ℕ) => p.1[p.2]?) (encPair (encList enc) encUnary) (encOption enc)

Looking up the element at a unary index in a list, in logarithmic space.

Automation

theorem Turing.MultiTapeTM.ComputableInLogSpace.bitsTake' {γ : Type} {encIn : γ ↪ List Bool} {w : γ → List Bool} {k : γ → ℕ} (hw : ComputableInLogSpace w encIn encBits) (hk : ComputableInLogSpace k encIn encUnary) : ComputableInLogSpace (fun (a : γ) => List.take (k a) (w a)) encIn encBits

The first k bits of a computed word, in the form used by fun_prop.

theorem Turing.MultiTapeTM.ComputableInLogSpace.bitsDrop' {γ : Type} {encIn : γ ↪ List Bool} {w : γ → List Bool} {k : γ → ℕ} (hw : ComputableInLogSpace w encIn encBits) (hk : ComputableInLogSpace k encIn encUnary) : ComputableInLogSpace (fun (a : γ) => List.drop (k a) (w a)) encIn encBits

A computed word without its first k bits, in the form used by fun_prop.

theorem Turing.MultiTapeTM.ComputableInLogSpace.getElem?' {γ : Type} {encIn : γ ↪ List Bool} {α : Type} {enc : α ↪ List Bool} {l : γ → List α} {k : γ → ℕ} (hl : ComputableInLogSpace l encIn (encList enc)) (hk : ComputableInLogSpace k encIn encUnary) : ComputableInLogSpace (fun (a : γ) => (l a)[k a]?) encIn (encOption enc)

Looking up a computed unary index in a computed list, in the form used by fun_prop.