blob: 0b05b13a4bab8b46d6e3bf2ccf15ef56578f1db9 (
plain)
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
|
+++
title = "Proof of translation validation theorem"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a7b"]
forwardlinks = ["3a7d"]
zettelid = "3a7c"
+++
The proof follows from the fact that the translation to the abstract
interpretation is semantics preserving. As the abstract interpretation
of both languages is equal, this means that
$$ \frac{\Sigma_s, s \downarrow_S \Sigma_s' \quad \Sigma_t, t \downarrow_T\Sigma_t' \quad s \sim t \quad \Sigma_s \sim \Sigma_t}{\Sigma_s' \sim \Sigma_t'}$$
This is because:
$$ \frac{\Sigma_s, \alpha \downarrow_{\mathcal{A}} \Sigma_s' \quad \Sigma_t,\alpha' \downarrow_{\mathcal{A}} \Sigma_t' \quad \alpha \sim \alpha' \quad\Sigma_s \sim \Sigma_t}{\Sigma_s' \sim \Sigma_t'} $$
And the latter can be used because :
$$ s \rightarrow_s \alpha \land t \rightarrow_t \alpha' $$
We can therefore get the following:
$$ \cfrac{\cfrac{}{\alpha \sim \alpha'} \quad \cfrac{\cfrac{}{\Sigma_s, s\downarrow_S \Sigma_s'} \quad \cfrac{}{s \rightarrow_s \alpha}}{\Sigma_s, \alpha\downarrow_{\mathcal{A}} \Sigma_s'} \quad \cfrac{\cfrac{}{\Sigma_t, t\downarrow_T \Sigma_t'} \quad \cfrac{}{t \rightarrow_t \alpha'}}{\Sigma_t,\alpha' \downarrow_{\mathcal{A}} \Sigma_t'} \quad \cfrac{}{\Sigma_s \sim\Sigma_t}}{\Sigma_s' \sim \Sigma_t' \land s \sim t} $$
|
