Quantification Operations for DFAs

This file implements existential (∃) and universal (∀) quantification over automata, which is fundamental for building first-order formulas in automata-based decision procedures.

Main Components

• Quantification Operator Type: Custom type implementing operators ∃ and ∀
• Reachability Analysis: Finding states reachable with leading zeros
• Determinization: Converting NFA to DFA
• Quantification Operations: ∃ and ∀ operators over an automaton

Theory

Given a DFA M over variables [x₁, x₂, ..., xₙ] and a variable xᵢ:

• ∃xᵢ. M: Creates a DFA over [x₁, ..., xᵢ₋₁, xᵢ₊₁, ..., xₙ] that accepts when there exists some value for xᵢ that makes M accept
• ∀xᵢ. M: Creates a DFA that accepts when M accepts for all values of xᵢ

Implementation Strategy

1. Remove Quantified Variable: Remove xᵢ's track from the alphabet
2. Non-Determinization: For each input on remaining variables, consider all possible values for xᵢ, this creates an NFA
3. Find All Initial States: Find all states reachable with leading zeros from the initial state
4. Determinization: Convert the NFA back to DFA
5. For ∀: Use De Morgan's law: ∀x.φ ≡ ¬∃x.¬φ

Quantification Operator Type

inductive quant_op : Type

Quantification operators for automata.

• exists : quant_op
• for_all : quant_op

Reachability Analysis

These functions find all states reachable from starting states by reading zero prefixes.

def process_symbol {Input : Type} (f : ℕ → Input → List ℕ) (current_states : List ℕ) (symbol : Input) (visited : List ℕ) : List ℕ

Return all states reachable from currentStates using symbol and f

Equations

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

@[irreducible]

def find_initial_states {Input : Type} (transition_function : ℕ → Input → List ℕ) (zero : Input) (current_states : List ℕ) (num_possible_states : ℕ) (states : List ℕ) : List ℕ

Finds all states reachable from the initial state with one or more consecutive zeros.

Parameters

• transition_function: Transition function returning a list of all reachable states for a state and a symbol
• zero: The zero symbol
• current_states: List of current initial states to visit
• num_possible_states: Maximum number of possible initial states
• states: Already visited states

Equations

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

NFA Determinization

After removing a variable, we get an NFA (non-deterministic finite automaton). We use powerset construction to convert it to a DFA, with memoization for efficiency.

structure determinize_state (Input : Type) : Type

State for the determinization algorithm with memoization.

• visited : Std.HashSet (List ℕ)
• transitions : List ((List ℕ × Input) × List ℕ)

@[irreducible]

def determinize_with_memo {Input : Type} [DecidableEq Input] (transition_function : ℕ → Input → List ℕ) (alphabet : List Input) (current_state : List ℕ) (num_possible_states : ℕ) (state : determinize_state Input) : determinize_state Input

Determinization using depth-first search with memoization.

Algorithm (Powerset Construction)

1. Start with a set of NFA states (represented as List Nat)
2. For each input symbol, compute all possible next states
3. Each set of NFA states becomes a single DFA state
4. Recursively process newly discovered state sets
5. Use memoization to avoid recomputing transitions

Parameters

• transition_function: NFA transition function (state → input → list of states)
• alphabet: Input alphabet
• current_state: Current set of NFA states (forms one DFA state)
• num_possible_states: Bound on recursion depth (prevents infinite loops)
• state: Memoization state (visited sets and cached transitions)

Returns

Pair of (all transitions discovered, updated memoization state)

Equations

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

def determinize_memo {Input : Type} [DecidableEq Input] (transition_function : ℕ → Input → List ℕ) (alphabet : List Input) (initial_state : List ℕ) (max_states : ℕ) : determinize_state Input

Public interface for determinization with memoization.

Parameters

• transition_function: NFA transition function
• alphabet: Input alphabet
• initial_state: Starting set of NFA states
• max_states: Upper bound on number of states (usually 2^n for powerset)

Returns

List of all transitions in the determinized DFA, where each transition is ((source_state_set, input_symbol), target_state_set)

Equations

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

def all_binary_combinations_qt : ℕ → List (List B2)

Equations

• all_binary_combinations_qt 0 = [[]]
• all_binary_combinations_qt n.succ = List.flatMap (fun (combo : List B2) => [B2.zero :: combo, B2.one :: combo]) (all_binary_combinations_qt n)

Quantification Implementation

def quant' (M : DFA_extended (List B2) ℕ) (zero : List B2) (var : Char) (alphabet_vars : List (List B2)) : DFA_extended (List B2) (List ℕ)

Existential quantification over a variable.

Parameters

• M: Original DFA
• zero: Zero symbol for handling leading zeros
• var: Variable to quantify over
• alphabet_vars: All possible values for the quantified variable

Algorithm

1. Remove variable from input

2. Create NFA

3. Handle leading zeros

4. Determinize

5. Accepting states

Equations

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

def quant (M : DFA_extended (List B2) ℕ) (var : Char) (op_type : quant_op) : DFA_extended (List B2) ℕ

Quantification operation (public interface).

Implements both existential (∃) and universal (∀) quantification.

• ∃x. M: Accepts input if there exists a value for x making M accept
• ∀x. M: Accepts input if M accepts for all values of x

Parameters

• M1: DFA to quantify over
• zero: Zero symbol for leading zeros
• var: Variable to quantify
• op_type: Quantifier type (exists or for_all)
• alphabet_vars: Possible values for quantified variable

Returns

DFA_extended with Nat states representing the quantified formula

Equations

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