ラムダ計算をちょっと勉強してみたので、忘れないうちに書いておく

なんとなく最近少し理論的な方面もやってみようかなと思い立って、今回はラムダ計算の基礎を勉強してみることにしました。
関数型言語の基盤らしいです。たしかにちょっと雰囲気はあります。

参考にしたページとしては

Wikipedia ラムダ計算 - http://ja.wikipedia.org/wiki/%E3%83%A9%E3%83%A0%E3%83%80%E8%A8%88%E7%AE%97
Wikipedia 型付きラムダ計算 - http://ja.wikipedia.org/wiki/%E5%9E%8B%E4%BB%98%E3%81%8D%E3%83%A9%E3%83%A0%E3%83%80%E8%A8%88%E7%AE%97
カリー・ハワード同型対応入門 - http://ocw.kyoto-u.ac.jp/ocw-archives-jp/002-006/pdf/curryhoward2.pdf

です。他にも参考にしたページは少しありましたが、覚えているのはとりあえず上の3つです。
最後の3つ目が最初にさらっとどんなものか見るにはいいかもしれませんね。

ラムダ記法

とりあえずラムダ計算にはラムダ記法というものがあるようです。

$\lambda x.(x+1)$

いわゆるプログラミングでいうところの関数に当たるものを表していて、

$f(x) = (x+1)$

のような関数に対応します(一般的に書くため、数学的な関数の書き方にしています)。ラムダ計算ではプロセス(関数)と結果(である値)が明確に区別されているようです。

また、 $x$ のような変数、および関数に引数を適用した $(\lambda x.(x+1))\hspace{6pt} 1$ もラムダ記法であり、ラムダ式と言います。

次に型付きラムダ計算というものでは、先ほどのラムダ計算のラムダ記法に“型”が導入されます。
先ほどの関数 $\lambda x.(x+1)$ では $x$ の種類がある程度決定できることがわかります。少なくとも $1$ と $+$ の演算が成り立つものでなければなりません。つまり $x$ は数値です。もっと厳格に強い型付けのプログラミング言語を意識して、整数(int)型としてしまいましょう。

つまり先ほどの関数はint型を受け取って、int型を返す関数となります。それを表すために次のようにラムダ記法で書きます。

$\lambda x.(x+1)\hspace{10.0pt}:\hspace{10.0pt}{\rm int \rightarrow int}$

関数型言語を知っている人の中には見覚えのあるような書き方かもしれません。

一般的には $\rm A$ と言う型の値を入力し、 $\rm B$ という型の値を出力する関数の型は $\rm A \rightarrow B$ となります。

もっと抽象的に $M$ をラムダ式として $\lambda x.M$ のように実装が明確に示されず書かれているものもあるようです。(詳しいことは知りませんが、そのように書く場面もあるようです)

複数の引数のときのラムダ記法と自由変数について少し書き足しておきたいと思います。

複数引数のときは $\lambda x.(\lambda y.x+y)$ となりますが、省略して $\lambda x\hspace{6pt}y.x+y$ と書けます。まさに関数型言語で言うところの高階関数ですね。

ちなみに自由変数は $\lambda x.x+y$ のように入力に依らない変数のことを言います。もっといえば束縛されていない変数、でしょうか。より正確な定義はWikipediaのラムダ計算を参照してください。

ラムダ式の同値関係、3つの変換

ラムダ式において、同値関係がどのようなものかを考えてみます。
そこで同値なものに変換する3つの変換を上げておきます。

$\bf \alpha -$ 変換
Wikipediaの言葉を借りると

束縛変数の名前は重要ではない

というのを基本的なアイディアとしたのが、 $\alpha -$ 変換だそうです。 $M$ 中の $x$ を全て $y$ に置き換えたものを $M[x:=y]$ と書くとすると
$\lambda x.M \rightarrow ^\alpha \lambda y.M[x:=y]$
のようにできるのが $\alpha -$ 変換です。
ただし、

- $M$ に自由変数として $y$ が出現しないこと
- $x$ の置換をすると $y$ が束縛されることがないこと

が条件です。

$\bf \beta -$ 変換( $\beta -$ 簡約)
関数適用を行った場合についてが、 $\beta -$ 簡約です。具体的には
$(\lambda x.x+1)\hspace{6pt}1 \rightarrow ^\beta 1+1$
とすることです。もっと一般には
$\lambda x.M\hspace{6pt}y \rightarrow ^\beta M[x:=y]$
であり、

- $y$ の代入によって $y$ 中の自由変数が束縛されないこと

が条件です。

$\bf \eta -$ 変換
ここは正直上手く説明できる気がしないのでWikipediaのお力を借りると

イータ変換の基本的なアイデアは、関数の外延性である。外延性とはここでは、2つの関数が全ての引数に対して常に同じ値を返すようなとき互いに同値であるとみなすという概念である。

だそうです。 $\eta -$ 変換自体は
$\lambda x.M\hspace{6pt} x\rightarrow ^\eta M$
のようなものです。

ここでちょっと用語まとめ

ラムダ記法(ラムダ計算)

$x$
$\lambda x.M$
$(\lambda x.M)\hspace{5pt} y$

のような記法。ちなみにこれらをラムダ式といいます。

ラムダ記法(型付きラムダ記法)
ラムダ計算のラムダ記法に型を導入したもの。
たとえば $\lambda x.(x+1)\hspace{6pt}:\hspace{6pt}{\rm int\rightarrow int}$ のように書きます。

変数
$x$ のようなもの。自由変数と束縛された変数があります。

(関数)適用
$(\lambda x.M) y$ のように関数に引数を適用すること。実際に代入した結果のラムダ式に変換することを([\beta -])簡約と言う。

(ラムダ)抽象
$\lambda x.M$ のようなもののことをいう。いわゆる引数をもつ関数。

$\bf \alpha -$ 変換
束縛変数の名前を変えるような変換。ただし変換前と後ではラムダ式は同値です。

$\bf \beta -$ 変換( $\beta -$ 簡約)
関数適用により、引数に代入する変換。ただし変換前と後ではラムダ式は同値です。

$\bf \eta -$ 変換
関数の外延性という概念に基づく変換。ただし変換前と後ではラムダ式は同値です。

さあ、再帰ってみよう

再帰をラムダ計算で使用するためには、「関数は自分自身をふくむ関数を定義できない」という問題があります。

しかしラムダ計算では、別の関数を定義してやることで再帰を定義することができます。
たとえば階乗計算の場合、 $g$ と言う関数を用いて

$g := \lambda f\hspace{6pt} n.(1,\hspace{6pt} {\rm if}\hspace{6pt} n = 0;\hspace{6pt} {\rm and}\hspace{6pt} n\times f(n- 1),\hspace{6pt} {\rm if}\hspace{6pt} n > 0)$

として、 $f$ と言う関数と $n$ を引数にとる関数として定義できます。
ただ、これはまだ再帰的にはなっていません。

この関数でもって再帰的に階乗計算を行うためには、引数で渡す関数がある性質をもっておく必要があります。それは
$g\hspace{5pt} f = f$
のようなもので、これによって再帰的に適用されることになります。

ここでYコンビネータと呼ばれるものがあります。
$Y = \lambda f.(\lambda x.f\hspace{5pt} (x\hspace{5pt} x))\hspace{5pt} (\lambda x.f\hspace{5pt} (x\hspace{5pt} x))$

これは
$Y\hspace{5pt} g=(\lambda f.(\lambda x.f\hspace{5pt} (x\hspace{5pt} x))\hspace{5pt} (\lambda x.f\hspace{5pt} (x\hspace{5pt} x)))\hspace{5pt} g$
$\hspace{13pt} =(\lambda x.g\hspace{5pt} (x\hspace{5pt} x))\hspace{5pt} (\lambda x.g\hspace{5pt} (x\hspace{5pt} x))$
$\hspace{13pt} =(\lambda y.g\hspace{5pt} (y\hspace{5pt} y))\hspace{5pt} (\lambda x.g\hspace{5pt} (x\hspace{5pt} x))$
$\hspace{13pt} =g\hspace{5pt} ( (\lambda x.g\hspace{5pt} (x\hspace{5pt} x))\hspace{5pt} (\lambda x.g\hspace{5pt} (x\hspace{5pt} x)))$
$\hspace{13pt} =g\hspace{5pt} (Y\hspace{5pt} g)$
のように、 $g\hspace{5pt} (Y\hspace{5pt} g) = (Y\hspace{5pt} g)$ の性質を持っています。

これを使って $g\hspace{5pt} (Y\hspace{5pt} g)\hspace{5pt} n$ のように適用することで、階乗計算が可能になります。