1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
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
|
