Total finite query programs

A fixed finite data table is an actual closed ambient program, total on every tree and polynomial in the size of that tree. The constants depend on the table; this lemma makes no uniform polynomial claim about its construction.

theorem MIPRE.Cost.PolyTimeFun.bits_prefix_unique (a b : Data) (xs ys : BitStr) (h : a.toBits ++ xs = b.toBits ++ ys) : a = b ∧ xs = ys

noncomputable def MIPRE.Cost.PolyTimeFun.treeEq : PolyTimeFun (Data × Data) Bool

Equality of arbitrary trees, through their injective serialization.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.Cost.PolyTimeFun.treeEq_apply (p : Data × Data) : treeEq.toFun p = decide (p.1 = p.2)

noncomputable def MIPRE.Cost.PolyTimeFun.treeTail : PolyTimeFun Data Data

A tree's right child, with a fixed default for a leaf.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.Cost.PolyTimeFun.treeTail_cons (a b : Data) : treeTail.toFun (a.cons b) = b

noncomputable def MIPRE.Cost.PolyTimeFun.treeHead : PolyTimeFun Data Data

A tree's left child, with a fixed default for a leaf.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.Cost.PolyTimeFun.treeHead_cons (a b : Data) : treeHead.toFun (a.cons b) = a

noncomputable def MIPRE.Cost.PolyTimeFun.treePair : PolyTimeFun (Data × Data) Data

Pair two raw trees.

Equations

• MIPRE.Cost.PolyTimeFun.treePair = MIPRE.Cost.PolyTimeFun.ofEncodeEq (fun (p : MIPRE.Cost.Data × MIPRE.Cost.Data) => p.1.cons p.2) MIPRE.Cost.PolyTimeFun.treePair._proof_1

@[simp]

theorem MIPRE.Cost.PolyTimeFun.treePair_apply (p : Data × Data) : treePair.toFun p = p.1.cons p.2

noncomputable def MIPRE.Cost.PolyTimeFun.finiteTable (f : Data → Data) : List Data → PolyTimeFun Data Data

First matching key, or nil. The function assigned to keys need not itself be computable: only its finitely many values become constants in the program.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Cost.PolyTimeFun.finiteTable f [] = MIPRE.Cost.PolyTimeFun.const MIPRE.Cost.Data.nil

theorem MIPRE.Cost.PolyTimeFun.finiteTable_apply_of_mem (f : Data → Data) (xs : List Data) (d : Data) (hd : d ∈ xs) : (finiteTable f xs).toFun d = f d

noncomputable def MIPRE.Cost.PolyTimeFun.finiteFunction {α : Type u_1} {β : Type u_2} [Fintype α] [SizedEncoding α] [SizedEncoding β] (f : α → β) : PolyTimeFun α β

Every fixed function on a finite, faithfully encoded domain has a concrete polynomial-time table program. No uniform bound in the domain's cardinality is asserted.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.Cost.PolyTimeFun.finiteFunction_apply {α : Type u_1} {β : Type u_2} [Fintype α] [SizedEncoding α] [SizedEncoding β] (f : α → β) (a : α) : (finiteFunction f).toFun a = f a