A total binary interface to the rational hitting-list generator

The input is true^n ++ [false] ++ true^s, with both parameters positive. Every other string returns the empty string. The successful output is exactly the source's encoding of its rational matrix hitting list.

def Complexity.RationalHitting.binaryInput (n s : ℕ) : List Bool

The binary form of the source's two unary parameters.

Equations

• Complexity.RationalHitting.binaryInput n s = List.replicate n true ++ false :: List.replicate s true

inductive Complexity.RationalHitting.InputState : Type

States recognizing two nonempty unary blocks separated by one false bit.

• start : InputState

  No input has been read.

• left : InputState

  At least one bit of the first unary block has been read.

• separator : InputState

  The separator has just been read.

• right : InputState

  At least one bit of the second unary block has been read.

• dead : InputState

  The input is malformed.

@[instance_reducible]

instance Complexity.RationalHitting.instDecidableEqInputState : DecidableEq InputState

Equations

• Complexity.RationalHitting.instDecidableEqInputState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Complexity.RationalHitting.instFintypeInputState : Fintype InputState

The validator uses five concrete states.

Equations

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

def Complexity.RationalHitting.inputDFA : DFA Bool InputState

A five-state validator for the literal source input format.

Equations

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

@[instance_reducible]

instance Complexity.RationalHitting.decidableInput : DecidablePred fun (x : List Bool) => x ∈ inputDFA.accepts

The format check is computable by the finite validator.

Equations

• Complexity.RationalHitting.decidableInput w = Complexity.RationalHitting.decidableInput._aux_1 w

def Complexity.RationalHitting.inputVariables (w : List Bool) : ℕ

Read the first unary block.

Equations

• Complexity.RationalHitting.inputVariables w = (List.takeWhile id w).length

def Complexity.RationalHitting.inputSize (w : List Bool) : ℕ

Read the remaining unary size, excluding the separator.

Equations

• Complexity.RationalHitting.inputSize w = w.length - Complexity.RationalHitting.inputVariables w - 1

def Complexity.RationalHitting.hittingGenerator (w : List Bool) : List Bool

Generate an encoded hitting list, returning empty output on malformed inputs.

Equations

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