Efficient threshold search for logarithmic-gap MINKT -- definitions

This module gives the reverse direction of Fact 3.4 an explicit string algorithm. On a canonical MINKT code (x,1^t), it scans the thresholds 0,...,t, remembers the first one accepted by the supplied gap decider, and returns that threshold in unary.

The loop state is the canonical nested tuple

(base, counter, found, best).

The counter grows by one unary mark per iteration. Once found becomes true, best is frozen. The loop runs t+1 times, so threshold t is included.

def Complexity.GapMINKT.Logarithmic.Efficient.chooseHead (selector whenTrue whenFalse : List Bool) : List Bool

Select between two strings using the first bit of a selector. An empty selector yields the empty string.

Equations

• Complexity.GapMINKT.Logarithmic.Efficient.chooseHead selector whenTrue whenFalse = if selector.head? = some true then whenTrue else if selector.head? = some false then whenFalse else []

def Complexity.GapMINKT.Logarithmic.Efficient.sweepInit (base : List Bool) : List Bool

Initial threshold-sweep state (base,0,false,clock). The clock is the total fallback returned when no threshold is accepted.

Equations

• Complexity.GapMINKT.Logarithmic.Efficient.sweepInit base = Complexity.pair base (Complexity.pair [] (Complexity.pair [false] (Complexity.pairSnd base)))

def Complexity.GapMINKT.Logarithmic.Efficient.sweepRuler (base : List Bool) : List Bool

One more than the unary clock length, so the sweep checks thresholds from zero through the clock inclusively.

Equations

• Complexity.GapMINKT.Logarithmic.Efficient.sweepRuler base = false :: Complexity.pairSnd base

def Complexity.GapMINKT.Logarithmic.Efficient.sweepWidth (base : List Bool) : List Bool

A linear-width envelope for every threshold-sweep state.

Equations

• Complexity.GapMINKT.Logarithmic.Efficient.sweepWidth base = Complexity.pair (true :: true :: base) (Complexity.pair (true :: Complexity.pairSnd base) (true :: Complexity.pairSnd base))

def Complexity.GapMINKT.Logarithmic.Efficient.sweepStep (decide : List Bool → Bool) (state : List Bool) : List Bool

One ascending threshold-search step.

The input state is (base,counter,found,best). The decider is queried on the canonical raw pair (base,counter), best is set exactly at the first accepted counter, and the counter then grows by one unary mark.

Equations

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

def Complexity.GapMINKT.Logarithmic.Efficient.encodedTimeSearchEstimator (decide : List Bool → Bool) (base : List Bool) : List Bool

Unary output of the complete threshold sweep on an arbitrary base code.

Equations

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

def Complexity.GapMINKT.Logarithmic.Efficient.executableEstimator (decide : List Bool → Bool) : Estimator

The numerical estimator represented by the unary sweep output on canonical MINKT codes.

Equations

• Complexity.GapMINKT.Logarithmic.Efficient.executableEstimator decide inst = (Complexity.GapMINKT.Logarithmic.Efficient.encodedTimeSearchEstimator decide inst.encode).length