Linear resource bounds for tagged sum constructors

Prepending the fixed Boolean tag bit to the payload encoding costs linear time and space in the encoded input length, without any finite-domain or inhabitance assumption on either summand.

Main results

• Turing.MultiTapeTM.ComputableInO.inl, .inr: linear-time and linear-space tagged sum injections.
• Turing.MultiTapeTM.ComputableInO.getLeft?, .getRight?: linear-time and linear-space tagged sum projections.

References

Uses Christian Reitwiessner's native degree/resource calculus (ComputableInO.append).

theorem Turing.MultiTapeTM.ComputableInO.inl {α β : Type} (left : α ↪ List Bool) (right : β ↪ List Bool) : ComputableInO Sum.inl left (encSum left right) (fun (a : α) => (left a).length) fun (a : α) => (left a).length

A left sum tag has a direct native linear implementation.

theorem Turing.MultiTapeTM.ComputableInO.inr {α β : Type} (left : α ↪ List Bool) (right : β ↪ List Bool) : ComputableInO Sum.inr right (encSum left right) (fun (a : β) => (right a).length) fun (a : β) => (right a).length

A right sum tag has a direct native linear implementation.

theorem Turing.MultiTapeTM.ComputableInO.isLeft_deg {α β : Type} (left : α ↪ List Bool) (right : β ↪ List Bool) : ComputableInDegree Sum.isLeft (encSum left right) encBool 1 0

Testing for a left sum tag takes linear time and constant output size.

theorem Turing.MultiTapeTM.ComputableInO.isRight_deg {α β : Type} (left : α ↪ List Bool) (right : β ↪ List Bool) : ComputableInDegree Sum.isRight (encSum left right) encBool 1 0

Testing for a right sum tag takes linear time and constant output size.

theorem Turing.MultiTapeTM.ComputableInO.getLeft?_deg {α β : Type} (left : α ↪ List Bool) (right : β ↪ List Bool) : ComputableInDegree Sum.getLeft? (encSum left right) (encOption left) 1 1

Extracting the left summand as an option takes linear time and space.

theorem Turing.MultiTapeTM.ComputableInO.getRight?_deg {α β : Type} (left : α ↪ List Bool) (right : β ↪ List Bool) : ComputableInDegree Sum.getRight? (encSum left right) (encOption right) 1 1

Extracting the right summand as an option takes linear time and space.

theorem Turing.MultiTapeTM.ComputableInO.getLeft? {α β : Type} (left : α ↪ List Bool) (right : β ↪ List Bool) : ComputableInO Sum.getLeft? (encSum left right) (encOption left) (fun (s : α ⊕ β) => ((encSum left right) s).length) fun (s : α ⊕ β) => ((encSum left right) s).length

Extracting the left summand as an option has linear time and space bounds.

theorem Turing.MultiTapeTM.ComputableInO.getRight? {α β : Type} (left : α ↪ List Bool) (right : β ↪ List Bool) : ComputableInO Sum.getRight? (encSum left right) (encOption right) (fun (s : α ⊕ β) => ((encSum left right) s).length) fun (s : α ⊕ β) => ((encSum left right) s).length

Extracting the right summand as an option has linear time and space bounds.