From 1a6bcadfb62849943ad3252a87ebc51f09b62d5e Mon Sep 17 00:00:00 2001
From: Liam O'Connor <me@liamoc.net>
Date: Fri, 9 May 2025 18:16:57 +1000
Subject: [PATCH] add note on automata

---
 trees/loc-000K.tree                 | 27 +++++++++++++++++++++++++++
 trees/people/dfirsov.tree           |  6 ++++++
 trees/people/tuustalu.tree          |  6 ++++++
 trees/places/cpp13.tree             |  8 ++++++++
 trees/places/ru.tree                |  4 ++++
 trees/places/taltech.tree           |  4 ++++
 trees/refs/firsov-uustalu-2013.tree | 10 ++++++++++
 7 files changed, 65 insertions(+)
 create mode 100644 trees/loc-000K.tree
 create mode 100644 trees/people/dfirsov.tree
 create mode 100644 trees/people/tuustalu.tree
 create mode 100644 trees/places/cpp13.tree
 create mode 100644 trees/places/ru.tree
 create mode 100644 trees/places/taltech.tree
 create mode 100644 trees/refs/firsov-uustalu-2013.tree

diff --git a/trees/loc-000K.tree b/trees/loc-000K.tree
new file mode 100644
index 0000000..fa21c5b
--- /dev/null
+++ b/trees/loc-000K.tree
@@ -0,0 +1,27 @@
+\author{liamoc}
+\import{dt-macros}
+\title{Finite Automata via Matrices}
+\date{2025-05-08T09:10:02Z}
+\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.}
+\subtree{
+\taxon{Definition}
+\p{Define a finite state automaton over an alphabet #{\Sigma} as a tuple #{(N, \delta, I, F)} where: }
+\ul{
+		\li{#{N \in \mathbb{N}} is the number of states.}
+		\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.}
+		\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.}
+		\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.}
+	}
+}
+\p{
+	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 #{\lsquare\lsquare 1 \rsquare\rsquare} if the word is in the language and #{\lsquare\lsquare 0 \rsquare\rsquare} otherwise:
+	##{
+		w \in \mathcal{L} \;\;\Longleftrightarrow\;\; \delta^\ast(I,w) \cdot F = \lsquare\lsquare 1 \rsquare\rsquare
+	}
+	
+}
diff --git a/trees/people/dfirsov.tree b/trees/people/dfirsov.tree
new file mode 100644
index 0000000..d6f0b2c
--- /dev/null
+++ b/trees/people/dfirsov.tree
@@ -0,0 +1,6 @@
+\title{Denis Firsov}
+\taxon{Person}
+\meta{external}{https://firsov.ee}
+\meta{institution}{[[taltech]]}
+\meta{orcid}{0000-0003-1267-7898}
+\meta{position}{Researcher}
diff --git a/trees/people/tuustalu.tree b/trees/people/tuustalu.tree
new file mode 100644
index 0000000..d7f8562
--- /dev/null
+++ b/trees/people/tuustalu.tree
@@ -0,0 +1,6 @@
+\title{Tarmo Uustalu}
+\taxon{Person}
+\meta{external}{https://cs.ioc.ee/~tarmo/}
+\meta{institution}{[[ru]]}
+\meta{orcid}{0000-0002-1297-0579}
+\meta{position}{Professor}
diff --git a/trees/places/cpp13.tree b/trees/places/cpp13.tree
new file mode 100644
index 0000000..ef06553
--- /dev/null
+++ b/trees/places/cpp13.tree
@@ -0,0 +1,8 @@
+\import{conf-name-macros}
+\taxon{Conference}
+\meta{doi}{10.1145/3176245}
+\title{\conf-name{CPP '13}{3rd ACM SIGPLAN International Conference on Certified Programs and Proofs}}
+\date{2013-12}
+\meta{venue}{Melbourne, Victoria, Australia}
+\meta{doi}{10.1007/978-3-319-03545-1}
+\p{Colocated with [[aplas13]].}
diff --git a/trees/places/ru.tree b/trees/places/ru.tree
new file mode 100644
index 0000000..995fb48
--- /dev/null
+++ b/trees/places/ru.tree
@@ -0,0 +1,4 @@
+\title{Reykjavik University}
+\taxon{Institution}
+\meta{venue}{Reykjavik, Iceland}
+\meta{external}{https://www.ru.is}
diff --git a/trees/places/taltech.tree b/trees/places/taltech.tree
new file mode 100644
index 0000000..5f0bd31
--- /dev/null
+++ b/trees/places/taltech.tree
@@ -0,0 +1,4 @@
+\title{Talinn University of Technology}
+\taxon{Institution}
+\meta{venue}{Talinn, Estonia}
+\meta{external}{https://taltech.ee}
diff --git a/trees/refs/firsov-uustalu-2013.tree b/trees/refs/firsov-uustalu-2013.tree
new file mode 100644
index 0000000..fea3cd5
--- /dev/null
+++ b/trees/refs/firsov-uustalu-2013.tree
@@ -0,0 +1,10 @@
+\title{Certified Parsing of Regular Languages}
+\taxon{Reference}
+\meta{venue}{[[cpp13]]}
+\author{dfirsov}
+\author{tuustalu}
+\date{2013-12-11}
+\meta{doi}{10.1007/978-3-319-03545-1_7}
+\tag{refereed}
+
+\meta{source}{[Available from Denis' Website](https://firsov.ee/cert-reg/firsov-uustalu-cpp13.pdf)}
-- 
2.51.2