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 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.ComputableInSpace (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).