2020-03-02

今日は型なしラムダ計算を使って「足し算」を発明するプログラムを書いてみた。

参考資料はWikipediaのLambda calculus。

機械学習といえばニューラルネットワークが人気だが、いまいち好きになれないので適当に思いついたことをやっている。前はWall-following問題をHaskellのGADTをガッツリ使って解くことをやっていたが、Typeableを使いすぎてよく分からなくなってしまったので放置。ここ最近数日かけて読んでいた前述のLambda calculusの頁を読んで思いの外面白いと思ったので、自作してみたいと思ったのがきっかけ。

プログラマー(俺)のインプットが少なければ少ないほどいいと思ったので untyped lambda calculusの実装にチャレンジ。概念は非常に簡単で、ラムダ式 (lambda term)は以下の3つのみから定義される:

• variable(変数): x
• abstraction(抽象): \x. M
• application(適用): M N

ここでM, Nは任意のラムダ式。つまりラムダ式は再帰的に定義される。

これをHaskellのdata typeに落とし込むのは極めて簡単である。

type Var = String

data Term
  = Var Var
  | Abs Var Term
  | App Term Term

それで、数や四則演算はどうするかというと、Church-encoding なるものがある。かいつまんで説明すると、自然数は以下のラムダ式で表現する。

0 := \f. \x. x
1 := \f. \x. f x
2 := \f. \x. f (f x)
...
n := \f. \x. f ((n-1) f x)

つまり2つの引数fとxを取り、xにfを適用する回数が自然数に対応するわけである。fに(+1)を、xに(普通の意味の)0を代入することで普通の自然数を得ることができる。

Church-encodingでエンコードされた自然数同士の足し算は以下のラムダ式で行える:

plus := \g. \h. \f. \x. (g f) (h f x)

nが自然数ならばn fは「fをn回適用する関数」となるため、上記の定義は「fをh回xに適用した後、更にfをg回適用する関数」となり、つまりg + h回fを適用する関数となるので足し算になっている。

で、今回はこのplus関数を見つけ出せるかということで、遺伝的アルゴリズムを導入してしっちゃかめっちゃかやってみたが、結論から言うとものすごい時間をかけるとできそうだということがわかった。

そもそもなんでこんなことをやったのかというと、Church-encodingは実用には向かないということで、どれくらい向かないのか試してみたかったから。足し算のような基礎的な演算を「発明」するのに大きな手間がかかるなら、もっと複雑なWall-following問題のような問題を解くプログラムを発明させることはできないだろうと思ったからである。

数十分間ぶん回して初めて足し算が発明されたので、正直厳しいと思う。でも面白かったからもうちょっといろいろやりたい。