1 files changed, 44 insertions, 0 deletions
diff --git a/content/zettel/3a8g5d.md b/content/zettel/3a8g5d.md
new file mode 100644
index 0000000..00b4d44
--- /dev/null
+++ b/content/zettel/3a8g5d.md
@@ -0,0 +1,44 @@
++++
+title = "Why this proof is tricky"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3a8g5c"]
+forwardlinks = ["3a8g5b", "3a8g5e"]
+zettelid = "3a8g5d"
++++
+
+However, one problem is that this proof is quite difficult, as there are
+many independent parts that need to be combined to show the correctness
+of the algorithm. One example is that the $t$ function, which translates
+a path expression to a predicate is completely independent from the
+correctness argument, which involves a separate function $\sigma$.
+Combining these parts all requires quite a lot of proofs of correctness
+between the different functions and how these interact with each other.
+
+For example, proving the path property ([\#3a8g5b]) requires
+interactions between $t$ and $\sigma$ already, proving that the
+predicates obtained from translating a list of paths compared to the
+regex are equivalent, which is not straightforward.
+
+In addition to that, even proving that the path expressions are indeed
+correct and follow the correctness property is non-trivial, because the
+algorithm by Tarjan \[1\] was followed, which uses Gaussian elimination
+for matrices to solve the path equation.
+
+<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>
+
+  [\#3a8g5b]: /zettel/3a8g5b
+  [10.1145/322261.322273]: https://doi.org/10.1145/322261.322273