Documentation

MIPRE.Foundations.Cost.SizeProgram

Encoded size as an ambient polynomial-time program #

source
noncomputable def MIPRE.Cost.PolyTimeFun.encodedSizeU (α : Type u_1) [SizedEncoding α] :
PolyTimeFun α Unary

Count the actual encoded tree size in unary. The output size is linear in the supplied encoding, including for arbitrary malformed object-level programs.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem MIPRE.Cost.PolyTimeFun.encodedSizeU_apply {α : Type u_1} [SizedEncoding α] (a : α) :
    (encodedSizeU α).toFun a = unary (esize a)