Login
Immutable PageDiscussionInfoAttachments

Revision 4 as of 2013-05-13 03:14:20

Clear message
alstamber/LambdaCalculus

MMA

ラムダ計算

研究室で勉強することを強いられているので。

関数の定義

まず前提として

コンピュータで実行可能な計算はすべて関数の組み合わせによって表現することができる(チャーチ=チューリングのテーゼ)

とする。

関数を表現する時、普通はfやらgやらの名前をつけるが、名前というのは関数の性質にとって本質的なものではない。
だから関数にわざわざ名前を付けずに取り扱えるようにしたい。たとえば

f(x) = 2 * x

という関数があったとする。これを以下のように表現することにする。

λx. 2*x

上のようにλという記号を使った関数の表現をラムダ記法と呼ぶ。
ラムダ記法を用いて関数の性質を定義することを関数抽象という。

関数適用

定義した関数を実際に用いることを関数適用と呼ぶ。関数をM、引数をNとしたとき、関数適用はM Nと記述する。

(λx. 2*x) y

上の式は「yにλx. 2*xを適用する」と読む。

複数引数関数とカリー化

一般に関数は複数の引数をとることがある。

f(x, y) = x + y

今までのラムダ記法の表現では2つ以上の引数を扱うことができない。
そこで2つ以上の引数を扱えるようにラムダ記法を拡張する必要があるのではないか、という気がしてくる。

実際にはそのようなことをしなくても2つ以上の引数を扱うことができる。
上の関数を少し変形してみよう。
そのために新しい関数gを定義する。

g(y) = y

このようにすると関数fは次のように定義できる。

f(x) = x + g(y)

この新しい関数fを実際に使ってみる。
まず関数fに3を与えてみよう。

f(3) = 3 + g(y)

となってyを引数に持つ新しい関数が結果となる。そこでgに5を与えてみる。すると

3 + 5 = 8

となってめでたく2つの数の和が求まる。

つまりn引数の関数は1引数の関数をn回適用する形に置き換えることができる。このことをカリー化という。

ラムダ記法と複数引数関数

ラムダ記法を使って複数引数関数を抽象することを考える。
たとえば次のようなラムダ式を考える。

λx.(λy.x)

外側から読んでいく。この関数はxという引数を受け取る。そして返すものが特徴的だ。
返すものはyという引数を受け取ってxを返す、という「関数」である。

このような関数を返したり、あるいは逆に関数を引数にとったりするような関数をラムダ記法では考えることができる。
これを高階関数という。
高階関数を使うことで、先ほどの項の要領を使って複数引数関数をカリー化し、ラムダ記法で表すことができるようになる。

高階関数を使うときには括弧を省略し、更にはλを省略することが多い。

λxy. x

束縛変数と自由変数

次のようなラムダ式を考える。

λx.M

この式において、Mの中にxが出てきた時、xのことを束縛変数と言う。
λの後ろにあるxは関数の引数なのでこのラムダ式を値に適用するとxは何らかの意味を持った存在となる。

一方Mの中にx以外の変数が出てきた時それを自由変数という。
自由変数は関数の引数として与えられないので、それ単体ではどういう意味を持った存在なのか(どういう値に対応するのか)わからない。

自由変数を持たない式をコンビネータという。 最も簡単なコンビネータはおそらく下のようなものだろう。

λx.x

これは引数として与えられたものをそのまま返すコンビネータで、Iコンビネータという名前がある。

α変換

束縛変数は式の中で値と対応付けられ意味を持った存在であるので、他の束縛変数と名前がかぶってしまうことは許されない。
しかしそうならない範囲で名前を変えても式は全く同じ意味となる。
そのように式中の変数の名前を変えることをα変換という。

β簡約

関数の適用を実際に行うことを簡約という。
簡約は左側が抽象になっている適用に対して、抽象の束縛変数を適用の右側で置き換えることで行われる。
これをβ簡約という。

(λx.x) a ←x(束縛変数)をa(右側)で置き換える
a

(λx.λy.x) a ←x(束縛変数)をa(右側)で置き換える。束縛変数が複数あるときは左から適用する。
λy.a

(λxyz.x z (y z)) (λxy.x) λxy.x ←xを置き換えたいが、置き換えるとyがダブってしまうので、ダブらないようにα変換する
(λxyz.x z (y z)) (λxw.x) λxy.x ←一番左のxを(λxw.x)で置き換える
(λyz.(λxw.x) z (y z)) λxy.x ←一番左のyをλxy.xで置き換える
(λz. (λxw.x) z ((λxy.x) z)) ←zに(λxw.x)を適用する
(λz. (λw. z) ((λxy.x) z)) ←wを((λxy.x) z)で置き換える
(λz. z) ←Iコンビネータになる

これ以上簡約できない形のことを正規形という。
簡約できる部分が複数あるときはどこから簡約してもよく、またどこから簡約しても正規形になるのであれば必ず同じ形になる。
つまり正規形はあるとすれば唯一である。
ただしどの順番で簡約しても必ず正規形になるとは限らない。

チャーチ数

今まで考えてきたラムダ記法にはまだ数というものがない。ラムダ記法には数が存在しないため、チャーチ数というものを導入して自然数を定義する。
チャーチ数というのはラムダ記法を使って(つまり抽象と適用を使って)自然数を定義する手法である。まず0を定義する。

0 = λsz. z

続いて1を定義する。

1 = λsz. s z

同じように2は

2 = λsz. s (s z)

と定義される。このように自然数nはzにsをn回適用することで表現される。
ここでzというのはzを表すもの、sは+1を表すものだと考えていただきたい。

チャーチ数の足し算

チャーチ数同士を足し算する関数を定義する。

a + b = (λmnsz.m s (n s z)) a b

1+1を計算してみよう。

(λmnsz.m s (n s z))(λsz. s z)λsz. s z
(λnsz.(λs'z'. s' z') s (n s z))(λsz. s z)
(λsz.(λs'z'. s' z') s ((λs''z''. s'' z'') s z))
(λsz.(λs'z'. s' z') s (s z))
λsz. s (s z)