A binary encoding of one-way liveness

The NFA scans a relation truth table using three groups of vertex counters. A two-bit encoding of four scanner letters adds a three-valued bit buffer.

inductive Complexity.FiniteAutomaton.BinaryLiveness.Letter : Type

Four letters encode matrix entries, row boundaries, and relation boundaries.

• bit : Bool → Letter
• row : Letter
• stop : Letter

@[instance_reducible]

instance Complexity.FiniteAutomaton.BinaryLiveness.instDecidableEqLetter : DecidableEq Letter

Equations

• Complexity.FiniteAutomaton.BinaryLiveness.instDecidableEqLetter = Complexity.FiniteAutomaton.BinaryLiveness.instDecidableEqLetter.decEq

def Complexity.FiniteAutomaton.BinaryLiveness.instDecidableEqLetter.decEq (x✝ x✝¹ : Letter) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Complexity.FiniteAutomaton.BinaryLiveness.instDecidableEqLetter.decEq (Complexity.FiniteAutomaton.BinaryLiveness.Letter.bit a) Complexity.FiniteAutomaton.BinaryLiveness.Letter.row = isFalse ⋯
• Complexity.FiniteAutomaton.BinaryLiveness.instDecidableEqLetter.decEq (Complexity.FiniteAutomaton.BinaryLiveness.Letter.bit a) Complexity.FiniteAutomaton.BinaryLiveness.Letter.stop = isFalse ⋯
• Complexity.FiniteAutomaton.BinaryLiveness.instDecidableEqLetter.decEq Complexity.FiniteAutomaton.BinaryLiveness.Letter.row (Complexity.FiniteAutomaton.BinaryLiveness.Letter.bit a) = isFalse ⋯
• Complexity.FiniteAutomaton.BinaryLiveness.instDecidableEqLetter.decEq Complexity.FiniteAutomaton.BinaryLiveness.Letter.row Complexity.FiniteAutomaton.BinaryLiveness.Letter.row = isTrue ⋯
• Complexity.FiniteAutomaton.BinaryLiveness.instDecidableEqLetter.decEq Complexity.FiniteAutomaton.BinaryLiveness.Letter.stop (Complexity.FiniteAutomaton.BinaryLiveness.Letter.bit a) = isFalse ⋯
• Complexity.FiniteAutomaton.BinaryLiveness.instDecidableEqLetter.decEq Complexity.FiniteAutomaton.BinaryLiveness.Letter.stop Complexity.FiniteAutomaton.BinaryLiveness.Letter.stop = isTrue ⋯

@[instance_reducible]

instance Complexity.FiniteAutomaton.BinaryLiveness.instFintypeLetter : Fintype Letter

Equations

• Complexity.FiniteAutomaton.BinaryLiveness.instFintypeLetter = Fintype.ofEquiv (Bool ⊕ Unit ⊕ Unit) Complexity.FiniteAutomaton.BinaryLiveness.Letter.proxyTypeEquiv

inductive Complexity.FiniteAutomaton.BinaryLiveness.State (n : ℕ) : Type

A row counter, a column counter, or the chosen target vertex.

• seek {n : ℕ} : Fin (n + 1) → State n
• scan {n : ℕ} : Fin (n + 1) → State n
• carry {n : ℕ} : Fin (n + 1) → State n

def Complexity.FiniteAutomaton.BinaryLiveness.instDecidableEqState.decEq {n✝ : ℕ} (x✝ x✝¹ : State n✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Complexity.FiniteAutomaton.BinaryLiveness.instDecidableEqState {n✝ : ℕ} : DecidableEq (State n✝)

Equations

• Complexity.FiniteAutomaton.BinaryLiveness.instDecidableEqState = Complexity.FiniteAutomaton.BinaryLiveness.instDecidableEqState.decEq

@[instance_reducible]

instance Complexity.FiniteAutomaton.BinaryLiveness.instFintypeState {n✝ : ℕ} : Fintype (State n✝)

Equations

• Complexity.FiniteAutomaton.BinaryLiveness.instFintypeState = Fintype.ofEquiv (Fin (n✝ + 1) ⊕ Fin (n✝ + 1) ⊕ Fin (n✝ + 1)) (Complexity.FiniteAutomaton.BinaryLiveness.State.proxyTypeEquiv n✝)

def Complexity.FiniteAutomaton.BinaryLiveness.rules {n : ℕ} : State n → Letter → Set (State n)

Scan the selected relation row and nondeterministically choose a true entry.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.FiniteAutomaton.BinaryLiveness.rules (Complexity.FiniteAutomaton.BinaryLiveness.State.carry i) x✝ = {Complexity.FiniteAutomaton.BinaryLiveness.State.carry i}
• Complexity.FiniteAutomaton.BinaryLiveness.rules x✝¹ x✝ = ∅

def Complexity.FiniteAutomaton.BinaryLiveness.machine (n : ℕ) : NFA Letter (State n)

The four-letter relation scanner; all row-selection states start and accept.

Equations

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

def Complexity.FiniteAutomaton.BinaryLiveness.columnWord (bits : ℕ → Bool) (k : ℕ) : List Letter

List the first k entries of a row in decreasing column order.

Equations

• Complexity.FiniteAutomaton.BinaryLiveness.columnWord bits k = List.map Complexity.FiniteAutomaton.BinaryLiveness.Letter.bit (List.map bits (List.range k).reverse)

def Complexity.FiniteAutomaton.BinaryLiveness.rowWord (n : ℕ) (bits : ℕ → Bool) : List Letter

A row marker followed by all entries in decreasing column order.

Equations

• Complexity.FiniteAutomaton.BinaryLiveness.rowWord n bits = Complexity.FiniteAutomaton.BinaryLiveness.Letter.row :: Complexity.FiniteAutomaton.BinaryLiveness.columnWord bits (n + 1)

def Complexity.FiniteAutomaton.BinaryLiveness.rowAt (rows : List (ℕ → Bool)) (i : ℕ) : ℕ → Bool

Read a row by its index, returning an all-false row outside the list.

Equations

• Complexity.FiniteAutomaton.BinaryLiveness.rowAt rows i = rows[i]?.getD fun (x : ℕ) => false

noncomputable def Complexity.FiniteAutomaton.BinaryLiveness.relationRows {n : ℕ} (R : BRel (Fin (n + 1))) : List (ℕ → Bool)

The truth-table rows of a relation in increasing source-vertex order.

Equations

• Complexity.FiniteAutomaton.BinaryLiveness.relationRows R = List.ofFn fun (i : Fin (n + 1)) (j : ℕ) => if hj : j < n + 1 then decide (R.holds i ⟨j, hj⟩) else false

noncomputable def Complexity.FiniteAutomaton.BinaryLiveness.code {n : ℕ} (R : BRel (Fin (n + 1))) : List Letter

Encode a relation by its marked rows followed by a relation terminator.

Equations

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

def Complexity.FiniteAutomaton.BinaryLiveness.letterBits : Letter → List Bool

Encode each scanner letter by a pair of bits.

Equations

• Complexity.FiniteAutomaton.BinaryLiveness.letterBits (Complexity.FiniteAutomaton.BinaryLiveness.Letter.bit a) = [false, a]
• Complexity.FiniteAutomaton.BinaryLiveness.letterBits Complexity.FiniteAutomaton.BinaryLiveness.Letter.row = [true, false]
• Complexity.FiniteAutomaton.BinaryLiveness.letterBits Complexity.FiniteAutomaton.BinaryLiveness.Letter.stop = [true, true]

def Complexity.FiniteAutomaton.BinaryLiveness.decode : Bool → Bool → Letter

Decode a pair of bits into a scanner letter.

Equations

• Complexity.FiniteAutomaton.BinaryLiveness.decode false x✝ = Complexity.FiniteAutomaton.BinaryLiveness.Letter.bit x✝
• Complexity.FiniteAutomaton.BinaryLiveness.decode true false = Complexity.FiniteAutomaton.BinaryLiveness.Letter.row
• Complexity.FiniteAutomaton.BinaryLiveness.decode true true = Complexity.FiniteAutomaton.BinaryLiveness.Letter.stop

def Complexity.FiniteAutomaton.BinaryLiveness.boundary {Q : Type} (S : Set Q) : Set (Q × Option Bool)

Original states at a codeword boundary, with no buffered bit.

Equations

• Complexity.FiniteAutomaton.BinaryLiveness.boundary S = {p : Q × Option Bool | p.1 ∈ S ∧ p.2 = none}

def Complexity.FiniteAutomaton.BinaryLiveness.binaryRules {Q : Type} (M : NFA Letter Q) : Q × Option Bool → Bool → Set (Q × Option Bool)

Buffer the first bit, then execute the transition named by the bit pair.

Equations

• Complexity.FiniteAutomaton.BinaryLiveness.binaryRules M (q, none) x✝ = {(q, some x✝)}
• Complexity.FiniteAutomaton.BinaryLiveness.binaryRules M (q, some a) x✝ = Complexity.FiniteAutomaton.BinaryLiveness.boundary (M.step q (Complexity.FiniteAutomaton.BinaryLiveness.decode a x✝))

def Complexity.FiniteAutomaton.BinaryLiveness.binaryMachine {Q : Type} (M : NFA Letter Q) : NFA Bool (Q × Option Bool)

Replace each transition of a four-letter NFA by two binary transitions.

Equations

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

noncomputable def Complexity.FiniteAutomaton.BinaryLiveness.binaryCode {n : ℕ} (R : BRel (Fin (n + 1))) : List Bool

The binary truth-table encoding of a relation.

Equations

• Complexity.FiniteAutomaton.BinaryLiveness.binaryCode R = List.flatMap Complexity.FiniteAutomaton.BinaryLiveness.letterBits (Complexity.FiniteAutomaton.BinaryLiveness.code R)

@[reducible, inline]

abbrev Complexity.FiniteAutomaton.BinaryLivenessState (n : ℕ) : Type

States of the binary liveness NFA for relations on n + 2 vertices.

Equations

• Complexity.FiniteAutomaton.BinaryLivenessState n = (Complexity.FiniteAutomaton.BinaryLiveness.State (n + 1) × Option Bool)

def Complexity.FiniteAutomaton.binaryLivenessNFA (n : ℕ) : NFA Bool (BinaryLivenessState n)

A binary NFA with 9 * (n + 2) states and exponential two-way deterministic cost.

Equations

• Complexity.FiniteAutomaton.binaryLivenessNFA n = Complexity.FiniteAutomaton.BinaryLiveness.binaryMachine (Complexity.FiniteAutomaton.BinaryLiveness.machine (n + 1))

noncomputable def Complexity.FiniteAutomaton.binaryLivenessCode {n : ℕ} (R : Alphabet (n + 2)) : List Bool

Encode a relation on n + 2 vertices as a binary word.

Equations

• Complexity.FiniteAutomaton.binaryLivenessCode R = Complexity.FiniteAutomaton.BinaryLiveness.binaryCode R