The weights of table entries within linear work space

The weight Cslib.TreeEval.Reader.weight p ℓ k x y, the product of x j or 1 - x j over the low bits of k and the same over its high bits for y, is tidily computable within work space linear in the lengths of its encoded arguments and in ℓ. Its products are taken over a counter rather than a list of indices, and they stay short: below p, or, for p = 0, no longer than the registers together.

Main results

• Cslib.TreeEval.Reader.weight_inSpace: the weight.

Half of a weight, over a counter

@[reducible, inline]

abbrev Cslib.TreeEval.Reader.encWeightIn : (ℕ × ℕ × ℕ) × List ℕ × List ℕ ↪ List Bool

The encoding of the arguments of a weight.

theorem Cslib.TreeEval.Reader.weight_inSpace : Turing.MultiTapeTM.ComputableTidilyInSpace (fun (w : (ℕ × ℕ × ℕ) × List ℕ × List ℕ) => weight w.1.1 w.1.2.1 w.1.2.2 w.2.1 w.2.2) encWeightIn Turing.MultiTapeTM.encNat fun (w : (ℕ × ℕ × ℕ) × List ℕ × List ℕ) => 64 * ((encWeightIn w).length + w.1.2.1 + 1)

The weight, weight p ℓ k x y from ((p, ℓ, k), x, y).