my forest
1\author{liamoc}
2\import{dt-macros}
3\title{Finite Automata via Matrices}
4\date{2025-05-08T09:10:02Z}
5\p{This technique is almost certainly folklore, but I first saw it in [[dfirsov]] and [[tuustalu]]'s [paper](firsov-uustalu-2013), which uses it to formalise and prove correct a regex matcher in Agda.}
6\subtree{
7\taxon{Definition}
8\p{Define a finite state automaton over an alphabet #{\Sigma} as a tuple #{(N, \delta, I, F)} where: }
9\ul{
10 \li{#{N \in \mathbb{N}} is the number of states.}
11 \li{#{\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.}
12 \li{#{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.}
13 \li{#{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.}
14 }
15}
16\p{
17 Running an NFA #{(N, \delta, I, F)} on a word #{x_0x_1x_2\dots
18 } 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:
19 ##{ \begin{array}{lcl}
20 \delta^\ast(X, x_0x_1x_2\dots) & = & X \cdot \delta(x_0) \cdot \delta (x_1) \cdot \delta(x_2) \cdot \cdots \\
21 \end{array}}
22 Start from #{I} and multiply #{F} at last and the result will be #{\lsquare\lsquare 1 \rsquare\rsquare} if the word is in the language and #{\lsquare\lsquare 0 \rsquare\rsquare} otherwise:
23 ##{
24 w \in \mathcal{L} \;\;\Longleftrightarrow\;\; \delta^\ast(I,w) \cdot F = \lsquare\lsquare 1 \rsquare\rsquare
25 }
26
27}