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
45
46
47
48
49
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
|
