Finite choice of polynomial-time programs

Only the fixed finite control alphabet is enumerated. Every selected branch still executes its own uniform program on the complete runtime input.

def MIPRE.Cost.PolyTimeFun.chooseList {T : Type u_1} {α : Type u_2} {β : Type u_3} [Fintype T] [DecidableEq T] [SizedEncoding T] [SizedEncoding α] [SizedEncoding β] (select : PolyTimeFun α T) (branch : T → PolyTimeFun α β) (fallback : PolyTimeFun α β) : List T → PolyTimeFun α β

A finite decision chain, with a specified default outside its domain.

Equations

• select.chooseList branch fallback [] = fallback
• select.chooseList branch fallback (t :: ts) = ((MIPRE.Cost.PolyTimeFun.finiteFunction fun (u : T) => decide (u = t)).comp select).ite (branch t) (select.chooseList branch fallback ts)

theorem MIPRE.Cost.PolyTimeFun.chooseList_apply {T : Type u_1} {α : Type u_2} {β : Type u_3} [Fintype T] [DecidableEq T] [SizedEncoding T] [SizedEncoding α] [SizedEncoding β] (select : PolyTimeFun α T) (branch : T → PolyTimeFun α β) (fallback : PolyTimeFun α β) (ts : List T) (x : α) (h : select.toFun x ∈ ts) : (select.chooseList branch fallback ts).toFun x = (branch (select.toFun x)).toFun x

noncomputable def MIPRE.Cost.PolyTimeFun.choose {T : Type u_1} {α : Type u_2} {β : Type u_3} [Fintype T] [DecidableEq T] [SizedEncoding T] [SizedEncoding α] [SizedEncoding β] (select : PolyTimeFun α T) (branch : T → PolyTimeFun α β) (fallback : PolyTimeFun α β) : PolyTimeFun α β

Select a program over a fixed finite alphabet. The fallback is unreachable on encoded inputs and does not add any computability assumption.

Equations

• select.choose branch fallback = select.chooseList branch fallback Finset.univ.toList

@[simp]

theorem MIPRE.Cost.PolyTimeFun.choose_apply {T : Type u_1} {α : Type u_2} {β : Type u_3} [Fintype T] [DecidableEq T] [SizedEncoding T] [SizedEncoding α] [SizedEncoding β] (select : PolyTimeFun α T) (branch : T → PolyTimeFun α β) (fallback : PolyTimeFun α β) (x : α) : (select.choose branch fallback).toFun x = (branch (select.toFun x)).toFun x