プログラムの意味
プログラムの操作的意味論だとプログラムの各種構造を数学の領域に移す関数を定義して、それを利用して数学的意味を決める。それは元のプログラムの構造と一貫性を持っているはずなので多分準同型写像になっていて、これを使って、最適化したプログラム同値性とかを測ることになる。
プログラムの意味する計算を厳密するという点では確かに必要なことではあるが、よく考えると、書きたい計算が数学の領域とかにあって、それをコーディングによって、実行可能な形に落とし込んだのがプログラムである。すると、この方向の準同型を考えることもできて、プログラムの意味付けを逆問題を解くことと考えることもできる。要するにプログラムの含意する計算を抽出する問題というのは、一意に解が定まるものではなくて、自然言語処理的なものにより文脈の情報を利用することになる。例を挙げると、
x + y
を Z で意味付けするか、 Z232 で意味付けするか、これは自明ではない。 *1
最適化ってプログラムの含意する計算を抽出する問題をどれだけうまく解けるかもかなり重要だと思う。ただ、これに都合よくしようと思うとできるだけ型を分けておく方がいいはずであるが、実際有効に活用するには依存型使ったり、不等式を上手に利用したりすることが必要で *2 一筋縄ではいかないものだなあ。
