Division with remainder, in unary

Every index decomposition in an algorithmic constraint graph is a division: which edge of the original graph, which step of the walk, which copy of the gadget. This module divides one unary number by another in polynomial time, by counting up and rolling the remainder over.

Main definitions

• Complexity.dmStep — one tick of the count

Main results

• Complexity.dmStep_iterate — the count divides
• Complexity.halfFn_mem_FP, Complexity.halfFn_eq — halving a length

def Complexity.dmStep (st : List Bool) : List Bool

One tick: extend the remainder, and roll it over into the quotient when it reaches the divisor. The state is pair (pair quotient remainder) divisor.

Equations

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

theorem Complexity.dmStep_mem_FP : dmStep ∈ FP

theorem Complexity.dmStep_iterate {B : List Bool} (hb : 0 < B.length) (a : ℕ) : dmStep^[a] (pair (pair [] []) B) = pair (pair (List.replicate (a / B.length) true) (List.replicate (a % B.length) true)) B

The count divides. After a ticks the state holds a / b and a % b.

Halving

theorem Complexity.length_selectHead_le (s x y : List Bool) : (Cobham.selectHead s x y).length ≤ max x.length y.length

theorem Complexity.dmStep_one (q r b : List Bool) : ∃ (q' : List Bool) (r' : List Bool), dmStep (pair (pair q r) b) = pair (pair q' r') b ∧ q'.length ≤ q.length + 1 ∧ r'.length ≤ r.length + 1

theorem Complexity.dmStep_shape (k : ℕ) (q r b : List Bool) : ∃ (q' : List Bool) (r' : List Bool), dmStep^[k] (pair (pair q r) b) = pair (pair q' r') b ∧ q'.length ≤ q.length + k ∧ r'.length ≤ r.length + k

noncomputable def Complexity.dmRun (b s : List Bool) : List Bool

The counting run: divide a length by a fixed divisor.

Equations

• Complexity.dmRun b s = Complexity.dmStep^[s.length] (Complexity.pair (Complexity.pair [] []) b)

noncomputable def Complexity.divFn (b s : List Bool) : List Bool

The quotient of a length by a fixed divisor, in unary.

Equations

• Complexity.divFn b s = Complexity.pairFst (Complexity.pairFst (Complexity.dmRun b s))

noncomputable def Complexity.modFn (b s : List Bool) : List Bool

The remainder of a length by a fixed divisor, in unary.

Equations

• Complexity.modFn b s = Complexity.pairSnd (Complexity.pairFst (Complexity.dmRun b s))

theorem Complexity.dmRun_mem_FP (b : List Bool) : dmRun b ∈ FP

theorem Complexity.divFn_mem_FP (b : List Bool) : divFn b ∈ FP

theorem Complexity.modFn_mem_FP (b : List Bool) : modFn b ∈ FP

theorem Complexity.divFn_eq {b : List Bool} (hb : 0 < b.length) (s : List Bool) : divFn b s = List.replicate (s.length / b.length) true

theorem Complexity.modFn_eq {b : List Bool} (hb : 0 < b.length) (s : List Bool) : modFn b s = List.replicate (s.length % b.length) true

Dividing by a length read from the input

theorem Complexity.fstBlock_len_le (z : List Bool) : (pairFst z).length ≤ z.length

theorem Complexity.sndBlock_len_le (z : List Bool) : (pairSnd z).length ≤ z.length

noncomputable def Complexity.dmRun2 (z : List Bool) : List Bool

The counting run with the divisor read from the argument: pair b s.

Equations

• Complexity.dmRun2 z = Complexity.dmStep^[(Complexity.pairSnd z).length] (Complexity.pair (Complexity.pair [] []) (Complexity.pairFst z))

noncomputable def Complexity.divFn2 (z : List Bool) : List Bool

The quotient of one length by another, in unary.

Equations

• Complexity.divFn2 z = Complexity.pairFst (Complexity.pairFst (Complexity.dmRun2 z))

noncomputable def Complexity.modFn2 (z : List Bool) : List Bool

The remainder of one length by another, in unary.

Equations

• Complexity.modFn2 z = Complexity.pairSnd (Complexity.pairFst (Complexity.dmRun2 z))

theorem Complexity.dmRun2_mem_FP : dmRun2 ∈ FP

theorem Complexity.divFn2_mem_FP : divFn2 ∈ FP

theorem Complexity.modFn2_mem_FP : modFn2 ∈ FP

theorem Complexity.divFn2_eq {b : List Bool} (hb : 0 < b.length) (s : List Bool) : divFn2 (pair b s) = List.replicate (s.length / b.length) true

theorem Complexity.modFn2_eq {b : List Bool} (hb : 0 < b.length) (s : List Bool) : modFn2 (pair b s) = List.replicate (s.length % b.length) true

noncomputable def Complexity.halfFn (s : List Bool) : List Bool

Halving a length, in unary.

Equations

• Complexity.halfFn s = Complexity.divFn [false, false] s

theorem Complexity.halfFn_mem_FP : halfFn ∈ FP

theorem Complexity.halfFn_eq (s : List Bool) : halfFn s = List.replicate (s.length / 2) true