読者です 読者をやめる 読者になる 読者になる

プログラムの意味

プログラミング

プログラムの操作的意味論だとプログラムの各種構造を数学の領域に移す関数を定義して、それを利用して数学的意味を決める。それは元のプログラムの構造と一貫性を持っているはずなので多分準同型写像になっていて、これを使って、最適化したプログラム同値性とかを測ることになる。

プログラムの意味する計算を厳密するという点では確かに必要なことではあるが、よく考えると、書きたい計算が数学の領域とかにあって、それをコーディングによって、実行可能な形に落とし込んだのがプログラムである。すると、この方向の準同型を考えることもできて、プログラムの意味付けを逆問題を解くことと考えることもできる。要するにプログラムの含意する計算を抽出する問題というのは、一意に解が定まるものではなくて、自然言語処理的なものにより文脈の情報を利用することになる。例を挙げると、

x + y

を Z で意味付けするか、 Z232 で意味付けするか、これは自明ではない。 *1

最適化ってプログラムの含意する計算を抽出する問題をどれだけうまく解けるかもかなり重要だと思う。ただ、これに都合よくしようと思うとできるだけ型を分けておく方がいいはずであるが、実際有効に活用するには依存型使ったり、不等式を上手に利用したりすることが必要で *2 一筋縄ではいかないものだなあ。

*1:たいていは前者にした方がいいが、ハッシュ関数とかは一部後者でないとまずいことになる

*2:不等式を制するものは距離空間を使う系の数学を制すると言っても過言ではないのでは