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 = "A Possible Destruction Proof"
date = "2022-06-28"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a8g2c"]
forwardlinks = ["3a8g2b1", "3a8g2e"]
zettelid = "3a8g2d"
+++
The idea hinges on the following lemma, which talks about a path $p$
from nodes $n$ to $m$, an arbitrary predicate $\mathcal{P}$ which gets
simplified over that path into $\mathcal{P}'$, and finally an execution
along a path from $n$ with register state $R$ to $m$ with register state
$R'$. The execution of the predicate $P$ with $R'$ should give the same
result as executing the predicate $P'$ with the initial state $R'$.
```{=latex}
\begin{gather*}
\frac{\begin{array}{c}
S^p(\mathcal{P}) = \mathcal{P}' \\
n, R \overset{p}{\longrightarrow^*} m, R'
\end{array}}{
R', \mathcal{P} \Downarrow \lfloor b \rfloor \Longleftrightarrow R, \mathcal{P}'
\Downarrow \lfloor b \rfloor
}
\end{gather*}
```
However, in addition to that we will also have to prove the
generalisation of the simplification ([\#3a8g2b1]) to show that this has
been done along the path of execution.
The idea, finally, is that during the proof of semantic preservation, a
path $n\rightsquigarrow_p m$, as well as the execution along that path
$n, R\overset{p}{\longrightarrow^*} m, R'$ are remembered, so that once
a γ function is reached, the lemma above can be applied. It might also
be true that:
$$ \frac{n, R \overset{p}{\longrightarrow^*} m, R'}{n \rightsquigarrow_p m} $$
In which case the lemma can be simplified.
[\#3a8g2b1]: /zettel/3a8g2b1
|
