はじめに注意
コードの途中で「こんなのどこから出てきたんだよ」というようなメモの断片があるだろうが、それはgistに俺がコツコツ貯めておいたコンビネータ達である。
あのくらいは時間さえあれば簡単に作れたりするので、解説はしない(或いは、いくつかには初めから解説が付いている)。
あと、consの作り方は昔記事書いたのでそっち参照。
有限リストをどう実装するか
まず、リスト終端をどう判定するかを考える。
- ((a . True) (b . True) (c . True) (x . False) <ゴミ>)
- ((True . a) (True . b) (True . c) (False . x) <ゴミ>)
- (3 a b c <ゴミ>)
- 要素自体を述語に渡す
…等が考えられるが、選択肢4は任意の数列や関数列等、あらゆるデータが含まれ得るリストでは実用的ではない。
(これは、実用的なリストには必ずメタデータが必要ということでもある。)
また1は要素の生成が面倒(car、つまり先に登場するパラメータが変数でcdrがほぼ固定のため)、3はリスト自体の生成が面倒(リストを数えるのと要素数の後に付けるのに、データが2度必要なため)ということで、ここでは2の方法を採用することにする。
とりあえず使えるように
とりあえず、Lazy K インタプリタから渡される入力をこの形式のリストに変換する関数を作る。
ご存知のとおり、Lazy Kでは標準入力のバイト列が、(cons a (cons b (cons c ...)))という形でプログラムに渡される。
そして入力の末端の位置には256が入っており、以降はいくら次の要素を取っても256しか出てこない。
つまりこの無限リストのそれぞれを、car部がTrue(=K)であるようなconsセルのcdr部に入れて、最初に出てきた256の位置にcar部がFalse(=KI)であるような任意のconsを置いておけば良い。
まあ普通はcarとcdrが同じ場合は K<要素> とするのが楽なので今回もそうしよう。
さて、とりあえず標準入力を有限リストに変換する関数を arg2list = ll とおこう。
ちなみに、llと置く理由は以下を見ればわかる。
再帰が必要なコンビネータを作るときは、だいたい別のあるコンビネータが2回登場するような形でおきなおす。
lla = (<lt_eq><256>(aK))(K(K(KI)))(<cons>(<cons>K(aK))(ll(a(KI))))
= <lt_eq><256>(RKa)(K(K(KI)))(<cons>(<cons>K(RKa))(ll(R(KI)a)))
= S(K(<lt_eq><256>))(RK)a(K(K(KI))) (<cons>(A(<cons>K)(RK)a)(A(ll)(R(KI))a))
Sa(Kb)c -> acb
= S(K(<lt_eq><256>))(RK)a (K(K(KI))) (A<cons>(A(<cons>K)(RK))a)( SA(K(R(KI)))(ll) a)
= S(K(<lt_eq><256>))(RK)a (K(K(KI))) (S(A<cons>(A(<cons>K)(RK)))(SA(K(R(KI))))(ll)a)
S(SP(KQ))Ta -> SP(KQ)a(Ta) -> Pa(KQa)(Ta) -> PaQ(Ta)
= S(S( S(K(<lt_eq><256>))(RK) )(K(K(K(KI))))) (S(A<cons>(A(<cons>K)(RK)))(SA(K(R(KI)))(ll))) a
= S(S(S(K(<lt_eq><256>))(RK))(K(K(K(KI)))))(S(A<cons>(A(<cons>K)(RK)))(SA(K(R(KI)))(SIIl))) a
= S(S(S(K(<lt_eq><256>))(RK))(K(K(K(KI))))) (S(A<cons>(A(<cons>K)(RK))) (A(SA(K(R(KI))))(SII) l )) a
S(Ka)(S(Kb)c)d -> a(b(cd))
= S(K(S(S(S(K(<lt_eq><256>))(RK))(K(K(K(KI))))))) (S(K (S(A<cons>(A(<cons>K)(RK))))) (A(SA(K(R(KI))))(SII))) l a
= S(K(S(S(S(K(<lt_eq><256>))(SI(KK)))(K(K(K(KI))))))) (S(K(S(A<cons> (A(<cons>K)(SI(KK))) ))) (A (S(S(KS)K)(K(SI(K(KI))))) (SII))) l a
= S(K(S(S(S(K(<lt_eq><256>))(SI(KK)))(K(K(K(KI)))))))(S(K(S(S(K(<cons>))(S(K(<cons>K))(SI(KK))))))(S(K(S(S(KS)K)(K(SI(K(KI))))))(SII))) la
= S(K(S(S(S(K(<lt_eq><256>))(SI(KK)))(K(K(K(KI)))))))(S(K(S(S(K(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)))(S(K(S(K(S(SI(KK))))K))(SI(KK))))))(S(K(S(S(KS)K)(K(SI(K(KI))))))(SII))) la
<lt_eq><256> = S(S(K(S(K(S(SI(K(K(KI))))(KK)))))(SI(K(S(K(S(K(S(K(SI(KI)))))))(S(K(S(S(KS)(S(KK)S))(KK)))(S(K(S(S(KS)K)(K(S(KK)K))))(SI(K(S(K(S(K(S(K(SI))K))))(SS(KI)))))))))))(K<256>)
= S(S(K(S(K(S(SI(K(K(KI))))(KK)))))(SI(K(S(K(S(K(S(K(SI(KI)))))))(S(K(S(S(KS)(S(KK)S))(KK)))(S(K(S(S(KS)K)(K(S(KK)K))))(SI(K(S(K(S(K(S(K(SI))K))))(SS(KI)))))))))))(K(SII(SII(S(S(KS)K)I))))
= S(K(S(S(S(K(S(S(K(S(K(S(SI(K(K(KI))))(KK)))))(SI(K(S(K(S(K(S(K(SI(KI)))))))(S(K(S(S(KS)(S(KK)S))(KK)))(S(K(S(S(KS)K)(K(S(KK)K))))(SI(K(S(K(S(K(S(K(SI))K))))(SS(KI)))))))))))(K(SII(SII(S(S(KS)K)I))))))(SI(KK)))(K(K(K(KI)))))))(S(K(S(S(K(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)))(S(K(S(K(S(SI(KK))))K))(SI(KK))))))(S(K(S(S(KS)K)(K(SI(K(KI))))))(SII))) la
= SII(S(K(S(S(S(K(S(S(K(S(K(S(SI(K(K(KI))))(KK)))))(SI(K(S(K(S(K(S(K(SI(KI)))))))(S(K(S(S(KS)(S(KK)S))(KK)))(S(K(S(S(KS)K)(K(S(KK)K))))(SI(K(S(K(S(K(S(K(SI))K))))(SS(KI)))))))))))(K(SII(SII(S(S(KS)K)I))))))(SI(KK)))(K(K(K(KI)))))))(S(K(S(S(K(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)))(S(K(S(K(S(SI(KK))))K))(SI(KK))))))(S(K(S(S(KS)K)(K(SI(K(KI))))))(SII)))) a
よって
arg2list = SII(S(K(S(S(S(K(S(S(K(S(K(S(SI(K(K(KI))))(KK)))))(SI(K(S(K(S(K(S(K(SI(KI)))))))(S(K(S(S(KS)(S(KK)S))(KK)))(S(K(S(S(KS)K)(K(S(KK)K))))(SI(K(S(K(S(K(S(K(SI))K))))(SS(KI)))))))))))(K(SII(SII(S(S(KS)K)I))))))(SI(KK)))(K(K(K(KI)))))))(S(K(S(S(K(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)))(S(K(S(K(S(SI(KK))))K))(SI(KK))))))(S(K(S(S(KS)K)(K(SI(K(KI))))))(SII))))
また、別に確認としてもう一度やりなおしたら長さは同じだけど別の形のものが現れたので、参考までに記録しておく。
lla = (<lt_eq><256>(aK))(K(K(KI)))(<cons>(<cons>K(aK))(ll(a(KI))))
cons_ a b = (cons (cons K a) b) = S(K cons) (cons K) a b
= S(K(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)))(S(K(S(SI(KK))))K) a b
= <lt_eq><256>(RKa)(K(K(KI)))(<cons_>(aK)(ll(a(KI))))
= A(<lt_eq><256>)(RK)a(K(K(KI)))(<cons_>(RKa)(ll(R(KI)a)))
= A(<lt_eq><256>)(SI(KK))a(K(K(KI)))(<cons_>(SI(KK)a)(ll(SI(K(KI))a)))
= S(K(<lt_eq><256>))(SI(KK)) a (K(K(KI)))(S(K(<cons_>))(SI(KK))a( SII l (SI(K(KI)) a) ))
S(S(K(S(KS)K))a)(Kb)xy -> ax(by)
= S(K(<lt_eq><256>))(SI(KK)) a (K(K(KI)))(S(K(<cons_>))(SI(KK))a( S(S(K(S(KS)K))(SII))(K(SI(K(KI))))la))
= S(K(<lt_eq><256>))(SI(KK)) a (K(K(KI)))(S (S(K(<cons_>))(SI(KK))) (S(S(K(S(KS)K))(SII))(K(SI(K(KI))))l) a)
S(SP(KQ))Ta -> SP(KQ)a(Ta) -> Pa(KQa)(Ta) -> PaQ(Ta)
(P = S(K(<lt_eq><256>))(SI(KK)), Q = K(K(KI)), T = S(S(K(<cons_>))(SI(KK)))(S(S(K(S(KS)K))(SII))(K(SI(K(KI))))l) )
= S(S (S(K(<lt_eq><256>))(SI(KK))) (K (K(K(KI))) ))( S(S(K(<cons_>))(SI(KK)))(S(S(K(S(KS)K))(SII))(K(SI(K(KI))))l) )a
S(Ka)(S(Kb)c)d -> a(b(cd))
= S(K( S(S(S(K(<lt_eq><256>))(SI(KK)))(K(K(K(KI))))) ))(S(K( S(S(K(<cons_>))(SI(KK))) ))( S(S(K(S(KS)K))(SII))(K(SI(K(KI)))) )) l a
cons_ a b = (cons (cons K a) b) = S(K cons) (cons K) a b
= S(K(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)))(S(K(S(SI(KK))))K) a b
= S(K(S(S(S(K(<lt_eq><256>))(SI(KK)))(K(K(K(KI)))))))(S(K(S(S(K(S(K(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)))(S(K(S(SI(KK))))K)))(SI(KK)))))(S(S(K(S(KS)K))(SII))(K(SI(K(KI)))))) la
<lt_eq><256> = S(S(K(S(K(S(SI(K(K(KI))))(KK)))))(SI(K(S(K(S(K(S(K(SI(KI)))))))(S(K(S(S(KS)(S(KK)S))(KK)))(S(K(S(S(KS)K)(K(S(KK)K))))(SI(K(S(K(S(K(S(K(SI))K))))(SS(KI)))))))))))(K<256>)
= S(S(K(S(K(S(SI(K(K(KI))))(KK)))))(SI(K(S(K(S(K(S(K(SI(KI)))))))(S(K(S(S(KS)(S(KK)S))(KK)))(S(K(S(S(KS)K)(K(S(KK)K))))(SI(K(S(K(S(K(S(K(SI))K))))(SS(KI)))))))))))(K(SII(SII(S(S(KS)K)I))))
= S(K(S(S(S(K(S(S(K(S(K(S(SI(K(K(KI))))(KK)))))(SI(K(S(K(S(K(S(K(SI(KI)))))))(S(K(S(S(KS)(S(KK)S))(KK)))(S(K(S(S(KS)K)(K(S(KK)K))))(SI(K(S(K(S(K(S(K(SI))K))))(SS(KI)))))))))))(K(SII(SII(S(S(KS)K)I))))))(SI(KK)))(K(K(K(KI)))))))(S(K(S(S(K(S(K(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)))(S(K(S(SI(KK))))K)))(SI(KK)))))(S(S(K(S(KS)K))(SII))(K(SI(K(KI)))))) la
= SII(S(K(S(S(S(K(S(S(K(S(K(S(SI(K(K(KI))))(KK)))))(SI(K(S(K(S(K(S(K(SI(KI)))))))(S(K(S(S(KS)(S(KK)S))(KK)))(S(K(S(S(KS)K)(K(S(KK)K))))(SI(K(S(K(S(K(S(K(SI))K))))(SS(KI)))))))))))(K(SII(SII(S(S(KS)K)I))))))(SI(KK)))(K(K(K(KI)))))))(S(K(S(S(K(S(K(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)))(S(K(S(SI(KK))))K)))(SI(KK)))))(S(S(K(S(KS)K))(SII))(K(SI(K(KI))))))) a
よって
arg2list = SII(S(K(S(S(S(K(S(S(K(S(K(S(SI(K(K(KI))))(KK)))))(SI(K(S(K(S(K(S(K(SI(KI)))))))(S(K(S(S(KS)(S(KK)S))(KK)))(S(K(S(S(KS)K)(K(S(KK)K))))(SI(K(S(K(S(K(S(K(SI))K))))(SS(KI)))))))))))(K(SII(SII(S(S(KS)K)I))))))(SI(KK)))(K(K(K(KI)))))))(S(K(S(S(K(S(K(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)))(S(K(S(SI(KK))))K)))(SI(KK)))))(S(S(K(S(KS)K))(SII))(K(SI(K(KI)))))))
この形式のリストを lazy k インタプリタの出力、あるいは戻り値として返す関数はmapによって可能なので今はまだ作らない。
さて、これから filter やら map やら色々な関数を作るが、その度に再帰など書きたくないので、 foldr を最初に作ることにする。
また、以後Boolとa型の値のペアの配列を[a]と略記することにする。
Axyz = S(KS)Kxyz = x(yz), Rxy = S(K(SI))Kxy = yx とおいておく。
foldr :: (a -> b -> b) -> b -> [a] -> b
foldr step zero list = if (caar list)
then step (cdar list) (foldr step zero (cdr list))
else zero
foldr = ff、step = t、zero = z、list = l とおくと
ffszl = lKK (s (lK(KI)) (ffsz(l(KI)))) z
Trueの場合とfalseの場合を入れ替える ( not a = a False True = a(KI)K )
= lKK (KI)K z (t (lK(KI)) (fftz(l(KI))))
= lKK(KI)K z (t (<cons>K(KI)l) (fftz(R(KI)l)))
= lKK(KI)K z (t (<cons>K(KI)l) (SA(K(R(KI)))(fftz)l))
= lKK(KI)K z (t (<cons>K(KI)l) (SA(K(R(KI)))(SIIftz)l))
= lKK(KI)K z (t (<cons>K(KI)l) ( SA(K(SI(K(KI)))) (SIIftz) l ))
a(bcde) <- Aa(bcd)e <- A(Aa)(bc)de <- A(A(Aa))bcde <- S(K(S(K(S(Ka)))))bcde
= lKK(KI)K z (t (<cons>K(KI)l) (S(K(S(K(S(K (SA(K(SI(K(KI))))) ))))) (SII)ftz l ))
b(ac) <- Abac <- SA(Ka)bc
= <cons>KK l (KI)K z (SA(K(<cons>K(KI))) tl (S(K(S(K(S(K (SA(K(SI(K(KI))))) ))))) (SII)ftz l ))
= <cons>(KI)K (<cons>KK l) z ( S (SA(K(<cons>K(KI)))t) (S(K(S(K(S(K (SA(K(SI(K(KI))))) ))))) (SII)ftz) l )
= S(K(<cons>(KI)K))(<cons>KK) lz ( S (SA(K(<cons>K(KI)))t) (S(K(S(K(S(K (SA(K(SI(K(KI))))) ))))) (SII)ftz) l )
P(Qt)(Ttz) <- P(AKQtz)(Ttz) <- P((AKQ)tz)(Ttz) <- S(K(S(KP)))(AKQ)tz(Ttz) <- S(S(KS)(S(K(S(KP)))(AKQ)))Ttz
S(S(KS)a)bcd -> acd(bcd)
S(S(KS)(S(K(S(KP)))(S(KK)Q)))Ttz -> P(Qt)(Ttz)
( P = S, Q = SA(K(<cons>K(KI))), T = S(K(S(K(S(K(SA(K(SI(K(KI))))))))))(SII)f
= S(K(<cons>(KI)K))(<cons>KK) lz ( S(S(KS)(S(K(S(KS)))(S(KK)(SA(K(<cons>K(KI)))))))(S(K(S(K(S(K(SA(K(SI(K(KI))))))))))(SII)f) t zl )
P(Qt)(Ttz) <- P(AKQtz)(Ttz) <- P((AKQ)tz)(Ttz) <- S(K(S(KP)))(AKQ)tz(Ttz) <- S(S(KS)(S(K(S(KP)))(AKQ)))Ttz
S(S(KS)a)bcd -> acd(bcd)
S(S(KS)(S(K(S(KP)))((S(KS)K)KQ)))Ttz -> P(Qt)(Ttz)
( P = S, Q = SA(K(<cons>K(KI))), T = S(K(S(K(S(K(SA(K(SI(K(KI))))))))))(SII)f
= S(K(<cons>(KI)K))(<cons>KK) lz ( S(S(KS)(S(K(S(KS)))(S(KK)(SA(K(<cons>K(KI)))))))(S(K(S(K(S(K(SA(K(SI(K(KI))))))))))(SII)f) t zl )
adc(bcd) <- Sa(Kc)d(bcd) <- A(Sa)Kcd(bcd) <- S(S(KS)(A(Sa)K))bcd <- S(S(KS)(S(K(Sa))K))bcd
S(S(KS)(S(K(Sa))K))bcd -> adc(bcd)
= S(S(KS)(S(K(S( S(K(<cons>(KI)K))(<cons>KK) )))K)) ( S(S(KS)(S(K(S(KS)))(S(KK)(SA(K(<cons>K(KI)))))))(S(K(S(K(S(K(SA(K(SI(K(KI))))))))))(SII)f) t) zl
P(Q(Ta)b) <- P(AQTab) <- S(K(S(KP)))(AQT)ab <- S(K(S(KP)))(S(KQ)T)ab
(P = S(S(KS)(S(K(S(S(K(<cons>(KI)K))(<cons>KK))))K)), Q = S(S(KS)(S(K(S(KS)))(S(KK)(SA(K(<cons>K(KI))))))), T = S(K(S(K(S(K(SA(K(SI(K(KI))))))))))(SII)
= S(K(S(K( S(S(KS)(S(K(S(S(K(<cons>(KI)K))(<cons>KK))))K)) )))) (S(K( S(S(KS)(S(K(S(KS)))(S(KK)(SA(K(<cons>K(KI))))))) ))( S(K(S(K(S(K(SA(K(SI(K(KI))))))))))(SII) )) ftzl
= S(K(S(K(S(S(KS)(S(K(S(S(K(S(SI(K(KI)))(KK)))(S(SI(KK))(KK)))))K))))))(S(K(S(S(KS)(S(K(S(KS)))(S(KK)(S(S(KS)K)(K(S(SI(KK))(K(KI))))))))))(S(K(S(K(S(K(S(S(KS)K)(K(SI(K(KI))))))))))(SII)))ftzl
よって
f = SII(S(K(S(K(S(S(KS)(S(K(S(S(K(S(SI(K(KI)))(KK)))(S(SI(KK))(KK)))))K))))))(S(K(S(S(KS)(S(K(S(KS)))(S(KK)(S(S(KS)K)(K(S(SI(KK))(K(KI))))))))))(S(K(S(K(S(K(S(S(KS)K)(K(SI(K(KI))))))))))(SII))))
foldr = SII(S(K(S(K(S(S(KS)(S(K(S(S(K(S(SI(K(KI)))(KK)))(S(SI(KK))(KK)))))K))))))(S(K(S(S(KS)(S(K(S(KS)))(S(KK)(S(S(KS)K)(K(S(SI(KK))(K(KI))))))))))(S(K(S(K(S(K(S(S(KS)K)(K(SI(K(KI))))))))))(SII))))
とりあえず
cons_ a b = (cons (cons K a) b) = S(K cons) (cons K) a b
= S(K(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)))(S(K(S(SI(KK))))K) a b
としておいて、
foldr cons (K <258>) (cons_ 2 (cons_ 1 (cons_ 0 (K(K(KI))))))
で実験してみる。(ちなみに、「K(K(KI))」は「(cons (cons (KI) (KI)) (cons (KI) (KI)))」と同値。)
こうすると、評価後には
cons 2 (cons 1 (cons 0 (K <258>)))
となり、結果出力にはバイナリで「0x02 0x01 0x00」が出て、終了コードは2になるはずである。
ちなみにコード全体はこんなかんじ。
K(
SII(S(K(S(K(S(S(KS)(S(K(S(S(K(S(SI(K(KI)))(KK)))(S(SI(KK))(KK)))))K))))))(S(K(S(S(KS)(S(K(S(KS)))(S(KK)(S(S(KS)K)(K(S(SI(KK))(K(KI))))))))))(S(K(S(K(S(K(S(S(KS)K)(K(SI(K(KI))))))))))(SII))))
(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK))
(K (S(S(KS)K)(S(S(KS)K)(SII(SII(S(S(KS)K)I))))) )
(S(K(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)))(S(K(S(SI(KK))))K) (S(S(KS)K)I)
(S(K(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)))(S(K(S(SI(KK))))K) I
(S(K(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)))(S(K(S(SI(KK))))K) (KI)
(K(K(KI)))
)))
)
…で、このコードは意図した通りに実行されたので、どうやらfoldrは完成っぽい。
次に、foldrの詳しいテストも兼ねてarg2listをテストしてみる。
foldr cons (K<256>) (arg2list arg)
= S(K(<foldr><cons>(K<256>)))<arg2list> <arg>
は入力を出力にそのまま垂れ流すはずである。
以下がコード。
# catらしきもの
# <compose> (<foldr> <cons>(<cons> <256> <256>)) <arg2list>
S(K(
# <foldr>
SII(S(K(S(K(S(S(KS)(S(K(S(S(K(S(SI(K(KI)))(KK)))(S(SI(KK))(KK)))))K))))))(S(K(S(S(KS)(S(K(S(KS)))(S(KK)(S(S(KS)K)(K(S(SI(KK))(K(KI))))))))))(S(K(S(K(S(K(S(S(KS)K)(K(SI(K(KI))))))))))(SII))))
# <cons>
(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK))
# <cons> <256> <256> = K<256>
(K(SII(SII(S(S(KS)K)I))))
))
# <arg2list>
(SII(S(K(S(S(S(K(S(S(K(S(K(S(SI(K(K(KI))))(KK)))))(SI(K(S(K(S(K(S(K(SI(KI)))))))(S(K(S(S(KS)(S(KK)S))(KK)))(S(K(S(S(KS)K)(K(S(KK)K))))(SI(K(S(K(S(K(S(K(SI))K))))(SS(KI)))))))))))(K(SII(SII(S(S(KS)K)I))))))(SI(KK)))(K(K(K(KI)))))))(S(K(S(S(K(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)))(S(K(S(K(S(SI(KK))))K))(SI(KK))))))(S(K(S(S(KS)K)(K(SI(K(KI))))))(SII)))))
これも意図したとおりに動作した。どうやら両方とも問題なさそうだ。
ご存知のとおり、foldrでmapやfilterやfoldl等様々な関数が実装できるので、別の記事で解説する。
…つもりだったけど、gist見てもらえばいいか。
