プログラミング言語の基礎概念

『プログラミング言語の基礎概念』 (五十嵐 淳 著、サイエンス社、2011 年 7 月刊) は、関数型言語 ML の一種である Objective Caml を題材に、プログラミング言語の意味論と型システム、そしてそれらの概念のあいだの数学的な関連を学ぶ教科書です。ライブラリ情報学コア・テキストの第 24 巻で、版元は難易度を入門と表示しています。大きな特徴は、証明を解答とする演習問題の正誤を、オンライン演習システムを使って Web 上で自動判定できる点で、版元のページのサポート情報から著者のサポートページと演習システムへ進めるようになっています。

3 部 10 章の構成、導出システム入門から型推論まで

本書は 3 部 10 章で構成されています。第 1 部の導出システム入門では、自然数の加算 / 乗算 / 比較を題材に推論規則と導出の記法を導入し、第 2 章でメタ定理と、数学的帰納法、構造帰納法、導出に関する帰納法、整礎帰納法による証明を扱います。第 2 部の ML の操作的意味論は、整数 / 真偽値式の評価と実行時エラーから始まり、let による定義と環境、fun 式と高階関数、静的有効範囲と関数閉包、再帰的定義、名前無し表現、リストとパターンマッチングへと進み、EvalML1 から EvalML5 までの導出システムを段階的に広げていきます。第 3 部の ML の型システムは、第 8 章の単純型システムと型安全性、第 9 章の let 多相を含む多相的型システム、第 10 章の方程式の抽出と一階の単一化による型推論アルゴリズムです。巻末にはさらに勉強したい人へ向けた案内と索引が置かれています。小さな言語に機能を一つずつ足しながら、そのたびに評価と型付けの規則を書き足していく構成と読めます。

プログラムの実行を証明として組み立てる操作的意味論

操作的意味論は、プログラムがどう実行されるかを推論規則の集まりとして定める方法です。ある式をある環境のもとで評価すると値が得られる、という判断を規則から導けたとき、その導出の木が実行結果の正しさの証拠になります。この見方の利点は、変数の有効範囲や クロージャ、パターンマッチといった機能の意味が、特定の処理系の実装に頼らず紙の上で一意に決まる点にあります。型システムを同じ規則の形で定めれば、型が付くプログラムは実行の途中で行き詰まらないという 型安全性 を、規則についての帰納法で示せるようになります。第 1 部で帰納法を独立して扱っているのは、後半でこうしたメタ定理を自分の手で確かめるための準備と読めます。また OCaml や Haskell の型推論は、第 10 章が扱う単一化に基づく型推論と同じ系統の考え方に立っており、型検査器がなぜその型を推論したのかを理解する手がかりにもなります。

前提知識と、処理系の使い方の本ではないという注意

推論規則の横線の記法や帰納法による証明に慣れていない人は、最初は戸惑うかもしれませんが、第 1 部は自然数の加算という単純な題材から記法そのものを導入しています。関数型プログラミング の経験があれば、第 2 部の高階関数や関数閉包の規則を、手元のコードの挙動と照らし合わせながら読み進められます。一方で、題材は Objective Caml でも、本書が扱うのは導出システムが対象とする小さな言語の定式化であり、処理系の使い方や実用的なプログラミング技法を学ぶ本ではありません。目次には構文解析やコード生成の章も置かれていないので、コンパイラーの作り方を一通り学びたい人は別の教科書を選ぶほうが目的に合います。2011 年の刊行ですが、扱う意味論と型システムの基礎は時間がたっても変わりにくい分野です。

型システムや型推論の論文を読めるようになりたい学生、あるいは普段使っている言語の型検査やスコープの規則を自分の言葉で説明できるようになりたいエンジニアにとって、本書は規則を書き、導出を組み、証明するという一連の作業を小さな言語で一通り経験できる一冊です。自分の導出を演習システムで判定してもらえるため、独学でも理解の手応えを確かめながら進められます。