人気ブログランキング | 話題のタグを見る

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

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

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

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

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

このサイトでも Haskell を使ったラムダ計算のインタープリタを作ってみた。関連記事からどうぞ

by tnomura9 | 2017-12-21 14:03 | ラッセルのパラドックス | Comments(0)
<< Python を始めた λ式 (λ-term) >>