ラムダ計算

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

関数の定義

まず前提として

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

とする。

関数を表現する時、普通は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+y)

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

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

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

λxy. x+y

束縛変数と自由変数

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

λx.M

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

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

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

λx.x

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

もう少し例を与える。

λy. x+y

上のラムダ式においてxは自由変数になっている。よってこのラムダ式が表す関数はコンビネータではない。
しかし外側に別に関数を次のように付け加えてみる。

λx. λy. x+y

するとxは外側の関数によって束縛される。この関数はすべての変数が束縛されているので、コンビネータになっている。

α変換

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

β簡約

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

(λ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)

チャーチ数の掛け算

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

2*2を計算してみよう。

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

β簡約の評価戦略

今までの簡約では簡約できるところを順序を気にせず全て簡約してきた。しかし他にも簡約の戦略というのは存在する。

たとえばnormal-orderと呼ばれる戦略は常に一番左で一番外側にある簡約できる場所から監訳するという戦略である。

call-by-nameと呼ばれる戦略はより制限があり、抽象の中身の簡約を許さない戦略である。

call-by-valueは多くの言語の実装にも使われている戦略で、簡約できるのは一番外側にある関数であり、かつそれは右側にある項を正規形に簡約してからという制約がある。
この戦略では式全体が常に評価され簡約されるとは限らない。

チャーチ真理値

数を導入したので、次に条件判定を記述するために真理値を導入する。

true = λtf. t
false = λtf. f

上のようなものを導入するとifは次のように書ける。

if a then b else c = λabc. a b c

本当かどうか気になるので、確かめる。

(λabc. a b c) true v w
true v w
(λtf. t) v w
(λf. v) w
v

同様にfalseのときはwが選ばれる。
ここで重要なのは、このifは一般的なプログラミング言語におけるif式とは異なるだろうということである。というのもcall-by-value戦略をとると先にif式の中の部分が評価されてしまうため、ifの条件がなんであれif式の中身が両方実行されてしまう、ということが起きてしまうからである。
これを防ぐためには遅延評価戦略をとる必要がある。

チャーチ真理値を用いた論理

and = λbc. b c false
or = λbc. b true c
not = λb. false true

対

チャーチ真理値を応用して対を定義することができる。

pair = λfsb. b f s
first = λp. p true
second = λp. p false

second(pair v w)
(λp. p false)(pair v w)
(λp. p false)((λfsb. b f s) v w)
(λp. p false)(λb. b v w)
(λp. p (λtf. f))(λb. b v w)
(λb. b v w)(λtf. f)
(λtf. f) v w
w

もう少し複雑な関数

チャーチ数を引数に取り与えられたチャーチ数が0に相当するものかどうかを調べるiszero

λm. m (λx. false) true

iszero 0を試してみる。

(λm. m (λx. false) true) λsz. z
(λsz. z) (λx. false) true
(λz. z) true
true

iszero 1を試してみる。

(λm. m (λx. false) true) λsz. s z
(λsz. s z) (λx. false) true
(λz. (λx. false)) true
(λx. false) true
false