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.

theorem Turing.MultiTapeTM.ComputableTidilyInLinearTimeAndSpace.of_frame {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} (h : ∀ (a : α), encOut (f a) = frame (encIn a)) : ComputableTidilyInLinearTimeAndSpace f encIn encOut

Framing an encoded value.

theorem Turing.MultiTapeTM.ComputableTidilyInLinearTimeAndSpace.of_unframe {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} (h : ∀ (a : α), encOut (f a) = unframe (encIn a)) : ComputableTidilyInLinearTimeAndSpace f encIn encOut

Reading the word framed at the start of an encoded value.

theorem Turing.MultiTapeTM.ComputableTidilyInLinearTimeAndSpace.of_dropFrame {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} (h : ∀ (a : α), encOut (f a) = dropFrame (encIn a)) : ComputableTidilyInLinearTimeAndSpace f encIn encOut

Dropping the frame at the start of an encoded value.

theorem Turing.MultiTapeTM.ComputableTidilyInLinearTimeAndSpace.of_cons_true {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} (h : ∀ (a : α), encOut (f a) = true :: encIn a) : ComputableTidilyInLinearTimeAndSpace f encIn encOut

Prepending true to an encoded value.

theorem Turing.MultiTapeTM.ComputableTidilyInLinearTimeAndSpace.of_tail {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} (h : ∀ (a : α), encOut (f a) = (encIn a).tail) : ComputableTidilyInLinearTimeAndSpace f encIn encOut

Dropping the first symbol of an encoded value.

theorem Turing.MultiTapeTM.ComputableTidilyInLinearTimeAndSpace.of_take_one {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} (h : ∀ (a : α), encOut (f a) = List.take 1 (encIn a)) : ComputableTidilyInLinearTimeAndSpace f encIn encOut

Keeping just the first symbol of an encoded value.

theorem Turing.MultiTapeTM.ComputableTidilyInLinearTimeAndSpace.of_isEmpty {α : Type u_1} {encIn : α ↪ List Bool} {f : α → Bool} (h : ∀ (a : α), f a = (encIn a).isEmpty) : ComputableTidilyInLinearTimeAndSpace f encIn encBool

Testing an encoded value for emptiness.