Chapter 10

2.4 なぜ数学的モデルが必要か?

さのたけと
さのたけと
2021.05.05に更新

あなたはプログラマとして,あなたが使うプログラミング言語の構文や文法を熟知しているはずだ.これらは通常,言語仕様の冒頭部分で形式的な表記として記述されている.しかし言語の意味,または意味論 (semantics) は,記述するのがずっと難しい.それはより多くのページを要し,形式的に書かれていることは稀だし,完全であることはほぼない.そのため,"言語弁護士" たちの間では常に議論が行われており,言語基準の細かな点を解説した本を作り出す "家内工業" が乱立している.

言語の意味論を記述するための形式的なツールはあるが,それは複雑であるために,ほとんどの場合は簡略化された学術言語に対して使用されており,現実の巨大なプログラミング言語に対しては使用されていない.そのようなツールの一つである 操作的意味論 (operational semantics) は,プログラムの実行の仕組みを説明する.それは形式化された理想的なインタープリタを定義する.C++ などの産業用言語の意味論は通常「抽象マシン」によって非形式的な操作推論を用いて記述される[1]

問題は,操作的意味論を用いてプログラムに関する何かを証明することは非常に難しいということだ.プログラムの何らかの性質を示すためには,本質的には,理想化されたインタープリタを通してプログラムを "実行" しなければならないのだ.

プログラマが正しさの形式的な証明をしないことは問題ではない.私たちは常に正しいプログラムを書いていると "考えて" いる.「さて,何行かコードを書いて,何が起こるか見てみよう」と言ってキーボードに向かう人はいない.私たちは,自分が書いたコードが特定の動作を行い,望ましい結果が得られると考える.そうならないときには,たいていとても驚く.つまり,私たちは書いたプログラムについて様々な推論をしている.頭の中でインタプリタを走らせているのだ.ただし,人間はプログラム内の変数をすべて追うことはできない.コンピュータはプログラムを実行するのが得意だが,人間はそうではない.もし得意ならばコンピュータは必要ないのだから.

しかし,別の方法がある.それは 表示的意味論 (denotational semantics) と呼ばれ,数学に基づいている.表示的意味論では,全てのプログラミング構造物は数学的な解釈が与えられる.そのために,プログラムの性質を証明したければ,数学の定理を証明すれば良いのだ.定理を証明するのは難しいことだと思うかも知れないが,実際には,我々人類は数千年に渡って数学的な道具を作ってきたのであって,そこには豊富な知識の蓄積がある.もっと言えば,プロの数学者たちが証明する定理と違って,プログラミングにおいて現れる問題は通常簡単なものなのだ.

Haskell は表示的意味論と相性がいい.例として階乗関数を考えてみよう:

fact n = product [1..n]

ここで product 関数は,リスト内の要素を全て掛ける.これは数学のテキストに出てくる階乗の定義にそっくりだ.C の場合と比べてみよう:

int fact(int n) {
    int i;
    int result = 1;
    for (i = 2; i <= n; ++i)
        result *= i;
    return result;
}

これ以上の説明が必要だろうか?

分かった,はじめにこれはチートだったと認めなければならない.そもそも階乗関数には数学的な表示がある.鋭い読者は問うかも知れない:キーボードから文字を読み取ったり,ネットワーク上でパケットを送ったりすることの数学的なモデルは何か?と.とても長い間,この妙な問いにはやたらと複雑な説明をつけて答えることしかできなかった.表示的意味論は,現実的に有用なプログラムを書く上で必須となる多くのタスクに対して,操作的意味論では簡単に解決できるようなものに対しても,最適ではないように思われた.そこに圏論がブレイクスルーをもたらした.Eugenio Moggi は,計算効果 (computational effect) はモナド (monad) によって表現できることを発見した.この発見が重要だったのは,表示的意味論に命を与え,純粋関数型プログラムをより有用なものにしただけでなく,従来のプログラミングに対しても新しい光をもたらしたのだ.モナドについては,圏論の準備が進んでから再び解説しよう.

プログラミングの数学的モデルが存在することのメリットの一つは,ソフトウェアの正当性に関して形式的な証明を行うことができることだ.あなたが一般消費者向けのソフトウェアを書いているなら大して重要なことと思われないかも知れないが,失敗のコストが莫大だったり,人命に関わるようなプログラミングの分野もある.そこまで行かなくても,健康システムのウェブアプリケーションを書くような状況でも,Haskell の標準ライブラリに備わっている関数やアルゴリズムが正当性の保証付きだという事実はきっとありがたく感じられるだろう.

(和訳:@taketo1024

脚注
  1. 訳注:訳者はこの分野のことは何も知らないので,不自然な訳になっている可能性が高い. ↩︎