2008-03-01 リンデンバウム/エルブランの原理 プログラム意味論 論理 リンデンバウム代数やエルブランの定理からの教訓としての指導原理。 構文構造からモデルを作れる。 モデル全体に十分に強い同値関係を入れれば、構文構造から作ったモデルを代表元にとれる。 したがって、妥当性検証は、構文構造から作ったモデルに対して行えばよい。 さらにはおそらく、 「構文構造から作ったモデル」は、ある空間(スペクトル、モジュライ)の点である。 命題は、この空間上の関数である。 したがって、妥当性検証とは、この空間上での関数値を求める問題である。 ここまで含めると、リンデンバウム/エルブラン/ストーンの原理かな。参考: 伝統的エルブラン理論 - 檜山正幸のキマイラ飼育記 メモ編 リンデンバウム代数のスペクトルとモデル - 檜山正幸のキマイラ飼育記 メモ編