my forest
Merge branch 'main' of https://github.com/liamoc/forest
+71
-2
+5
-1
trees/dt/dt-0038.tree
+5
-1
trees/dt/dt-0038.tree
···
1
1
\import{dt-macros}
2
2
\author{liamoc}
3
3
\taxon{Theorem}
4
-
\p{#{+ : \mathbf{Cpo} \times \mathbf{Cpo} \rightarrow \mathbf{Cpo}} is a lawful [bifunctor](dm-000M).
4
+
\p{#{+ : \mathbf{Cpo} \times \mathbf{Cpo} \rightarrow \mathbf{Cpo}} is a lawful [bifunctor](dm-000M), that is:
5
+
\ol{
6
+
\li{ #{ (\lambda a. a) \times (\lambda b. b) = (\lambda x.x)} }
7
+
\li{ #{ (f_1 \circ g_1) \times (f_2 \circ g_2) = (f_1 \times f_2) \circ (g_1 \times g_2)} }
8
+
}
5
9
}
+1
-1
trees/dt/dt-003L.tree
+1
-1
trees/dt/dt-003L.tree
···
5
5
\p{With [the lifting operator](dt-003K), we can relate the lazy constructions like [product](dt-0021) and [sum](dt-0031) with [strict](dt-000K) constructions like [smash product](dt-003G) and [sum](dt-003H) via [isomorphism](dt-002E):
6
6
\ul{
7
7
\li{ #{A\contto B \simeq A_\bot \strictto B}}
8
-
\li{ #{A + B \;\; \simeq A_\bot \oplus B_\bot}}
8
+
\li{ #{A + B \simeq A_\bot \oplus B_\bot}}
9
9
\li{ #{(A \times B)_\bot \simeq A_\bot \otimes B_\bot } }
10
10
}
11
11
}
+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)}