Linear bounds for the optional head of a list

The certificate uses the framed list and option encodings and charges encoded output to space. The inhabitance hypothesis supplies a fixed default for the head primitive; the result remains none on the empty list. Apply the certificate explicitly to compose it with other computations.

Main results

• Turing.MultiTapeTM.ComputableInO.head?: linear time and charged space for List.head?.

theorem Turing.MultiTapeTM.ComputableInO.head? {β : Type} {encB : β ↪ List Bool} [Inhabited β] : ComputableInO (fun (l : List β) => l.head?) (encList encB) (encOption encB) (fun (l : List β) => (2 * (encB default).length + 8) * (((encList encB) l).length + 1)) fun (l : List β) => (2 * (encB default).length + 8) * (((encList encB) l).length + 1)

Read the optional head in linear time and charged space. The displayed constant depends only on the fixed default encoding, not on the input list.