Loops over a range of indices — definitions

A loop over the indices 0, 1, …, n - 1 is described by a rule E, which reads pair z (1^i) (the loop's input z and the index i in unary) and says what the loop contributes at index i. Every loop here reads its range and its input from one string pair u z, and runs over the indices below |u|; only the length of u matters, so the count is written in unary.

This file only says what the loops compute. Complexitylib.Classes.P.Range proves that each is polynomial-time whenever its rule is.

Main definitions

• Complexity.catRange — the rule's outputs over the range, run together
• Complexity.listEncFn — the same between the two bracket bits that DataEncode puts around the entries of a list
• Complexity.countOver — the total length of the outputs, in unary
• Complexity.findFirst — the least index at which the rule outputs anything
• Complexity.maxOver, Complexity.maxFn — the greatest output length

Concatenation

def Complexity.catRange (E : List Bool → List Bool) (z : List Bool) : List Bool

Concatenation over a range. On pair u z, the outputs of E on pair z (1^i) for i = 0, 1, …, |u| - 1, run together.

Equations

• Complexity.catRange E z = List.flatMap (fun (i : ℕ) => E (Complexity.pair (Complexity.pairSnd z) (List.replicate i true))) (List.range (Complexity.pairFst z).length)

def Complexity.listEncFn (E : List Bool → List Bool) (z : List Bool) : List Bool

The list encoder: catRange between a leading false and a trailing true. When the rule writes the encodings of a list's entries, this is the encoding of the list.

Equations

• Complexity.listEncFn E z = false :: Complexity.catRange E z ++ [true]

Counting and searching

def Complexity.countOver (E : List Bool → List Bool) (z : List Bool) : List Bool

The total length of the rule's outputs over the range, in unary. A rule that outputs [true] or [] counts the indices where it says yes.

Equations

• Complexity.countOver E z = List.replicate (Complexity.catRange E z).length true

def Complexity.isEmptyMark : List Bool → List Bool

One mark when the string is empty, none otherwise.

Equations

• Complexity.isEmptyMark [] = [true]
• Complexity.isEmptyMark (head :: tail) = []

def Complexity.findFirst (E : List Bool → List Bool) (z : List Bool) : List Bool

The least index below the bound at which the rule outputs anything, or the bound itself when it never does, in unary. At index j it marks whether the rule has output nothing on the indices up to j, and counts the marks.

Equations

• One or more equations did not get rendered due to their size.

The maximum

def Complexity.maxOver (f : List Bool → List Bool) (z : List Bool) : ℕ → ℕ

The largest length among the outputs of f on pair z (1^i) for i < n, and 0 when n = 0.

Equations

• Complexity.maxOver f z 0 = 0
• Complexity.maxOver f z n.succ = max (Complexity.maxOver f z n) (f (Complexity.pair z (List.replicate n true))).length

def Complexity.nonemptyMark : List Bool → List Bool

One mark when the string is nonempty, none otherwise.

Equations

• Complexity.nonemptyMark [] = []
• Complexity.nonemptyMark (head :: tail) = [true]

def Complexity.dropEntry (f : List Bool → List Bool) (v : List Bool) : List Bool

The output of f on pair z (1^i) with its first j bits dropped, read off pair (pair z (1^j)) (1^i).

Equations

• Complexity.dropEntry f v = List.drop (Complexity.pairSnd (Complexity.pairFst v)).length (f (Complexity.pair (Complexity.pairFst (Complexity.pairFst v)) (Complexity.pairSnd v)))

def Complexity.maxProbe (f : List Bool → List Bool) (w : List Bool) : List Bool

Whether some output of f over the range of pair u z is longer than j, read off pair (pair u z) (1^j), as one mark or none.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.maxFn (f : List Bool → List Bool) (w : List Bool) : List Bool

The greatest output length over the range, in unary. The maximum is at most the total length, so it is the number of j below the total length that some output is longer than.

Equations

• Complexity.maxFn f w = Complexity.countOver (Complexity.maxProbe f) (Complexity.pair (Complexity.countOver f w) w)