このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」（http://d.hatena.ne.jp/m-hiyama-memo/）のデータを移行・保存したものであり、今後（2019年1月以降）更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

最小のletrec式の求め方

モノイド圏 トレース／コンパクト閉圏 Caty プログラム意味論

x, y, z, f, g などは変数（を表すメタ記号、以下同様の注意を適用）、N, M などの大文字はラムダ式。x = N とか、f x = M とかの形を定義文と呼ぶ。式じゃなくて文なのは、これがある種の副作用（変数とラムダ式の束縛状態）をもたらすから。定義文を単に定義とも呼ぶ。

f x = M の形は関数定義だが、f = λx.M と書き換えて、常に左辺は変数（名前）だけの形に揃えるとする。JavaScriptで、function f(x) {...} を var f = function(x){...} にするのと同じ。

Sが定義の集まりのとき、登場する左辺変数の全体を LVar(S) とする。x∈LVar(S) だとして、変数（名前）xを定義するための、自由変数を持たない最小のletrec式を求める手順を以下に示す。今言った自由変数は、ラムダ式レベルの自由変数である（モジュールレベルの自由変数は残る、次節の注意を参照）。

自由変数

ラムダ式の自由変数とは、その式に出現する「ラムダ束縛されてない変数」のことである。ラムダ束縛されている変数は関数（引数の）パラメータだから、パラメータじゃない変数と言っても同じ*1。

ここでは、自由変数という言葉を二つの意味で使うので注意しておく。Mがラムダ式のとき、普通の意味の自由変数の集合を FVar(M) と書く。この場合、Mという単一の式だけを見て、そこに出現する変数を調べているので、他の式はまったく関係ない。Mだけで FVar(M) は決まる。

一方、Sが定義の集まりとして、FVar(S) は次の意味となる； まず、Sに含まれる定義の右辺（定義体）に含まれる自由変数をすべて寄せ集める。これを右辺変数の集合と呼ぶ。当然ながら、右辺変数の集合を作るとき、ラムダ変数（束縛変数）は入れない。Sの左辺変数の集合は説明するまでもないだろう。FVar(S) = (Sの右辺変数の集合)＼(Sの左辺変数の集合) である。ここで、＼ は集合差。

Sは、ひとつのモジュールや関連する（related）モジュールの集まりを意味するので、FVar(S) はモジュールレベルの自由変数だと言ってよい。モジュールレベルの自由変数は、モジュール内の定義からは意味が定まらない（自由である、開いている）。他のモジュールやなにか他のメカニズムで変数の値が供給される。

letrec式の構成

ここで作るletrec式は、letrec x1 = M1, x2 = M2, ..., xn = Mn in x1 という形とする。in の後は常に変数 x1 に固定するので、定義（束縛）の集まり {x1 = M1, x2 = M2, ..., xn = Mn} だけを問題にすればよい。

定義（束縛）の集まり（主にひとつのモジュール）と、ひとつの左辺変数xが与えられとして、別な定義の集まり {x1 = M1, x2 = M2, ..., xn = Mn} を構成していく。以下に手順を書く。なお、変数（またはラムダ式）には、再帰性を示すフラグが付けられるとする。変数の循環参照の検出アルゴリズムは述べないが、それは使えるものとする。

  1. 新しい定義（束縛）セットをTとして、その左辺変数集合をVとする。TとVを空集合で初期化する。
  2. x = x1 と置いて、Vにx1を追加する。この時点で V = {x1}。
  3. 左辺変数 x1 に対する定義体（右辺）M1 をSから取り出しTに入れる。この時点で T = {x1 = M1}。
  4. x1∈FVar(M1) なら（循環参照しているので）、x1（またはM1でも同じ）に再帰性フラグを立てる。
  5. FVar(M1) が空集合なら、ここで終わり。
  6. FVar(M1) の変数（名前）で、まだVに入ってないものがあれば、それらをすべてVに加える。
  7. Vに含まれる変数で、Sに定義があり、まだTの左辺にないものを選ぶ。それがないなら終わり。
  8. 選んだ変数をx2として、x2 に対する定義体（右辺）M2 をSから取り出しTに入れる。この時点で T = {x1 = M1, x2 = M2}。
  9. Tのなかで循環参照があるかどうかを調べて、循環参照がある変数に（複数あるならすべてに）再帰性フラグを立てる。
  10. FVar(M2) が空集合なら、ここで終わり。
  11. FVar(M2) の変数（名前）で、まだVに入ってないものがあれば、それらをすべてVに加える。
  12. Vに含まれる変数で、Sに定義があり、まだTの左辺にないものを選ぶ。それがないなら終わり。
  13. 以下、繰り返し。

変数の集合Vと、定義（束縛）の集合Tの2つを使う代わりに、Tだけを使い、Tのなかに、xi = (まだ未定義) のような特別な束縛を入れるだけでもよい。Tにハッシュマップ（辞書構造）、未定義にnullとかを使えばいい。

上記の手順はいつか終わり、左辺変数の集合と対応する定義体（右辺）、それと再帰性フラグが確定する。モジュールレベルの自由変数は未定義のままでVに残るが、これは捨てる（Tだけを使っているときも同様）。ただし、モジュールレベルの自由変数が有意義なら、どこかに取っておくことになる。

letrec式の簡約

先の手順で構成されたletrec式の左辺変数の集合のなかで、x1以外で、再帰性フラグが付いてない変数（非再帰変数）はすべて消去する -- 非再帰変数の出現を、その定義体（右辺）で置き換える。非再帰変数なら、この置換えでループ（無限展開）することはない。

再帰変数はそのまま何もしないで残す。再帰変数は、参照の有向グラフのサイクル上に載っている頂点となっている。つまり、展開不可能な参照サイクルが最後に残ることになる。

残った左辺変数がただ1つ（最初に選んだ変数）で、しかも非再帰のときは、letrecである必要はないので、letrecキーワードを外して右辺（定義体）だけの式に簡約する。再帰がない状況では、letrec式は消えてしまう。

letrec式のXJSONレイフィケーション

束縛の集まりは、{*: TypeExpr?} として表現できる。* のプロパティ名には変数名が入る。最初に選んだ変数を特定する必要があるので、"$" という特別な名前のプロパティ値に変数名文字列を入れておくことにする（アドホックだが簡単でいいだろう）。λx.M に相当する型表現は型抽象としてレイフィケーションする。



type LetrecExpr = @letrec {

  "$": string(remark="変数名（関数名を含む）"),
  /* プロパティ名は変数名 */

  *: TypeExpr?

};

ワイルドカード（'*'）の部分に登場する変数（プロパティ名）は、このletrec式で束縛されるので、自由変数ではない。letrec式に出現する自由変数はモジュールレベルの自由変数のみとなる。

*1:自由変数を「パラメータ」と呼ぶ場合もあるので注意が必要だ。