- Lazy K は関数だけでできている
- どの関数も関数 1 個を引数にとって、関数 1 個を返す関数
- 関数 x を y を引数にして呼ぶのを xy と書く
-
- xy して得られた関数を z を引数にして呼ぶのは (xy)z だが、演算の優先順位的に括弧は省略できるので、xyz と書ける
- 関数 z を、xy して得られた関数を引数にして呼ぶのは z(xy)
- unlambda 記法だと、それぞれ ``xyz、`z`xy
- 関数は S と K と I がある
- Sxyz -> xz(yz)
- Sxy は引数 z を与えると xz(yz) を返す関数
- Sx は引数 y を与えると「引数 z を与えると xz(yz)を返す関数」を返す関数
- S は引数 x を与えると「引数 y を与えると「引数 z を与えると xz(yz)を返す関数」を返す関数」を返す関数
- Kxy -> x
- Kx は引数 y を与えると x を返す関数
- K は引数 x を与えると「引数を 1 個与えると x を返す関数」を返す関数
- Ix -> x
- あと Iota 記法とか Jot 記法とかで * とか 0 とか 1 とか出てくるけど略
- s と k は大文字と同じ。i は unlambda 記法で使われているときは I と同じ、Iota 記法で使われているときは別の意味になる。区別はできるらしい。
- # で 1 行コメント
- 遅延評価されるので、使わない引数は実行されない
- 例えば Kxy の y が無限ループだった時に無限ループにならない
- ある条件で再帰を止めたいときに楽。
- Grass なんかだと、再帰を実行する方の関数はすぐに評価されないよう工夫しなければいけない
- Lazy K プログラムにできるのは、標準入力を読んで標準出力に書き出すことだけ
- 標準入力の文字列はチャーチ数のリストになる
- 入力の終わりはチャーチ数で表した 256 が無限に続くリスト
- プログラムはチャーチ数のリストを引数にとって、チャーチ数のリストを返す関数
- チャーチ数は関数だけで数値を表す方法で、リストは関数だけで書けるので、関数を引数にとって関数を返す関数になっている
- チャーチ数のリストと同じように振る舞えれば、中身は何でもよい
- 得られたチャーチ数のリストは文字列に直されて出力される
- 256 以上の数値は出力の終わりを意味する
- そこでプログラムは終了するので、続きはリストでなくてもよい。
- prelude.scm で定義されている end-of-output は 256 を返す定数関数だが、car の引数になっても cdr の引数になっても 256 を返すので、(cons 256 256) と同じ振る舞いをする。ということで、出力の終わりとして扱える。
- prelude.scm に () が定義されているが、チャーチ数のリストとして振る舞わないので、出力用のチャーチ数のリストの終わりに入れるとエラー終了になる。
- "文字列の終端の数値-256" がプログラムの終了ステータスになる
- リストの要素がチャーチ数以外だと、ランタイムエラー
- というわけで、標準入力をそのまま標準出力に返すプログラム
I
- リスト
- リストは、引数が K の時先頭要素 a を、引数が KI の時先頭要素を除いたリスト b を返す関数とする
- 流儀は多分複数あるけど、標準入出力で使われている方式でやるのが都合がいいので、これを使う
- この流儀のリストは、引数が f の時 fab を計算する関数でいい
- K と KI 以外を引数に与えた場合、当方は一切関知しません。
- S、K、I で書くと S(SI(Ka))(Kb)
# リストに f を渡す
S(SI(Ka))(Kb)f
=(SI(Ka))f((Kb)f)
=If((Ka)f)b
=fab
# f が K の時
Kab
=a
# f が KI の時
(KI)ab
=((KI)a)b
=Ib
=b
fab
=(fa)b
=(SI(Ka)f)b # (fa) について、f を引数の立場に追いやる
=((SI(Ka))f)b
=(S(SI(Ka))(Kb))f # f を括弧の外に
-
- car はリスト l に引数 K を渡す関数
- つまり、(car l)=lK
- S、K、I で書くと SI(KK)
- cdr はリスト l に引数 KI を渡す関数
- つまり、(cdr l)=l(KI)
- S、K、I で書くと SI(K(KI))
- cons は引数に a と b を渡すと S(SI(Ka))(Kb) を返す関数
- S、K、I で書くと S(S(KS)(S(KK)(S(KS)(S(K(SI))K))))(KK)
- というわけで、例
# 入力の最初の 1 文字を消して出力するプログラム。cdr そのもの
SI(K(KI))
- チャーチ数
- チャーチ数が何なのかは、はてなキーワードとか Wikipedia とか読んでください
- 0 は KI
- 1 は I
- 2 は S(S(KS)K)I
- チャーチ数に 1 を足す関数 1+ は ( (1+ n) f x)=(f(n f x)) なので S(S(KS)K)
- 足し算 n+m は m を n 回 1+ すると考えて、(n 1+ m) から SI(K(S(S(KS)K)))
- 掛け算 n*m は「関数 f を m 重に適用する関数」を n 重に適用すると考えて ( (* n m) f x)=(n (m f) x) から S(KS)K
- 巾乗 n^m は、m に関して数学的帰納法を使って mn が示せる
- 例 : 標準入力の先頭に 0x01 をつけたものを出力
S(S(KS)(S(KK)(S(KS)(S(K(SI))K))))(KK)I # (cons 1)
S(K(S(SI(KI))))K # 単純化すると
- 真偽値と条件分岐
- true は K、false は KI とすると (真偽値 true節 false節) で条件分岐できる
- 遅延評価されるので、使う方しか実行されない
- prelude.scm によると、チャーチ数を比較して条件分岐するのは面倒くさい。
- 面倒くさくなったのであとは略