プログラム意味論

蓮尾 一郎(情報理工学系研究科コンピュータ科学専攻 講師)

プログラムを書いたら,とりあえず手頃な入力に対して結果が期待通りか確かめるだろう。これをプログラムのテストとよぶ。

しかし人命がかかっているような場合には,テストよりも気合の入った品質保証をしたくなる(試した以外の入力についてはどうなの?)。この気合を突き詰めたのが,プログラムの正しさに対する数学的証明である(プログラム検証とよぶ)。ともかく目標は,プログラムの正しさの証明を,あたかも幾何学の証明のように,与えることである。

プログラムを数学的議論の土俵に乗せてやるためには,プログラムの実行過程・実行結果・振る舞いを,数学的に扱える形で表現してやる必要がある。これがプログラムの意味論(セマンティクス)である。つまり,「このプログラムの意味は何か?」を論じる営みだ。

本当に現実に沿うならば,プログラムの振る舞い・意味は「実行時のiMac内部の電圧変化」だ。しかしこれでは複雑すぎて手に負えないので,もっと単純な数理モデルを考える。プログラム意味論の分野では,書き換え系,順序集合…とさまざまなモデルが用いられる。ともかく良い数理モデルとは,単純で,一般的で,本質をついていて,よって数学的に美しくて,しかもプログラム検証のために役に立つようなものである。このような,情報学的現象と数学の境目こそが,情報科学の中でも「セマンティクス屋さん」とよばれるわれわれの活躍(?)の場だ。

そもそも数学の歴史をひもとくと,物理学(自然現象の数理モデルをつくる営みだ)と,数学が手を携えて発展してきた。これに対してプログラム意味論は,情報科学的現象とともに発展するような,新しい数学の方向性を示唆していないだろうか。前者の「数理物理学」は(少なくとも初期においては)解析学を中心に発展してきたのに対し,後者の「数理情報学」では代数学と数理論理学が大きな役割を果たす。

筆者らは最近,2つの新しい計算パラダイム―具体的には量子計算ハイブリッドシステム(デジタルデータと物理的なアナログデータが混在する)―に対して,新しい数理モデルを与えた上で検証手法に結実させた。このさい,代数学(とくに圏論)などの抽象数学のコトバの一般性が,たとえば古典計算・量子計算に共通する本質を抽出するためにフル活用されている。