「アリティ付きフラット・ラムダ計算 (1)」において、
アリティ付きラムダ計算は、通常のラムダ計算のサブセットというよりは、なにか別な世界を形成するように思えます。
と言いました。「なにか別な世界」がどんな世界なのかはそれほどハッキリしてません。ですが、「だいたいこんな感じ」という程度なら見えているので、それをインフォーマルにザザッと述べてみます。
僕の動機は次のことです。
今回この話題を仕切り直した主たる動機のは、再帰を許すモジュール概念をハッキリさせたかったからです。
このことを念頭においていただくと、理解しやすいのではないかと思います。
アリティ付きフラット・ラムダ計算では、高階の関数は出てこない（それでフラットと呼んでる）と言いましたが、裏方では高階の関数（指数）をバリバリに使うことになります。裏方とは意味論のことです。
再帰を考えない場合は、意味論も含めてフラットにできます。実際、「アリティ付きフラット・ラムダ計算 (1)」で記述した話では、まだ再帰が出てきてないので、高階の対象（指数）を持たない圏による意味論が可能です。
アリティ付きフラット・ラムダ計算の構文を見ると、ラムダ抽象を使って高階の関数を定義することはできません。ラムダ抽象がユーザー定義関数を表すと解釈すると、「ユーザーは、高階関数を定義することはできない」となります。なので、再帰的な関数を定義するための不動点コンビネータを定義することもできず、（それが高階でなくても）再帰的に定義された関数を扱えません。
再帰的な関数定義を許すための仕掛けがモジュールです。モジュールとは、名前を付けたラムダ項の集まりです。ここで名前とは変数記号のことです。uがアリティnの変数（u∈Vn）、tがアリティnのラムダ項として、ペア (u, t) が「名前を付けたラムダ項」ですが、(u, t) を def u t とか u := t とか書けばより馴染み深い記法となるでしょう。
モジュール内で、名前（変数記号）の循環参照を許せば、それにより関数の再帰的な定義が可能となります。モジュールが、通常のラムダ計算のletrecの役割を果たしていると言えます。あるいは、モジュールが不動点コンビネータの機能を提供します。
単独のラムダ項に意味は与える状況では高階の対象（指数）を必要としませんが、モジュールに対する意味論では高階の対象が必要です。モジュールとは「名前を付けたラムダ項の集まり」だと言いました。名前とは変数であり、必ずしもアリティ0とは限りません。つまり、関数変数も登場します。ですから、モジュールは複数の関数変数を未知数とする連立方程式系だとみせます。
u1, u2, ..., uk がモジュールに含まれる変数（名前）だとすると、連立方程式系とみなしたモジュールは次の形になります。
u1 = f1(u1, u2, ..., uk)
u2 = f2(u1, u2, ..., uk)...
uk = fk(u1, u2, ..., uk)
(f1(u1, u2, ..., uk), f2(u1, u2, ..., uk), ..., fk(u1, u2, ..., uk)) を (f1, f2, ..., fk)(u1, u2, ..., uk) と書くことにすると、上記の連立方程式系は、次の形に書けます。
- (u1, u2, ..., uk) = (f1, f2, ..., fk)(u1, u2, ..., uk)
番号の添字がうるさいので、u = (u1, u2, ..., uk)、f = (f1, f2, ..., fk) という“ベクトル記法”を採用すると、
- u = f(u)
となります。この形は、不動点方程式だというのは明らかでしょう。
モジュールが不動点方程式を記述するのは分かりました。モジュールの意味とは、この不動点方程式の解です。つまり、変数（未知数）u1, u2, ..., uk 達に具体的な意味的実体を割り当てたものがモジュールの意味となります。不動点方程式 u = f(u) の最小の解はギリシャ文字μ（ミュー）を使って μu.f(u) と書かれるので、u = f(u) の形をしたモジュールの意味は μu.f(u) だとも言えます。
今述べたような主張を正当化するには、意味論を展開する圏にそれなりの構造が必要です。それなりを正確に記述するのがアリティ付きフラット・ラムダ計算の目的のひとつです。
さて、モジュールが自由変数 w1, w2, ..., wm を含んでいる状況を考えましょう。すると、モジュールが定義する連立方程式系は次の形になります。
u1 = f1(w1, w2, ..., wm, u1, u2, ..., uk)
u2 = f2(w1, w2, ..., wm, u1, u2, ..., uk)...
uk = fk(w1, w2, ..., wm, u1, u2, ..., uk)
“ベクトル記法”を使うなら、u = f(w, u) です。変数ベクトルw は自由なので、この不動点方程式はパラメータ付き不動点方程式となります。パラメータが変数ベクトルwです。パラメータがあっても不動点方程式が解けるとして、その最小解を μu.f(w, u) と書きます。wは自由なのでラムダ束縛すると λw.(μu.f(w, u)) となります。ここで使ったラムダは形式的体系の内部のラムダ抽象ではなくて、説明のためのインフォーマルな記法です。
まとめれば； 自由変数を含むモジュールは、u = f(w, u) というパラメータ付き不動点方程式を定義して、そのパラメータ付き最小解は、λw.(μu.f(w, u)) という“関数”を定義します。この“関数”とは、意味論を展開する圏の射です。
意味論を展開する圏を適切に設定すれば、モジュールはその圏の射と解釈できます。通常のラムダ計算では、ラムダ項だけで何でも出来てしまうのですが、アリティ付きフラット・ラムダ計算では、ラムダ項（特にラムダ抽象）の能力が低いため、再帰や高階の対象の扱いはモジュールを使うことになります。このような役割分担をしたほうが通常のプログラミング言語やライブラリの構造に近いのじゃないか、と思うのです。
