Word operations for encodings

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

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 tidily computable in linear time and space.

Framed words

def Turing.MultiTapeTM.frame (w : List Bool) : List Bool

Each symbol b of w as [true, b], followed by [false].

def Turing.MultiTapeTM.unframe : List Bool → List Bool

The word framed at the start of v, see Turing.MultiTapeTM.frame.

def Turing.MultiTapeTM.dropFrame : List Bool → List Bool

What follows the frame at the start of v, see Turing.MultiTapeTM.frame.

@[simp]

theorem Turing.MultiTapeTM.frame_nil : frame [] = [false]

@[simp]

theorem Turing.MultiTapeTM.frame_cons (b : Bool) (w : List Bool) : frame (b :: w) = true :: b :: frame w

@[simp]

theorem Turing.MultiTapeTM.length_frame (w : List Bool) : (frame w).length = 2 * w.length + 1

@[simp]

theorem Turing.MultiTapeTM.unframe_frame_append (w u : List Bool) : unframe (frame w ++ u) = w

@[simp]

theorem Turing.MultiTapeTM.unframe_frame (w : List Bool) : unframe (frame w) = w

@[simp]

theorem Turing.MultiTapeTM.dropFrame_frame_append (w u : List Bool) : dropFrame (frame w ++ u) = u

theorem Turing.MultiTapeTM.frame_append_inj {w w' u u' : List Bool} (h : frame w ++ u = frame w' ++ u') : w = w' ∧ u = u'

A framed word followed by another word determines both.

theorem Turing.MultiTapeTM.frame_injective : Function.Injective frame

Framing is injective.

@[simp]

theorem Turing.MultiTapeTM.frame_ne_nil (w : List Bool) : frame w ≠ []

Transducers for the word operations

def Turing.MultiTapeTM.Encodings.frameT : Transducer Bool Unit

Frames its input.

@[simp]

theorem Turing.MultiTapeTM.Encodings.frameT_q₀ : frameT.q₀ = ()

@[simp]

theorem Turing.MultiTapeTM.Encodings.frameT_step (x✝ : Unit) (b : Bool) : frameT.step x✝ b = ((), [true, b])

@[simp]

theorem Turing.MultiTapeTM.Encodings.frameT_final (x✝ : Unit) : frameT.final x✝ = [false]

theorem Turing.MultiTapeTM.Encodings.frameT_run (v : List Bool) : frameT.run () v = frame v

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)

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.

theorem Turing.MultiTapeTM.ComputableTidilyInLinearTimeAndSpace.of_isEmpty_ite {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} (d : β) (hd : ∀ (a : α), encIn a = [] → f a = d) (h : ComputableTidilyInLinearTimeAndSpace (f ∘ Subtype.val) ((Function.Embedding.subtype fun (a : α) => (encIn a).isEmpty = false).trans encIn) encOut) : ComputableTidilyInLinearTimeAndSpace f encIn encOut

A function with a fixed value d on the input encoded by the empty word, and tidily computable in linear time and space on the other inputs.