Documentation

CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.BigO.Cases

Case analysis on a component, within given bounds #

Case analysis on the second component of a pair, when that component is a tagged sum (Turing.MultiTapeTM.encSum) or an option (Turing.MultiTapeTM.encOption). Each branch need only be computable on its own case, and only the branch taken is charged, plus the length of the encoded input. No default values of the component types are needed: the branches run on the inputs of their case only.

Main results #

source
theorem Turing.MultiTapeTM.ComputableInO.sumElimSnd {π α β ε : Type} {encP : π ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encE : ε ↪ List Bool} {f : π × α → ε} {g : π × β → ε} {Tf Sf : π × α → ℕ} {Tg Sg : π × β → ℕ} (hf : ComputableInO f (encPair encP encA) encE Tf Sf) (hg : ComputableInO g (encPair encP encB) encE Tg Sg) :
ComputableInO (fun (p : π × (α ⊕ β)) => Sum.elim (fun (a : α) => f (p.1, a)) (fun (b : β) => g (p.1, b)) p.2) (encPair encP (encSum encA encB)) encE (fun (p : π × (α ⊕ β)) => ((encPair encP (encSum encA encB)) p).length + Sum.elim (fun (a : α) => Tf (p.1, a)) (fun (b : β) => Tg (p.1, b)) p.2) fun (p : π × (α ⊕ β)) => ((encPair encP (encSum encA encB)) p).length + Sum.elim (fun (a : α) => Sf (p.1, a)) (fun (b : β) => Sg (p.1, b)) p.2

Case analysis on a sum component. If f is computable on the left case and g on the right case, so is the case analysis, within the bounds of the branch taken plus the length of the encoded input.

source
theorem Turing.MultiTapeTM.ComputableInO.optionElimSnd {π α ε : Type} {encP : π ↪ List Bool} {encA : α ↪ List Bool} {encE : ε ↪ List Bool} {f : π → ε} {g : π × α → ε} {Tf Sf : π → ℕ} {Tg Sg : π × α → ℕ} (hf : ComputableInO f encP encE Tf Sf) (hg : ComputableInO g (encPair encP encA) encE Tg Sg) :
ComputableInO (fun (p : π × Option α) => p.2.elim (f p.1) fun (a : α) => g (p.1, a)) (encPair encP (encOption encA)) encE (fun (p : π × Option α) => ((encPair encP (encOption encA)) p).length + p.2.elim (Tf p.1) fun (a : α) => Tg (p.1, a)) fun (p : π × Option α) => ((encPair encP (encOption encA)) p).length + p.2.elim (Sf p.1) fun (a : α) => Sg (p.1, a)

Case analysis on an option component. If f is computable on the first component in the none case and g on the pair in the some case, so is the case analysis, within the bounds of the branch taken plus the length of the encoded input.