Direct plain polynomial-time option operations

The option encoding machines supply construction and fixed-default elimination. Composition retains every encoded input, including captured arguments and a runtime fallback. Empty value types need no inhabitant assumption.

Main results

• ComputableInPolyTime.optionSome: construct an optional value.
• ComputableInPolyTime.optionIsSome: test a computed optional value.
• ComputableInPolyTime.optionGetD: read an option with a runtime fallback.
• ComputableInPolyTime.optionGetDWithInput, .optionElimWithInput: retain captured inputs.

theorem Turing.MultiTapeTM.ComputableInPolyTime.optionSome {α : Type} (enc : α ↪ List Bool) : ComputableInPolyTime some enc (encOption enc)

Construct an optional value with the standard option encoding.

theorem Turing.MultiTapeTM.ComputableInPolyTime.optionIsSome {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {value : α → Option β} (hvalue : ComputableInPolyTime value encA (encOption encB)) : ComputableInPolyTime (fun (a : α) => (value a).isSome) encA encBool

Test whether a computed option contains a value, without requiring a default value.

theorem Turing.MultiTapeTM.ComputableInPolyTime.optionGetD {α : Type} (enc : α ↪ List Bool) : ComputableInPolyTime (fun (p : Option α × α) => p.1.getD p.2) (encPair (encOption enc) enc) enc

Read an option with a fallback supplied as part of the input.

theorem Turing.MultiTapeTM.ComputableInPolyTime.optionGetDWithInput {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {value : α → Option β} {fallback : α → β} (hvalue : ComputableInPolyTime value encA (encOption encB)) (hfallback : ComputableInPolyTime fallback encA encB) : ComputableInPolyTime (fun (a : α) => (value a).getD (fallback a)) encA encB

Read a computed option with a computed fallback, using their shared value encoding.

theorem Turing.MultiTapeTM.ComputableInPolyTime.optionElimWithInput {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {γ : Type} {encC : γ ↪ List Bool} {value : α → Option β} {fallback : α → γ} {body : α → β → γ} (hvalue : ComputableInPolyTime value encA (encOption encB)) (hfallback : ComputableInPolyTime fallback encA encC) (hbody : ComputableInPolyTime (fun (p : α × β) => body p.1 p.2) (encPair encA encB) encC) : ComputableInPolyTime (fun (a : α) => (value a).elim (fallback a) (body a)) encA encC

Branch on a computed option, charging its full value and any captured original input.