my forest
add note on automata
+65
+27
trees/loc-000K.tree
+27
trees/loc-000K.tree
···
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
+
}
+6
trees/people/dfirsov.tree
+6
trees/people/dfirsov.tree
+6
trees/people/tuustalu.tree
+6
trees/people/tuustalu.tree
+8
trees/places/cpp13.tree
+8
trees/places/cpp13.tree
···
1
+
\import{conf-name-macros}
2
+
\taxon{Conference}
3
+
\meta{doi}{10.1145/3176245}
4
+
\title{\conf-name{CPP '13}{3rd ACM SIGPLAN International Conference on Certified Programs and Proofs}}
5
+
\date{2013-12}
6
+
\meta{venue}{Melbourne, Victoria, Australia}
7
+
\meta{doi}{10.1007/978-3-319-03545-1}
8
+
\p{Colocated with [[aplas13]].}
+4
trees/places/ru.tree
+4
trees/places/ru.tree
+4
trees/places/taltech.tree
+4
trees/places/taltech.tree
+10
trees/refs/firsov-uustalu-2013.tree
+10
trees/refs/firsov-uustalu-2013.tree
···
1
+
\title{Certified Parsing of Regular Languages}
2
+
\taxon{Reference}
3
+
\meta{venue}{[[cpp13]]}
4
+
\author{dfirsov}
5
+
\author{tuustalu}
6
+
\date{2013-12-11}
7
+
\meta{doi}{10.1007/978-3-319-03545-1_7}
8
+
\tag{refereed}
9
+
10
+
\meta{source}{[Available from Denis' Website](https://firsov.ee/cert-reg/firsov-uustalu-cpp13.pdf)}