１ヶ月くらい前に少し遊んだLazyKですが再びやる気が出てきたので今回はHelloWorld出力を目指します。
概要
まずLazyKについて復習的なところから。今回はお話中心。
LazyK
- 3つの関数 S K I と括弧のみを使う
I x = x #恒等写像
K x y = x #定数関数
S x y z = (x z)(y z) #関数の適用
- 標準入力が
チャーチ数のスコットエンコードされたリストにエンコードされ
関数の引数として渡される。
-
関数の返り値が逆にデコードされて標準出力に。
-
使用するにも、処理系を実装するにも、コンビネータ論理の知識が必要
→SKI？ チャーチ数？ スコットエンコード？ コンビネータ理論？
謎が多いので色々調べたのですがHelloWorldまでに必要な勉強のおおまかな流れは以下のような感じです
HelloWorldまでの道
- コンビネーターって何？
- コンビネータとラムダ計算
- ラムダ計算でチャーチ数とか演算
- ラムダ計算でスコットエンコードリスト
- T[]変換でLazyKに回帰
- 謎
- HelloWorld!
実は現状３あたりまでやって停止中。ついでに型付ラムダ計算とかをやったので力尽きました。
コンビネーター理論
なんとなくイメージでは「有限個の原始関数を使った計算モデル」という感じ？説明できるほどわかってないのでWikipedia:コンビネータ理論参照。
SKIコンビネータ
LazyKで使われる３つの関数SKIを原始関数とする計算モデル。
詳しくはWikipedia:SKIコンビネータ計算を参照ください。
形式的定義では
以下の３つのみがコンビネータ項
x : 変数
p : 原始的関数(SKIのどれか)
(E1 E2) : 項の適用(E1 E2は項)
SKIコンビネータ計算はラムダ計算を単純化したひとつの計算モデルで、任意のラムダ項に対し、それと外延的に等価かつ同じ自由変数を持つ。逆も成り立つ。つまりラムダ計算で計算可能であることとSKIコンビネータで計算可能であることは同値。だそうです。さらに、ラムダ計算可能であることとチューリングマシンで計算可能なことは同値なのでSKIコンビネータはチューリング完全。だからLazyKもチューリング完全。
また T[]変換というものによりラムダ項をSKIコンビネータ項に（機械的に）変換することができます。
で、どうやってプログラム書くのかということですが、使えるのはSKIという関数と括弧、変数のみ。数字は？？
関数だけで自然数を扱う
数字がないのにどうするの？ということですがチャーチ数と言うものを使います。
以下は定義
0:(K I)
1:(I)
2:(S (S (K S) K) I)
3:(S (S (K S) K) (S (S (K S) K) I))
こんな感じで関数のかたまりを数と対応付けます。
プログラム書く
雰囲気はチャーチ数表現のASCIIコードのリストを作ってそれを出力する関数を書く。するとHelloWorldが出せます。
しかしどうすればいいのか全くわからない。そこでT[]変換でラムダ項はSKIコンビネータ項に変換可能というのを利用し、もう少しわかりやすいラムダ計算の力を借ります。というわけでHelloWorldは次回以降に持ち越し。