Word operations for encodings

The building blocks of concrete encodings of pairs, options and lists, and their plain computability in linear time and space (Turing.MultiTapeTM.ComputableInLinearTimeAndSpace).

A word w is framed by writing each symbol b as [true, b] and appending [false]. A framed word marks its own end, so it can be followed by any word and still be read back.

Main definitions

• Turing.MultiTapeTM.frame: the framed word.
• Turing.MultiTapeTM.unframe, Turing.MultiTapeTM.dropFrame: the word framed at the start of a word, and what follows the frame.

Main results

• Turing.MultiTapeTM.frame_append_inj: a framed word followed by another word determines both.
• Functions that act on encoded values by frame, unframe, dropFrame, List.cons true, List.tail or List.take 1, or that test the encoded value for emptiness, are computable in linear time and space.

def Turing.MultiTapeTM.encOfEquiv {α : Type u_1} {β : Type u_2} (e : α ≃ β) (enc : β ↪ List Bool) : α ↪ List Bool

The encoding of α through an equivalence with β, such as that of a structure with the tuple of its fields.

@[simp]

theorem Turing.MultiTapeTM.encOfEquiv_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) (enc : β ↪ List Bool) (a : α) : (encOfEquiv e enc) a = enc (e a)