1 files changed, 50 insertions, 0 deletions
diff --git a/content/zettel/3a8g5a.md b/content/zettel/3a8g5a.md
new file mode 100644
index 0000000..58c1326
--- /dev/null
+++ b/content/zettel/3a8g5a.md
@@ -0,0 +1,50 @@
++++
+title = "Proof of path expressions"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3a8g5"]
+forwardlinks = ["3a8g5b"]
+zettelid = "3a8g5a"
++++
+
+The base of the proof relies on the path expressions being correct. What
+does this mean?
+
+Well, there are various correctness properties one could try and come up
+with. The base structure of path expressions is a regex, which can match
+a possible path \[1\]. Therefore, the basic correctness property of the
+path expressions is that it should only match paths that are actually
+valid:
+
+$$ \forall a p b R_{a \rightarrow b}, p \in \sigma(R_{a \rightarrow b}) \implies\textit{path}\ a\ p\ b $$
+
+where $p$ is a path from $a$ to $b$ and $R$ is a path expression from
+$a$ to $b$. $\sigma$ is a function that returns the set of all the paths
+that were matched.
+
+However, that is not the correctness theorem that is needed during the
+proof. In actuality, we want to ensure that all the possible paths from
+$a$ to $b$ will be matched by the path expression $R$, which leads to
+the following correctness property that needs to be proven:
+
+$$ \forall a p b R_{a \rightarrow b}, \textit{path}\ a\ p\ b \implies p \in\sigma(R_{a \rightarrow b}) $$
+
+This allows us to show that if there is a certain path in the graph,
+that it will definitely be in the set of $\sigma(R)$.
+
+<div id="refs" class="references csl-bib-body" markdown="1">
+
+<div id="ref-tarjan81_fast_algor_solvin_path_probl" class="csl-entry"
+markdown="1">
+
+<span class="csl-left-margin">\[1\]
+</span><span class="csl-right-inline">R. E. Tarjan, “Fast algorithms for
+solving path problems,” *J. ACM*, vol. 28, no. 3, pp. 594–614, Jul.
+1981, doi: [10.1145/322261.322273].</span>
+
+</div>
+
+</div>
+
+  [10.1145/322261.322273]: https://doi.org/10.1145/322261.322273