カテゴリ:ラッセルのパラドックス( 64 )

ラムダ計算インタープリタ

ラムダ計算の項 (term) の定義は次のように再帰的に定義される。

(1) 変数 x0, x1, ... は λ 式である。
(2) M が λ 式で x が変数のとき (λx. M) は λ 式である。
(3) M と N が λ 式のとき (MN) は λ 式である。

これは項の文法が文脈自由法で次のような BNF 記法で定義できることを示している。

<term> ::= <identifier>
<term> ::= (λ<identifier>. <term>)
<term> ::= (<term> <term>)

つまりラムダ記法は文法規則がたった3行しかないプログラム言語なのだ。プログラム言語というからには、インタープリタができるはずだ。そのインタープリタはどういう動作をするのだろうか。これは端的に言うと、ラムダ計算のインタープリタはラムダ計算の項を β 簡約でインライン展開してできるラムダ計算の項を出力するという動作をするのだ。ラムダ計算の項で記述されたソースを取り、それを β 簡約して新しいラムダ計算の項をターゲットとして出力するのがラムダ計算のインタープリタの仕事だ。

ラムダ計算の本質は、項の文法規則と、α 変換と β 簡約による項の変形規則からなる記号列の集合なので、こういうことが起きる。たった3行の文法規則と、本質的には β 簡約というひとつの変形規則だけでコンピュータで実現できるすべての計算を表現できるらしい。

ラムダ計算のインタープリタがそのような簡単なものなら誰かが作ってくれているのではないかとネット検索したら次のようなサイトを見つけた。


インタープリタは次のサイトで実際に実行してみることができる。


実行例

>(function (x) {return x}) a
(function(x){ return x })(a)
→a

抽象的なラムダ計算だが、インタープリタを操作しながら動作を確認できるのはありがたい。

記号列のソースをインタープリターで処理して出力が記号列というのはあまり意味がないように思えるが、ノイマン型のコンピュータでも機械語のレベルで見れば、ソースはビット列で出力もビット列だ。コンピュータの処理がいろいろできているように見えるのは、出力のビット列を解釈してモニターの画像や、通信機の出力に変換しているからだ。ラムダ計算のインタープリターの入力が記号列で出力も記号列であってもその意味付けはマイクロプロセッサーと構造的に同じなのだろう。

ラムダ計算では数値や論理値も関数で表現するので違和感を感じるが、マイクロプロセッサーの場合もそれらの値はビット列で表される。両者の記号列に対する意味付けの方法に共通性があるのかもしれない。

[PR]
by tnomura9 | 2017-12-21 14:03 | ラッセルのパラドックス | Comments(0)

λ式 (λ-term)

プログラム言語のλ記法は次のように無名関数を記述するのに使われる。

Prelude> (\x -> x * x) 2
4

このようなλ記法では λx はそれに続く数式の変数を指定するために用いられている。関数に名前のない無名関数を利用できるのは、不必要な名前空間の浪費を避けることができるのでプログラマにとっては非常にありがたい機能だ。

しかし、λ計算の世界では λ式 (λ-term) は再帰的に次のように定義される。

(1) 変数 x0, x1, ... は λ 式である。
(2) M が λ 式で x が変数のとき (λx. M) は λ 式である。
(3) M と N が λ 式のとき (MN) は λ 式である。

この定義をもとにλ式 M を次々に作っていくことができる。たとえば x は (1) からλ式である。また、x がλ式であることと規則 (2) と から λx.x はλ式である。さらに、x, y はλ式であるから (3) から xy はλ式である。こういうふうにして作られた、

λx.λy.(x(λz.(xz)(yz)))y

のような変数とλと()の記号の並びが λ 式なのだ。この記号列の中には + も * もその他どんな演算子も含まれていない。Charch-Rosser の定理のようなものはこのような記号の列についての法則だ。ここが分かっていないと、λ計算の議論についていけない。

λ計算についてのもう一つのポイントは、変数 x はそれ自身で関数であるということだ。変数 x が関数であるというのは納得できない感じがするが、それを認めないと変数 x の自己適用 (xx) が受け入れられなくなる。

このように、λ 式は変数から規則 (2) と規則 (3) で無限に作り出される記号列であって、どのλ式をとってもそれは関数であるような記号列なのである。λ計算の領域 D はこうした記号列で表される関数の集合である。

ところで、λ式は全て関数だといったが、λ式の再帰的定義には関数という用語は出てこない。定義は単に記号の配列のルールを述べているだけだ。したがって、関数適用や関数抽象などのλ式の変形規則も単にλ式の記号列の変形の規則でしかない。つまり、λ計算で論じられる様々な定理は、すべてλ式という記号列の操作に関するものであって、それが関数かどうかは問題にしていない。λ計算の議論は純粋に統語論的な議論なのだ。

しかしながら、このような記号の操作が、すべての関数の不動点を作り出す Y-コンビネータのような関数を作り出してそれが実際のプログラムとして動くのは不思議な感じがする。

[PR]
by tnomura9 | 2017-12-05 20:02 | ラッセルのパラドックス | Comments(0)

関数の自己適用とゲーデル文

領域 D を関数の集合とする。また、この関数は全て領域 D を定義域とし、領域 D が値域であるとする。つまり、領域 D の要素は全て任意の D の要素を引数としてとり、その値が領域 D の要素であるような関数である。

x を D の要素の1つとすると、x は x 自身を引数として取ることができ、関数の自己適用 x x の値は D の要素のひとつである。

そこで、x x を引数として取る f (x x) を考えると、領域 D では f (x x) も関数であるから、その自己適用 (f (x x)) (f (x x)) も考えることができ、それもやはり領域 D の関数だ。そこで、これをβ縮約してみる。

(f (x x)) (f (x x)) = f ((f (x x)) (f (x x)))

これは (f (x x)) (f (x x)) が関数 f の不動点になっていることを示している。

ところで領域 D の要素としては 1 と 0 という定数も含むことができる。これらはチャーチ数として次のように関数で定義する。

0 := λf x. x
1 := λf x. f x

0 は引数 f をとり任意の関数 x に0回関数適用する関数である。1 は引数 f をとり関数 x に 1 回適用する関数である。

この条件のもとで、領域 D の要素をとり、1または0の値(関数)を返す D の要素 x は通常の述語である。x(y) =「y は赤い」という述語は領域 D の要素 y が赤ければ 1 を返しそうでなければ 0 を返す。すなわち、x y という要素 y に対する x の関数適用は 1 または 0 になる。りんごに対する(赤い)の関数適用 (赤い)りんご の値は1であり、(赤い)メロン の値は 0 である。また、述語 (赤い)を自己適用すると (赤い)赤い になるが(赤い)という述語は赤くはないのでこれは 0 である。

そこで x = 「証明可能である」という述語と f = ¬ という論理演算子を上の不動点の等式に代入してみる。

(¬((証明可能) 証明可能)) (¬((証明可能) 証明可能))) = ¬ (¬((証明可能) 証明可能)) (¬((証明可能) 証明可能)))

(f (x x)) (f (x x)) が f の不動点になるために、(¬((証明可能) 証明可能)) (¬((証明可能) 証明可能))) が真ならば (¬((証明可能) 証明可能)) (¬((証明可能) 証明可能))) が偽となって、パラドックスになってしまう。

(¬((証明可能) 証明可能)) を普通の文で表すと、「証明可能という述語が証明可能ではない」という述語になるが、この述語の自己適用は証明可能でも証明不可能でもない。ゲーデルの不完全性定理は理解していないが、おそらくこれがゲーデル文の正体だろう。

概念をも含んだ森羅万象を閉じ込めた領域 D を考えると、不動点が発生してしまい、論理的なパラドックスが発生してしまう。この原因は関数を引数に取る高階関数の存在だ。Haskell を使うと、

map (*2) [1, 2, 3, 4, 5]

のような高階関数の威力を感じるし、一度これを使い始めると手放せないが、それゆえにプログラムの中に森羅万象を閉じ込めるのは不可能だという結論はプログラミングの可能性と限界を示していて感慨深い。

[PR]
by tnomura9 | 2017-12-01 01:22 | ラッセルのパラドックス | Comments(0)

集合とは何か

素朴集合論における集合の定義は「集合とはものの集まり(というもの)」である。しかし、これでは、集合という「もの」の位置づけと、「ものの集まり」との関係が曖昧だ。そこで、素朴集合論における集合の定義を次のように変えてみる。

対象の集まりを領域 D とする。また、領域 D の任意の2つの対象間には帰属関係 ∋ が定義されているとする。集合とは領域 D の対象のうち帰属関係 a ∋ b の左項になりえる対象の事を言う。言い方を変えると、領域 D の対象のうち、他の対象を要素として含んでいるものが集合である。(ただし例外として要素を一つも含まない空集合 {} も集合であるとする。空集合は要素を含まないが、同じ要素を含まない個体とは区別する。)

ここで帰属関係の判別関数 ψ : D ✕ D -> {0, 1} を次のように定義する。

領域 D の任意の対象 x, y について x ∋ y ならば ψ(x, y) = 1、それ以外は ψ(x, y) = 0

この判別関数を用いることで、集合 a の外延を求めることができる。すなわち、領域 D の対象である集合 a に対し ψ(a, x) = 1 を満たす対象 x の集まりが集合 a の外延である。このことよって集合 a の「もの」としての性質と「ものの集まり」という性質の関係を明確にできる。

これらの条件のもとで領域 D の性質をいろいろと調べてみることにするが、それらの概念は集合の用語を使わないと不便だ。したがって、用語の循環を恐れずに集合の用語を用いて考えることにする。

領域 D の要素の部分集合を全て集めた D の冪集合 2^D を考える。これは領域 D で完全に決定される。このとき領域 D の集合 a の外延は 2^D の要素の1つと一致する。また、領域 D の集合の外延の全ては必ず 2^D の要素の1つと一致する。

領域 D から領域 2^D への全単射はないので、領域 D の対象である集合 a をすべて集めても、2^D に現れる領域 D の部分集合全てを表すことはできない。したがって、領域 D の集合では、領域 D で出現可能な全ての集合を表現することができない。この領域 D の集合では表現できない領域 D の部分集合を「(狭義の)クラス」と呼ぶことにする。しかし、領域 D の対象の可能な集まりは、領域 D の集合と「クラス」でもれなく表現することができる。これを「(広義の)クラス」と呼ぶことにする。

集合の述語 P : D -> {0, 1} は領域 D の対象 a を引数にとり、a がその述語を充足するとき P(a) = 1、それ以外は P(a) = 0 であるとする。この時領域 D の全ての対象について P(x) = 1 か P(x) = 0 のどちらかが成り立つ。すなわち述語は排中律を満たす。

述語 P(x) の値によって、領域 D の全ての部分集合を定義することができる。すなわち 2^D の要素を A としたとき、

A = { x | P(x) }

で内包的定義を行うことができる。

しかしながら、内包的定義で定義できるのは 2^D の要素である「広義のクラス」である。領域 D の要素数では 2^D の要素である D の部分集合全てを表現することはできないので、集合を定義できない内包的定義が存在する。そのような領域 D の要素に集合を持たない内包的定義のみの D の部分集合は「狭義のクラス」である。ラッセルの集合は領域 D の部分集合としては存在するが、これを外延とする「集合」を領域 D の中に求めることができないので、これは「狭義のクラス」である。

内包的定義は 2^D について排中律をみたすので、1階述語論理の適用ができる。すなわち、

A = {x | P(x) ∧ Q(x)}

のような論理演算に対応する真理集合は定義でき、また、2^D は全ての論理演算子について閉じている。ここでは量化子については述べないが、量化子の演算を含めた全ての1階述語論理は領域 D について 2^D に展開可能である。

このように、領域 D を明確化すると、2^D の要素としての「広義のクラス」、領域 D の要素としての「集合」、領域 D の要素としては存在しない「狭義のクラス」を定義できることができる。そうして一階述語論理が「広義のクラス」に対し矛盾なく適用できることが分かる。

ラッセルのパラドックスに始まる「集合論」の危機は、素朴集合論の「集合」が領域 D の部分集合の全体を表現できないことを示しただけだったのだ。また、複雑な公理的集合論は、領域 D の「集合」で表現できるものは何であるかを限定するための規則なのだ。

このように、集合と論理の整合性は、領域 D を明確にすることで「広義のクラス」として成立させることができる。ベン図における全体集合の存在は、集合と論理の整合を図る上で必須の概念なのだ。

集合とは何か。それは領域 D の対象の外延として表現できる領域 D の部分集合なのである。



[PR]
by tnomura9 | 2017-11-23 09:24 | ラッセルのパラドックス | Comments(0)

ラッセルのパラドックスとY-コンビネータ

『自己言及の論理と計算』長谷川真人著の7ページには、ローヴィルの不動点定理について次のように説明してある。

ここからは,より一般的な観点から,ラッセルの逆理やカントールの対角線論法などの背後に共通する数学的な仕組みについて考えてみよう.ここでは,一種の不動点定理を拠所にして,種々の同様な現象へのシステマティックなアプローチを試みる.
 まず,ややインフォーマルな説明をしよう.φ : A × A → B について,以下のことが成り立っているものとする.
任意の g : A → B に対しある a ∈ A が存在して g(x) = φ(a, x) が成り立つ (このような a を g のインデックスと呼ぶ).

このとき,任意の f : B → B は不動点を持つ.具体的には,g0 : A → B を g0(x) =f(φ(x, x)) で定義してやり, a0 ∈ A を g0 のインデックスとすると, φ(a0, a0) は fの不動点になっている.実際,f(φ(a0, a0)) = g0(a0) = φ(a0, a0).
ほとんど自明とも思われる結果だが,ここには,インデックス付けによる数え上げ,対角成分への着目 (関数の自分自身のインデックスへの自己適用) による不動点の構成といった,数理論理学や計算の理論の基礎的なアイデアが,端的なかたちであらわれている.
 より正確には,有限直積をもつ任意の圏について,以下の結果が知られている (ローヴィル4 の不動点定理).圏論の言葉になじみのない人には,上記の説明で十分なので,とばしてもらってかまわない.

この不動点定理の説明で A を対象の集合、Bを真理値の2値集合 {0, 1}、φを対象の直積から2値集合 {0, 1} への関数、つまり対象間の帰属関係をあらわす判別関数とすると、この不動点定理を素朴集合論の世界に適用できる。

すなわち、g(x) はある集合 a が任意の対象 x を要素として含むかどうかの判別関数であり、素朴集合論の世界では任意の対象(集合)a がそういう判別関数を持っているので、g(x) = φ (a, x) だ。このとき対象(集合)a は g(x) のインデックスになる。g(x) = 1 となる対象 x を集めると対象 a の外延である対称の集まりを求めることができる。{x| g(x) = 1} は a の内包的定義になる。

関数 f : B -> B は真理値から真理値への関数つまり、1引数の論理演算子だ。g0(x) = f(φ(x,x)) なので、g0(x) は対象 x が自分自身を要素として含むかどうかの真理値に論理演算子 f を適用したときの判別関数だ。対角線成分に f が関数適用されていることになる。

この判別関数 g0 のインデックス a0 は対角線成分に f を適用して得られる集合 a0 を表している。すると素朴集合論の世界では次の不動点が存在する。

f(φ(a0, a0)) = g0(a0) = φ(a0, a0)

f が否定演算子 ¬ の場合この不動点はラッセルのパラドックスを発生する。すなわち、a0 が自分自身を要素として含んでいなければ(¬(φ(a0, a0)) a0 は自分自身を要素として含む (φ(a0, a0))が同時に起きる。この時判別関数 g0(x) のインデックス a0 は「自分自身を要素として含まない集合の集合」である。

どこに問題があるのかというと、

任意の g : A → B に対しある a ∈ A が存在して g(x) = φ(a, x) が成
り立つ (このような a を g のインデックスと呼ぶ).

という仮定だ。つまり、全ての集合がその要素を判別するための判別関数(内包的定義)を持つと考える素朴集合論の世界では、否定論理演算子 ¬ についての不動点のためにパラドックスが発生してしまうのだ。

このパラドックスの解決は上の仮定が成立しないことを認めることだ。すなわち、インデックス a を持たない判別関数 g : A -> B が存在する。対象(集合)の集合の要素をその冪集合の要素と全単射させることは不可能なため(要素数のほうが圧倒的に不足する)、判別関数 g(x) によって定められる対象の集合でありながら、そのインデックス a を持たないものが存在しているのだ。その対象からなる全ての集合を判別関数(内包的定義)で定義するには要素数(濃度)が不足するということだ。

しかし、対象の集合の部分集合を表す記号を、対象の集合の外に求めれば、この問題は起きない。言い方を変えると、集合の世界を「帰属関係の定義された対象の集合」として捉えようとしても、その集合の全ての部分集合を表すためには、対象の数が不足してしまうが、集合をあらわすインデックスを対象の集合以外に求めれば問題は解決する。集合を表すインデックスが対象の集合の外にあれば、不動点は発生せず、任意の判別関数に対し集合のインデックスを求めることができる。

ただし、このことはインデックスを対象の集合の要素に求められないというわけではなく、対象のうちインデックスとすることができるものはそうすればいいのだ。この観点から見ると、対象の集合の部分集合のインデックスは対象の外にあり、これを「広義のクラス」と考える。また、対象の集合の要素にインデックスを求めることができる場合は、これを「集合」と考える。対象の集合の要素にインデックスを求められない要素の(部分)集合に対しては、これを「狭義のクラス」と考えるのだ。こうすれば、対象の集合の全ての部分集合に対し「広義のクラス」のインデックスを求めることができ、内包的定義はかならず「広義のクラス」を定めることが分かる。

こう考えると公理的集合論の公理がなぜあのように複雑なのかが分かる。これらの公理は、対象の集合内にインデックスを持つ集合だけを取り出すためのルールなのだ。

ところで、上の不動点の議論のかなめとなるのが、

f(φ(a0, a0)) = g0(a0) = φ(a0, a0)

となる任意の関数 f の不動点 φ(a0, a0) の存在だ。これは、Y-コンビネータによる不動点、

Y g = g (Y g)

と対応している。Y−コンビネータはラッセルのパラドックスと同じメカニズムなのが分かる。

[PR]
by tnomura9 | 2017-11-22 07:48 | ラッセルのパラドックス | Comments(0)

関数の自己適用

Y - コンビネータのλ式は次のようになる。

Y = (λf . (λx . f (x x)) (λx . f (x x)))

このコードには不可解な点が多いが、先ず目につくのは (x x) という関数の自己適用だ。関数 x をそれ自身の x に適用させている。Y-コンビネータはさらにこの関数の自己適用でできた関数を利用して、(f (x x)) (f (x x)) とさらに2重の関数の自己適用を行っている。おそらく、これが、Y-コンビネータの無名関数で再帰的定義の関数をつくるという離れ業の原因だろう。

そこで、まず、最も単純な (x x) という形の関数の自己適用について考えてみた。この形の関数の自己適用が行われたときに x について必要な条件はなんだろうか。まず、x は関数 x を引数として取るので高階関数でなくてはならない。x に 2 を代入して (2 2) としてもこれは動作しない。

それでは x = λy.(y*2) の場合はどうだろうか。この場合 (x x) = ((λy.(y*2)) (λy.(y*2))) となるが、これも動作しない。λy.(y*2) は数値の引数をとり、数値を戻り値として返す関数だ。別の言い方をすると、この関数の domain は数値の集合で、codomain も数値の集合である。従って λy.(y*2) は関数である λy.(y*2) を引数にとることはできない。

こんどは x = id の場合を考えてみる。id x 関数は次のように定義され、引数 y をそのまま返す関数だ。

id y = y

この関数 id は (id id) のように関数の自己適用ができるだろうか。これは可能だ。id は引数 id をそのまま帰すので (id id) = id となる。これは次のように Haskell でも試してみることができる。

Prelude> let id x = x
Prelude> id 2
2
Prelude> ((id id) 2)
2
Prelude> ((id (id id)) 2)
2
Prelude> ((id (id (id id))) 2)
2

(id id) = id なので (id (id id)) や (id (id (id id))) のようなものも全て id と等しくなる。つまり、(x x) という関数の自己適用は、

(x x) = (x (x x)) = (x (x (x x)) = (x(x(x(.... (x x)....))))

と無限に展開するラムダ式を発生させることができる。まるで合わせ鏡のように、(x x) という簡潔な表現の中に無限を閉じ込めることができるのだ。x が関数の場合、x のdomain は関数の集合で、x の codomain も関数の集合なので、この展開は無現に続けることができる。

そこで改めて Y-コンビネータ (f (x x)) (f (x x)) を展開してみよう。

(f (x x)) (f (x x))
= (f ((f (x x)) (f (x x)))
= (f (f ((f (x x)) (f (x x))))
= (f (f (f (f .... ((f (x x)) (f (x x))) .... ))))

やはり、この式が無限に展開できることが分かる。これは f (x x) のように f が合わせ鏡の関数を引数に取るために、それを展開すると f ((f (x x)) (f (x x))) となり、展開された f の引数が ((f (x x)) (f (x x)) のように元のλ式になってしまうからだ。

Y-コンビネータの場合、任意の関数 g を上の f にあてはめることができるので、つぎの等式が成立する

Y g = g (Yg)

したがって g に階乗を求める関数をとると、

(Y g) 5 = 5 * (g (Y g) 4)) = 5 * 4 * (g (Y g) 3) = ...

となって遅延評価の関数言語であれば、階乗の計算ができることになる。それだけではなく、g に任意の再帰関数をとれば、任意の再帰関数の定義が Y g でできることが分かる。

Haskell では遅延評価なのでつぎのように簡単に階乗を計算する無名関数を記述することができる。

Prelude> let y x = x (y x)
Prelude> (y (\f n -> if (n == 1) then 1 else n*(f (n-1)))) 5
120

このように関数が first-order のデータであるような言語では、高階関数の自己適用により合わせ鏡のような関数を記述でき、そのなかに無限の操作を導入することができる。ただし、その場合無限の展開が終わらない場合も出てくるので、絶対に停止するプログラムだけを作ることはできなくなる。

ラッセルのパラドックスのメカニズムも自己言及が原因なので、このような合わせ鏡のメカニズムが関係している可能性がある。素朴集合論の世界は、プログラム記述可能な世界と同じものなのだろう。素朴集合論の世界でも無限を全て捉えたと考えてくると矛盾がでてくるが、プログラムの世界も無限の全体を捉えることはできない。しかし、どちらも無限にそれを展開していくことができるという可能無限な世界なのだ。

[PR]
by tnomura9 | 2017-11-19 07:05 | ラッセルのパラドックス | Comments(0)

Z - コンビネータ

Y - コンビネータのλ式は次のようになる。

Y = (λf . (λx . f (x x)) (λx . f (x x)))

これを任意の関数 g に関数適用するとつぎのように Y g が g についての不動点になる。

Y g
= (λf . (λx . f (x x)) (λx . f (x x))) g
= (λx . g (x x)) (λx . g (x x))
= (λy . g (y y)) (λx . g (x x))
= g ((λx . g (x x)) (λx . g (x x)))
= g (Y g)

このとき、g が第1引数に関数、第2引数に整数を取るような場合、たとえば g f n = n * f(n - 1) のような場合、

(Y g) 5 = (g (Y g)) 5 = g (Y g) 5 = 5 * ((Y g) 4) = 5 * (4 * ((Y g) 3)) ....

のように再帰的な計算ができることになる。ところが、Y - コンビネータの定義をそのまま Scheme のλ式にコーディングしても動作しない。それは、プログラムのパースのときに、

Y g = g (Y g) = g (g (Y g)) = g (g (g (Y g))) = ....

と無限の展開が行われるからだ。これを解決するためにはつぎのような Z - コンビネータを利用する。

Z = λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))

これは Y - コンビネータの定義に変数 y を付け加え Y - コンビネータの (x x) を λy. x x y に置き換えただけだ。この置き換えは η 変換と言うらしい。変数を1つ付け加えることで Z g の展開は次のように整数 n を巻き込む形になるので、Y g 部分の無限の展開が起きず再帰は base case で停止することができる。

(Z g) n
= (λf. (λx. f (λy. x x y)) (λx. f (λy. x x y)) g) n
= ((λx. g (λy. x x y)) (λx. g (λy. x x y))) n
= g (λy. (λx. g (λy. x x y)) (λx. g (λy. x x y)) y) n
= g (λy. (λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))) g) y) n
= g (λy. (Z g) y) n)
= g (Z g) n

Scheme で実行すると次のようになる。

1 ]=> (define z (lambda(f)((lambda(x)(f(lambda(y)((x x)y)))) (lambda(x)(f(lambda(y)((x x)y)))))))

;Value: z

1 ]=> ((z (lambda(f)(lambda(n) (if (zero? n) 1 (* n (f (- n 1))))))) 5)

;Value: 120

λ計算の面白いところは任意の関数 g についての不動点を作り出す Y - コンビネータの動作が、記号列の等価変換だけで証明できるということだ。不動点による無限の再帰もλ式の記号列の変換だけで定義できる。

しかし、その中には無限の再帰が存在するために、プログラムを解釈して実行するプログラム言語による意味論的な解釈によっては無限の再帰に陥ってプログラムが動作しなくなる場合がある。

プログラムの動作をプログラムの記号列だけが決定しているのであれば、プログラムの記号列を検査するだけでそのプログラムがきちんと動くかどうかを決定できる。しかし、残念ながら任意のプログラムが動作するかどうかを決定するプログラムをλ式で作ることはできないことが証明されているらしい。

ヒルベルトの夢は数学をこのような記号列の変換に閉じ込めようとしたことだ。しかしそれは、

「対角式は証明できない」の対角式は証明できない

という不動点を作り出すことができることをゲーデルが証明し、証明もその否定も証明できない命題が存在することが分かってしまった。(上の命題が証明可能であるとすると「対角式が証明できない」という語の対角式はその命題自身になってしまうのでその命題は証明不可能ということになる。「対角式は証明できない」の対角式が証明不可能であるとすると、その対角式である上の命題が証明可能であるということになるので、いずれもパラドックスになってしまうのだ。

どうやら、プログラム言語を含め、言語には不動点がつきもので、そのことが、絶対に動くプログラムや、全ての真理を網羅した言語を作らせないようになっているらしい。

[PR]
by tnomura9 | 2017-11-15 23:25 | ラッセルのパラドックス | Comments(0)

λ記法とは何か

プログラマの視点からはλ記法は無名関数を記述できる一種の魔法だ。さらに、無名関数で再帰的定義を可能にする Y コンビネーターのようなものが出てくると、ますます魔法の呪文感が強くなってくる。

しかし、λ計算の本質を考えると、それは、等価な記号列を作るための簡潔な規則でしかない。つまり、λ計算の本質とは、ある文字列からそれと等価な文字列を作るための記号の置き換えの規則に過ぎないのだ。おまけにその規則は3つしかない。つまりα-変換、β-簡約、η-変換の3つだ。λ計算はこれらの規則を使って、等価な文字列を次々に作って行くという意味しかない。

α-変換と言っても単なる変数名の付け替えだし、β-簡約は変数を値で置き換えることで、η-変換は関数 X の変数を表に出すか出さないか、つまり λx.X x = X という置き換え規則でしかない。

λ記法でプログラムが書けるように思えるのは、コンパイラやインタープリターが勝手に文字列を解釈して実行するからだ。λ計算自体は単なる記号の置き換えでしかない。Haskell や Scheme でラムダ記法で書いたプログラムが動いたり動かなかったりするのは、その記号列をそれらの処理系が意味論的に翻訳する時の問題で、ラムダ記法は本来は意味論とは無関係な統語論的な規則なのだ。

統語論的という意味は、その記号列にプログラムとしての意味があるかどうかは無関係に、記号の置き換えのルールに従って記号を置き換えて等価な記号列に変形していくということだ。

たとえば、つぎのような Y コンビネータには (x x) のような関数の自己適用があったりして呪文感が半端ないが、

Y = (λf . (λx . f (x x)) (λx . f (x x)))

Y を任意の関数 g に関数適用して不動点 Yg を作り出すことの証明は、単に変数を引数で置き換えたり、その逆をやったり、変数の名前を付け替えたりしているに過ぎない。

Y g
= (λf . (λx . f (x x)) (λx . f (x x))) g(Yの定義より)
= (λx . g (x x)) (λx . g (x x))(λfのβ簡約、主関数をgに適用)
= (λy . g (y y)) (λx . g (x x))(α変換、束縛変数の名前を変える)
= g ((λx . g (x x)) (λx . g (x x)))(λyのβ簡約、左の関数を右の関数に適用)
= g (Y g)(第2式より)

これは中学校のときに習った2次方程式 ax^2 + bx + c = 0 の一般解を求める時の操作と同じことをしているだけだ。

したがって、関数の自己適用 (x x) のようなものもその意味を考える必要はないのだ。自己適用のある関数 (x x) を更に自己適用する ((f (x x)) (f (x x))) という不可思議な呪文も、単に文字列として捉えれば、それを等価変換していくと Y g = g (Y g) という不動点にたどり着くだけのことだ。

このようにλ計算そのものは単に記号の置き換えだと考えると、そこにはなんの不思議な事もない。しかし、関数の自己適用とは何かなどと、(x x) の意味論まで考えてしまうと、迷宮に迷い込んでしまう。

このように、λ計算は記号列の統語論的な変換規則なのだと割り切ってしまうと、その意味が理解しやすくなる。

[PR]
by tnomura9 | 2017-11-13 06:36 | ラッセルのパラドックス | Comments(0)

Haskell の Y コンビネータ

Yコンビネータの情報を探していたら Haskell でもできるという記事を見つけた。Haskell は型つきラムダ記法なので再帰関数はラムダ記法では定義できないはずだと不審に思ったが、次のように試してみた。

Prelude> let y x = x (y x)
Prelude> y (\f n -> if (n == 1) then 1 else (n * (f (n - 1)))) 5
120

...... 動いてしまった。

厳密には Y コンビネータ y の定義はラムダ記法ではないが、y x = x (y x) という動作をする高階関数の引数にラムダ記法の関数を与えると、第1引数にその関数自身がバインドされて再帰関数が定義できることが分かった。

Y コンビネータの威力が y x = x (y x) という不動点 (y x) で発揮されることが分かる。なぜそういうことが起きるのか考えてみた。

y x = x (y x)

なのでコンビネータ y は関数をひとつ引数に取る1変数関数だ。また、再帰関数を定義するときは x に上の階乗の例から分かるように関数と数値を引数に取る2変数関数を与える。そこで階乗を計算するための関数 g を g f x のように関数 f と整数 x を引数に取る2変数関数で表現してみる。すると、

y g = g (y g)

なので、(y g) を整数 3 に関数適用すると次のようになる。

(y g) 3 = (g (y g)) 3 = g (y g) 3

これは関数 g = \f n -> if n == 1 then 1 else n = n * (f (n - 1)) の f に (y g) がバインドされ、n に 3 がバインドされていることを示すので、

(y g) 3 = g (y g) 3 = 3 * ((y g) 2)

である。

同様に、(y g) 2 = 2 * ((y g) 1), (y g) 1 = 1

となるから、結局

(y g) 3 = g (y g) 3 = 3 * ((y g) 2) = 3 * 2 * ((y g) 1) = 3 * 2 * 1 = 6

と不動点 (y g) による再帰的計算が行われ 3 の階乗の 6 が計算される。つまり、高階関数 y が、

y x = x (y x)

のように不動点 (y x) を作り出す関数であれば、これを関数と整数の2つの引数をもつ2変数関数に関数適用すると、どのような再帰関数も作り出すことができることになる。この場合、どのような再帰関数を y コンビネータで定義しても、その(局所)関数名は (y x) という不動点になる。

Scheme で作った複雑な Y コンビネータも結局は y x = x (y x) という不動点を作り出す関数を定義したに過ぎない。Scheme の場合は Y コンビネータの定義もλ記法でできるので、型なしλ計算が再帰関数を記述できる根拠となる。しかし、Haskell でも y x = x (y x) のように y を定義するだけで、簡単に不動点を作り、無名再帰関数を記述できることが分かる。

追記

同じ発想で Scheme でもできないかと思ってやってみたが、スタックオーバーフローになってしまった。

y g = g (y g) = g (g (y g) = g (g (g (y g))) = ...

と永遠に β 変換をやり続けたためらしい。これを防ぐために前回の記事では Z コンビネータが使われていたようだが、これを y x = x (y x) の形にすることができなかった。β 変換の順序次第で無限ループになってしまうところが λ 計算の面白いところだ。真実はひとつではない?

[PR]
by tnomura9 | 2017-10-25 12:32 | ラッセルのパラドックス | Comments(0)

Y コンビネータの使い方

型なしラムダ計算の勉強のために Scheme をインストールした。

Linux : > sudo apt-get install mit-shceme
Mac : > brew install mit-scheme
Windows : Gaushe のインストーラをダウンロードした。(MIT Scheme が何故か動かなかった。)

型なしラムダ計算を学習しようと思ったのは、関数の自己適用がラッセルのパラドックスと関係があるのではないかと思ったからだ。ラムダ計算で関数の自己適用が現れるのは不動点コンビネータの Y コンビネータだ。ラムダ計算の教科書の説明では1ページくらいで解説してあるが、Scheme で実行しようとして躓いた。

そこでネット検索で、Y コンビネータで再帰的プログラムがかけることがわかった。再帰的プログラムの代表は階乗の計算だ。Scheme では次のように書ける。

1 ]=> (define (factorial n) (if (zero? n) 1 (* n (factorial (- n 1)))))

;Value: factorial

1 ]=> (factorial 5)

;Value: 120

しかしながら、これは自分自身を呼び出すのに関数名を必要としているので、ラムダ計算は使えない。

ところが、Y コンビネータを使うとラムダ計算でも再帰関数を定義できる。ラムダ計算の Y コンビネータは次のようになる。

Y = (λf . (λx . f (x x)) (λx . f (x x)))

何のことか分からないが、Scheme で記述した Y コンビネータは次のようになる。

1 ]=> (define yc (lambda (f) ((lambda (x) (f (lambda (n) ((x x) n)))) (lambda (x) (f (lambda (n) ((x x) n)))))))

;Value: yc

関数 (x x) に値を与えるための変数 n をλ記法で確保した以外はほぼ上のλ計算の Y コンビネータと同じものだ。Y コンビネータの一種で Z コンビネータというらしい。λ計算の Y コンビネータには任意の関数 g に関数適用することによって。

Y g = g (Y g)

となり、Y g が g の不動点になることがわかっている。とは言え、この Y でどうやって再帰関数を記述することができるのだろうか。

いろいろな解説をウェブで見たが、はっきりわからなかったのでこの記事を書いたわけだが、とにかく動くプログラムを作って動作させて見ることにした。Y コンビネータを使った階乗の関数は次のようになるが、実際に動作しているのが分かる。

1 ]=> (define fact (yc (lambda (f) (lambda (n) (if (zero? n) 1 (* n (f (- n 1))))))))

;Value: fact

1 ]=> (fact 5)

;Value: 120

そこで、階乗の計算を定義した部分を g とすると、上の定義は、

fact 5 = (Y g) 5 = g (Y g) 5

となるが、g(f, n) の引数 f に Yg がはいり、g の引数 n に5が入るので、

fact 5
= (g (Y g) 5)
= (if (zero? 5) 1 (* 5 ((Y g) 4)))
= 5 * ((Y g) 4)
= 5 * (g (Y g) 4)
= 5 * (if (zero? 4) 1 (* 4 ((Y g) 3)))
= 5 * 4 * ((Y g) 3)
...
= 5 * 4 * 3 * 2 * 1 * 1 = 120

と毎回関数 (Y g) が g の引数 f に入るので再帰関数の計算ができることになる。

要するに、λ記法で記述された関数に Y を関数適用すると第1引数を使ってその関数自身を利用するという、再帰的定義ができるのだ。無名関数であるλ記法で再帰的定義ができるという不思議な現象が起きてしまうが、このことによってλ記法はループのあるプログラムを作ることができるのが分かる。

Y コンビネータとは何かと考えるのは大変だが、Y コンビネータを使って再帰関数を定義する方法は意外に簡単だった。

[PR]
by tnomura9 | 2017-10-24 07:21 | ラッセルのパラドックス | Comments(0)