<   2017年 12月 ( 3 )   > この月の画像一覧

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

ラムダ計算の項 (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)