Finite Automata via Matrices [loc-000K]

This technique is almost certainly folklore, but I first saw it in Denis Firsov and Tarmo Uustalu's paper, which uses it to formalise and prove correct a regex matcher in Agda.

Definition

Define a finite state automaton over an alphabet \Sigma as a tuple (N, \delta , I, F) where:

  • N \in \mathbb {N} is the number of states.
  • \delta : \Sigma \rightarrow N \times N is the transition function. Here \delta (a) gives a boolean matrix M where M_{ij} = 1 iff state j is a successor of state i for the symbol a. As \Sigma is finite this could also be viewed as a three-dimensional tensor.
  • I : 1 \times N is a row vector specifying the initial states, where element I_{1k} is 1 iff state k is an initial state.
  • F : N \times 1 is a column vector specifying the final states, where element I_{k1} is 1 iff state k is a final state.

Running an NFA (N, \delta , I, F) on a word x_0x_1x_2\dots from a starting set of states X is the same as the product of X (interpreted as a row vector) with each matrix for each symbol in the word: \begin {array}{lcl} \delta ^\ast (X, x_0x_1x_2\dots ) & = & X \cdot \delta (x_0) \cdot \delta (x_1) \cdot \delta (x_2) \cdot \cdots \\ \end {array} Start from I and multiply F at last and the result will be [[ 1 ]] if the word is in the language and [[ 0 ]] otherwise: w \in \mathcal {L} \;\;\Longleftrightarrow \;\; \delta ^\ast (I,w) \cdot F = [[ 1 ]]