型推論に関わる論理の概念と用語 その6：substitutionの記法

とりあえず、「型推論」を「プログラマに代わって自動的に最適(?)な型宣言／型注釈を書いてくれる機能」と捉えることにしましょう。その型推論の処理のなかで単一化と呼ばれる計算が行われます。単一化（ユニフィケーション）は、型推論に限らず、式やデータ構造のパターンマッチングとして幅広く利用できる手法です。

単一化ではsubstitutionという概念を使うのですが、これがなかなかにややこしいのです。そこで、substitutionについて説明しようと思い立ったのですが、今日は記法の紹介だけ。

シリーズ目次：

1. その1
2. その2
3. その3
4. その4
5. その5
6. その6
7. 番外（型理論ってば）

---

まず、substitutionの訳語で悩みますね。「置換の圏から代入の圏へ」では、permutationを置換と呼んだ都合から、substitutionは代入と呼びました。実際、代入という訳語もよく使われています。僕の感覚だと、代入はメモリ領域への破壊的書き込みの感じがするのですが、それをあまり気にせずに今回は「代入」を使うことにします。

代入とは、変数の置き換え操作のことなんですが、代入の書き表し方から紹介します。この書き方（記法）がまたすごくイッパイあるんですよね。

x, yを変数としてE, Fは式だとします。式としては、例えば 2*x + y + 1 とかの算術式を思い浮かべるのが分かりやすいでしょう。E, Fには変数x, yが入ってもいいし、2 + 3 のような変数を含まない式でもいいし、x, y 以外の変数、例えばtを含んでもかまいません。

僕が一番多く見る記法は、{E/x, F/y} のようにスラッシュを使った書き方です。これはもちろん「変数xを式Eで置き換え、変数yを式Fで置き換える」という意味です。代入は一種の作用素（オペレーター）と考えて、「式 2*x + y + 1 に、代入 { (2 + 3)/x, (t + 1)/y} を作用させると 2*(2 + 3) + (t + 1) + 1 になる」のような言い方をします。

ただ、(2 + 3)/x と書くとスラッシュが割り算のように見えてしまいます。{ '2 + 3'/x, 't + 1'/y} とクォートすればいいでしょうか。でも、代入を文字列置換だと誤解されるのも困ります。
「式 '2*x + y + 1' に、代入 { '2 + 3'/x, 't + 1'/y} を作用させると '2*2 + 3 + t + 1 + 1'」
ではありません。式のテキスト表現じゃなくて、構文解析した後のAST（abstract syntax tree）のようなデータ構造を考えて、その構造に対する置換操作なんですよね。

僕が単一化についてお勉強した(したのか？)本はJ.W.ロイド(著)の『論理プログラミングの基礎』（佐藤雅彦, 森下真一 (翻訳)）という本なのですが：

論理プログラミングの基礎 (ソフトウェア サイエンス シリーズ)

この本では、{x/E, y/F} という記法が使われていました。変数がスラッシュの前に置かれるんですね。一方、タイガーブックだと、{x|→E, y|→F} のような矢印が使われています。

最新コンパイラ構成技法

他に、{x := E, y := F} とか {x = E, y = F}、{x <= E, y <= F} という記法もあります。{x : E, y : F} も見たことあるような、JSONオブジェクトみたいです。ブレイス（波括弧）の代わりにブラケット（角括弧）で囲むこともあります。いずれにしても、“変数と式のペア”の集合となっています。変数も式も単なる名前やテキストではなくて、構文的なデータ構造と考えます。

で、どれを採用するべきか？ 色々な書き方があることを承知の上ならどれでもいいでしょう。「置換の圏から代入の圏へ」では {x := E, y := F} を使っています。たぶん、説明では今後もこの記法を使うでしょう*1。

*1:僕自身が一番よく使っているのは {E/x, F/y} という記法です。