#acl alstamber:read,write,revert,delete,admin All:read = ラムダ計算 = 研究室で勉強することを強いられているので。 == 関数の定義 == まず前提として {{{ コンピュータで実行可能な計算はすべて帰納的関数の組み合わせによって表現することができる(チャーチ=チューリングのテーゼ) }}} とする。 関数を表現する時、普通は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 }}} == チャーチ数・チャーチ真理値を実際の数・真理値に変換すること == 今までチャーチ数およびチャーチ真理値をみてきたが、これを現実の数及び真理値と相互に変換できる関数を考えることができる。区別のため現実の真理値はTrueおよびFalseと表記する。<
> チャーチ真理値から現実の真理値を得る関数realboolは {{{ realbool = λb. b True False }}} 現実の真理値からチャーチ真理値を得る関数churchboolは通常のif文を用いて {{{ churchbool = λb. if b then true else false }}} と表せる。 またチャーチ数から現実の数を得る関数realnatは {{{ realnat = λm. m (λx. succ x) 0 }}} と表せる。 {{{ (λm. m (λx. succ x) 0) λsz. s z (λsz. s z) (λx. succ x) 0 (λz. (λx. succ x) z) 0 (λx. succ x) 0 succ 0 1 }}} このような関数はうまく働くように見えるが、call-by-value戦略においては綺麗な形に簡約できないことがある。<
> しかし見た目が全然違うからと言って実際の意味が違うわけではなく、その結果に対してすべての簡約できる部分を監訳する操作を加えれば簡潔な形となって、求める結果が得られていることがわかる。 == 再帰 == たとえば次のようなコンビネータを考える。 {{{ omega = (λx. x x) (λx. x x) }}} このコンビネータを簡約してみる。 {{{ (λx. x x) (λx. x x) (λx. x x) (λx. x x) (λx. x x) (λx. x x) ... }}} このように何度簡約しても同じ形が出てくる。このように正規形にならない状態のことを発散するという。 特にこのomegaコンビネータは何度簡約しても同じ形になる。このようなコンビネータは不動点コンビネータというものに一般化できる。<
> 不動点コンビネータは再帰を定義する際に有効である。 {{{ fix = λf. (λx. f (λy. x x y)) (λx. f (λy. x x y)) }}} 上のfixコンビネータは少し形が複雑で一見しただけではどのような性質を持つのか不透明である。 しかしこのコンビネータを使うと再帰を簡単に書くことができる。たとえば階乗は次のように書ける。<
> ここでrealeqとは2つのチャーチ数が等しいかどうかを調べて実際の真理値を返す関数、timesは掛け算をする関数、prdはチャーチ数から1を引く関数である。<
> またc0はチャーチ数で0を表す。同様にcnはチャーチ数で自然数nを表す。 {{{ g = λfn. if realeq n c0 then c1 else (times n (f (prd n))) factorial = fix g }}} 上の関数を使うにはfactorial c3などと使う。