Binary list length in polynomial time

Turing.MultiTapeTM.ComputableTidilyInPolyTime.length_list computes the length of a framed list in unary (encUnary), the representation required by bounded loops and List.range. Verifiers and reductions that compare a list length against a binary parameter or add it to binary wire and vertex indices instead need the length in the binary natural encoding encNat. Composing length_list with unary_to_binary provides plain rules for fun_prop and polytime.

Main results

• Turing.MultiTapeTM.ComputableInPolyTime.length_list_binary: the length of a framed list in the binary encoding encNat.
• Turing.MultiTapeTM.ComputableInPolyTime.length_list_binary': the binary length of a computed framed list, fixing the intermediate list encoding for proof search.

theorem Turing.MultiTapeTM.ComputableInPolyTime.length_list_binary {α : Type} (enc : α ↪ List Bool) : ComputableInPolyTime (fun (l : List α) => l.length) (encList enc) encNat

Length of a framed list in binary (encNat); the element encoding is inferred from the list encoding.

theorem Turing.MultiTapeTM.ComputableInPolyTime.length_list_binary' {α β : Type} {input : α ↪ List Bool} {enc : β ↪ List Bool} {list : α → List β} (hlist : ComputableInPolyTime list input (encList enc)) : ComputableInPolyTime (fun (a : α) => (list a).length) input encNat

Length of a computed framed list in binary (encNat), fixing the intermediate list encoding for proof search.