blob: 703fcb9d1672902ddafcf764b394d3fd22d1789a (
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
|
+++
title = "New semantics to prove equivalent to RTL and HTL"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3c3b2"]
forwardlinks = []
zettelid = "3c3b3"
+++
Maybe new semantics are needed to prove the equivalence between RTL
$\to$ RTLBlock and RTLPar $\to$ HTL. These would have to then be proven
equivalent to the current semantics, so that finally each translation is
formally proven.
However, if it is possible then the same semantics could be used to
prove the equivalence between the languages, which might be more tricky
but would not need another equivalent semantics. It probably needs to be
investigated first to be able to tell which technique would be faster
and simpler.
It seems that from RTLPar to HTL there should not be such a big gap in
the semantics, however, it does need to be shown that no states will be
overwritten and therefore every state will still be reachable. It might
therefore be necessary to do some renaming to ensure this property
before continuing.
|
