ラムダ計算の特徴のひとつは、容易に高階関数が定義できることです。例えば、λf.λx.(f x) と書けば、applyを定義したことになります。高階関数とカリー化を使えば、多変数関数を考える必要はありません。f(x, y) の代わりに (f x) y と書けます（丸括弧を省略してもいいです）。プログラミング言語Haskellの構文は、この特徴を本質的に利用しています。
ただ、いつでも高階関数とカリー化が必要かというとそうでもなくて、「高階関数は要らないが、多変数関数は要る」という状況もあります。そんな状況ならラムダ計算は不要じゃないの？ -- いや、let式や不動点演算子などの議論はラムダ計算から拝借したいのです。というわけで、高階には登らないようなラムダ計算を定義してみます。
記事のタイトルに「(1)」が付いてますが、実を言うと、この記事と類似の内容は何度も話題にしたことがあります。以下の記事などです。
これらの記事との連続性は無視して、仕切り直しに近いので「(1)」と番号を付けました。僕の感触では、アリティ付きラムダ計算は、通常のラムダ計算のサブセットというよりは、なにか別な世界を形成するように思えます。
内容：
- 構文要素と基本的な意味論
- 項の定義
- 擬似項の定義
- 値割り当てと擬似項の具体化
- 閉じた擬似項の意味
- 再帰的定義やモジュールは次の機会
構文要素と基本的な意味論
F0, F1, F2, ... は非負整数で添字が付いた集合達です。iとjが異なればFiとFjの共通部分は空としましょう。Fnの要素はn引数の関数記号だと解釈します。特に、F0の要素は0引数の関数記号ですが、これは定数記号と同じなので、F0をC（Constantの'C'）とも書きます。f∈Fn のとき、arity(f) = n とします。
V0, V1, V2, ... も非負整数で添字が付いた集合達です。Fi達とは別な記号集合の列で、添字が異なれば共通部分はないとします。Vnの要素はアリティがnの変数記号です。気持ちとしては、「任意の」あるいは「可変の」n引数の関数を表すつもりの記号です。特に、V0の要素は「任意の」あるいは「可変の」値を表す変数記号です。u∈Vn のとき、arity(u) = n とします。
Fiが空であるようなiがあってもかまいません。むしろ、大部分のiで（有限個を除くiで）Fiが空であることが多いでしょう。極端なケースとして、すべてのFiが空であることも許されます。一方、Vi はすべてのiで可算無限集合とします。現実的には、必要なだけ変数が揃っていればいいのですが、理論上は無限としておくのが便利です。
変数記号が最初から無限個揃っているという仮定はほんとに理論上のもので、実装ではかなり異なった方式になります。有限集合Vがあって、Vの要素に対して動的にアリティを決めていく感じになることが多いでしょう。
さて、Dは、適当に選んで固定した集合とします。この集合Dを「値の領域」として意味論を考えます。Fnの要素fには、Dn→D である関数を対応させます。ここで、Dn は集合Dのn回の直積です。fに対応する実際の関数は【f】と書くことにします。f∈Fn なら、【f】:Dn→D ですね。
現実的には、【f】は部分関数となりますが、ボトム（⊥）の導入などで細工すれば、全域の関数とみなすこともできるので、全域性／部分性は気にしないことにします。意味割り当て 【-】をより正確に言えば； Dn→D の形の関数の全体（集合の指数）を [Dn, D] と書くことにして、【-】n:Fn→[Dn, D] の集まりになります。ですが、面倒なので、下付き添字のnは断りなしに省略します。
以下では、構文と共に基本的な意味写像【-】も備えた体系を考えます。今のところ、変数記号には意味を割り当てないでおきます。後で、変数記号にも意味を割り当てることがあります。
項の定義
項の定義は帰納的に行います。高階に登らないように注意して定義します。また、項の定義と共に、項のアリティと、項に含まれる 自由変数の集合も決めていきます。項tに出現する自由変数の集合を FVar(t) と書くことにします。
- fがFnに属する関数記号なら、fはアリティnの項である。FVar(f) = {}（空集合）。
- uがVnに属する変数記号なら、uはアリティnの項である。FVar(u) = {u}。
- tがアリティnの項で、t1, ..., tn がすべてアリティmの項のとき、t(t1, ..., ｔn) はアリティmの項である。FVar(t(t1, ..., ｔn)) = FVar(t)∪FVar(t1)∪ ... ∪FVar(tn)。
- tが任意の項で、x1, ..., xn がアリティ0の変数記号のとき、λ(x1, ..., xn).t はアリティnの項である。FVar(λ(x1, ..., xn).t) = FVar(t)＼{x1, ..., xn}(記号「＼」は集合差）。
- 以上で定義されるモノだけが項である。
t(t1, ..., ｔn) の形の項を適用（による項）、λ(x1, ..., xn).t の形の項をラムダ抽象（による項）と呼びます。
ラムダ抽象のときに使えるラムダ変数はアリティ0に限られます。これにより、高階引数が禁止されます。アリティ1以上の変数は高階の変数ですが、そのような変数の具体化は環境（いずれ述べます）によるもので、適用（引数渡し）で具体化はできません。
自由変数をひとつも含まない項、つまり FVar(t) = {} でああるtは閉じた項と呼びます。また、アリティ0の閉じた項を基礎項または具体項と呼びます。具体項は、値の領域Dの要素を表すと考えられます。また、具体項を作るための操作である、適用（引数渡し）と環境による置き換えを具体化と呼びます。なお、適用による具体化は環境による具体化（の特殊例）に還元できます。
擬似項の定義
項の定義は、完全に構文的なものであり、意味論とは無関係です。実際、値の領域Dは、項の定義のなかに出現しません。構文論と意味論の橋渡しとして、値の領域Dを考慮した項もどきを定義しておくと便利です。以下に定義するDを考慮した項もどきを、D擬似項と呼ぶことにします。
よく使われるD擬似項の定義は次のようなものです； Dの要素aごとに定数記号caを準備して、それらをすべてのcaを定数記号に付け足して、項の定義をやり直します。こうして定義できた新しい項がD擬似項です。
「Dの要素a ←→ 定数記号ca」は1：1の対応なので、aとcaを区別しないことにしてD擬似項の定義を律儀にするなら：
- aがDに属する要素なら、aはアリティ0の擬似項である。FVar(a) = {}（空集合）。
- fがFnに属する関数記号なら、fはアリティnの擬似項である。FVar(f) = {}
- uがVnに属する変数記号なら、uはアリティnの擬似項である。FVar(u) = {u}。
- tがアリティnの擬似項で、t1, ..., tn がすべてアリティmの擬似項のとき、t(t1, ..., ｔn) はアリティmの擬似項である。FVar(t(t1, ..., ｔn)) = FVar(t)∪FVar(t1)∪ ... ∪FVar(tn)。
- tが任意の擬似項で、x1, ..., xn がアリティ0の変数記号のとき、λ(x1, ..., xn).t はアリティnの擬似項である。FVar(λ(x1, ..., xn).t) = FVar(t)＼{x1, ..., xn}(記号「＼」は集合差）。
- 以上で定義されるモノだけが擬似項である。
最初の箇条項目以外は、項の定義の完全な繰り返しです。
Dの要素aに対して、擬似項としてのaの意味は値としてのaです。つまり、【a】 = a と決めます。これは当たり前ですね。閉じた擬似項、具体擬似項（基礎擬似項）も同様に定義できます。
擬似項は項とほとんど同じですが、意味論的な集合Dに依存している点に注意してください。完全に構文的な定義ではありません。Dの要素だけではなくて、実際の関数である [Dn, D] の要素も項のなかに混ぜ込んで擬似項を一般化することもできます（後で使うことになるでしょう）。要するに、意味領域の存在物を大量に（つうか全部）密輸入(?)して、構文的構造のなかに埋め込んでしまうわけです。ちょっと不純でご都合主義的ですが、便利な手法です。
値割り当てと擬似項の具体化
Dは、値の領域となる集合だとします。値割り当て（value assignment）とは、アリティ0の変数記号に対してDの要素を対応付けることです。より正確に書くと、ρ（ギリシャ文字ロー）が値割り当てだとは、ρが V0→D という部分写像であることです。ρの定義域を Def(ρ) と書くことにします。もちろん、Def(ρ)⊆V0 です。通常、Def(ρ) は有限集合です。
Def(ρ) = {x1, ..., xn} のときρを具体的に書き下すには、ρ(xi) = ai として、ρ = {x1|→a1, ..., xn|→an} のような記法を使うこともあります。
tがD擬似項だとして、t[ρ] とは、擬似項tに出現するアリティ0の変数記号xを、一律にρ(x)で置き換えたものです。もちろん、変数記号xが集合Def(ρ)に入るときだけ置き換えが行われます。t[ρ] を「置換」と呼ぶべきか「代入」と呼ぶべきか毎回悩むので、今回はρによるtの具体化と呼ぶことにします。この呼び方は、先に述べた「具体化」と整合します。
擬似項tを値割り当てρで具体化すると、変数記号は減ります。正確に言えば、変数記号が増えることはありません。FVar(t[ρ]) = (FVar(t)＼Def(ρ)) となります。FVar(t)∩Def(ρ) が空でないなら、実際に変数記号が減ることになります。
閉じた擬似項の意味
tが閉じた擬似項であるとき、その意味を定義します。値の領域Dと、各nに対するアリティnの関数記号に対する意味 【-】n:Fn→[Dn, D] は前もって決まっていると仮定します。これから定義する意味写像は、【-】の拡張となっているものなので、同じ記号【-】で表すことにします。
閉じた擬似項tの構文的な定義に沿って、帰納的に【t】を定義します。閉じた擬似項だけを相手にするので、自由変数は登場しないことに注意してください。tがアリティnの閉じた擬似項なら、【t】∈[Dn, D]、同じことですが 【t】:Dn→D となります。
- aがDに属する要素なら、【a】 = a である。
- fがFnに属する関数記号なら、【f】は前もって決まっている値を使う。
- tがアリティnの閉じた擬似項で、t1, ..., tn がすべてアリティmの閉じた擬似項のとき、【t(t1, ..., ｔn)】 = 【t】(【t1】, ..., 【ｔn】) と定義する。右辺は、実際の関数の合成を意味する。
まだ、閉じたラムダ抽象に対する意味が残っています。アリティnの閉じたラムダ抽象 λ(x1, ..., xn).t の意味は Dn→D という関数です。つまり、φ = 【λ(x1, ..., xn).t】 だとすれば、(a1, ..., an)∈Dn に対して関数値 φ(a1, ..., an)∈D が一意的に定まる必要があります。逆に、そのような φ(a1, ..., an)∈D がちゃんと決まるなら、閉じたラムダ抽象の意味【λ(x1, ..., xn).t】が確定することになります。
では、閉じたラムダ抽象 λ(x1, ..., xn).t に対して、実際の関数 φ = 【λ(x1, ..., xn).t】 を定めましょう。与えられた (a1, ..., an)∈Dn に対して、値割り当てρを、ρ = {x1|→a1, ..., xn|→an} として定義します。次に、このρにより擬似項tを具体化します。t[ρ] を作るのですね。
仮定より、ラムダ抽象 λ(x1, ..., xn).t が閉じているので、FVar(t)⊆{x1, ..., xn} です。したがって、t[ρ] に自由変数は含まれず、t[ρ] は閉じた擬似項です。閉じた義事項 t[ρ] には【-】の帰納的な定義が適用できて【t[ρ]】が計算できるので、その値を φ(a1, ..., an) とします。φ = 【λ(x1, ..., xn).t】 の定義をまとめて書くなら：
- φ(a1, ..., an) := 【t[{x1|→a1, ..., xn|→an}]】
項は擬似項の特殊なものなので、以上の定義で閉じた項の意味も確定します。
再帰的定義やモジュールは次の機会
閉じた項に対する意味は以上の手順で確定します。意味の定義は帰納的なので、値の計算を実行することもできます。しかし、これだけだと、再帰的な関数定義とその意味は確定しません。モジュールのような実用的な概念も定義されてません。これらは次の機会に述べたいと思います。今回この話題を仕切り直した主たる動機のは、再帰を許すモジュール概念をハッキリさせたかったからです。
