「コンパイラ」とfull abstraction
あまり抽象的な与太話ばかりしていてもしようがないので、ちょっとだけ(素朴な)テクニカルな質問を。ETのホームページによると、等価変換は意味(semanticsないしdenotationと理解します)を保存するとありますが、一般に「コンパイラ」(高水準言語から低水準言語への変換器)はdenotation(の等価性)を保存しません(full abstractionが成立しない)。関数など、入力を受け取って出力を返すものは、通常は「等価な入力に対して等価な出力を返せば等価」と定義されますが、コンパイルすると値域定義域が拡大してしまうためです。そうすると、コンパイラを(上述の定義での)等価変換で表現することは不可能ということにもなってしまいますが、この問題はどう回避されているのでしょうか…?