Skip to content

Instantly share code, notes, and snippets.

@lo48576

lo48576/README

Created October 14, 2012 09:15
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save lo48576/3888085 to your computer and use it in GitHub Desktop.
Save lo48576/3888085 to your computer and use it in GitHub Desktop.
Download ZIP
useful combinators and memos about Lazy K
Raw
README
ここは、俺がこつこつ貯めたSKIコンビネータのいろいろなものを保管しておくための場所です。
無限リスト用のコンビネータは https://gist.github.com/3369073 に(たぶん解説といっしょに)置いてあります。
こちらには、無限リスト用以外のコンビネータを置いておきます。
ちょっとHaskell的な記法で解説すると、Lazy Kでは普通のやり方では無限リストしか表現できません。
たとえばLazy Kインタプリタの入力では、終端に256を使うことになっていますが、任意の数値やコンビネータを含むリストではこの手法は使えません。
そこで、各要素にメタデータ(リスト終端かどうか、Bool)を付加することにしました。
通常は
[a]
[a, b, c, d, ...] <- 終われない
ですが、
[(Bool,a)]
[(True,a), (True,b), (True,c), (True,d), (False, 任意のゴミデータ)]
とすれば有限長のリストを表現可能です。
ここのファイル群は基本的に、リストを扱うときにはこの(後者の)形式のリストを扱います。
従来の(前者の)形式のリスト、つまり無限リスト(ストリームとも)は前述のとおり、旧バージョンの方に保管してありますのでそちらを参照してください。
Raw
arg2list.txt
Lazy K インタプリタから渡される標準入力を有限リストに変換するコンビネータ。
さて、有限リストをどう実装するか。
まず、リスト終端をどう判定するかを考える。
1. ((a . True) (b . True) (c . True) (x . False) <ゴミ>)
2. ((True . a) (True . b) (True . c) (False . x) <ゴミ>)
3. (3 a b c <ゴミ>)
4. 要素自体を述語に渡す
等が考えられるが、選択肢4は任意の数列や関数列等、あらゆるデータが含まれ得るリストでは実用的ではない。
(これは、実用的なリストには必ずメタデータが必要ということでもある。)
また1は要素の生成が面倒(carが変数でcdrがほぼ固定のため)、3はリスト自体の生成が面倒(リストを数えるのと
要素数の後に付けるのに、データが2度必要なため)ということで、ここでは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)))))))
****************
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))))
= 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によって可能なのでここには書かない。
Raw
foldr.txt
filter やら map やら色々な関数を作ることになるが、その度に再帰など書きたくないので、
foldr を最初に作ることにする。
また、以後Boolとa型の値のペアの配列を[a]と略記することにする。
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は完成っぽい。
ついでに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とarg2listの実装は正しそうだ。
Raw
number_comparation.txt
ISZERO n = n (<and> <false>) <true>
<and><false> = K(KI)
= n(K(KI))K = S(SI(K(K(KI))))(KK) n
ISNOTZERO n = n (<or> <true>) <false>
<or><true> = KK
= n(KK)(KI) = S(SI(K(KK)))(K(KI)) n
ここで、
<n-m> = <m><PRED><n> = MINUS m n = 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))))))))) m n
とする。引数の順番おかしいけど、これ作ったとき面倒だったから放っておいたんだ。覚悟してね！
m >= n のとき n-m == 0 であるから
GE m n = ISZERO (MINUS m n) = S(K(S(K ISZERO))) MINUS m n
= 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)))))))))) m n
よって
GE = 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))))))))))
m < n のとき n-m != 0 であるから
LT m n = ISNOTZERO (MINUS m n) = S(K(S(K ISNOTZERO))) MINUS m n
= S(K(S(K(S(SI(K(KK)))(K(KI))))))(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)))))))))) m n
よって
LT = S(K(S(K(S(SI(K(KK)))(K(KI))))))(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))))))))))
S(K(Sa))K
m <= n のとき m-n = 0 であるから
LE m n = ISZERO (MINUS n m) = S(K(S(K ISZERO))) MINUS n m = S(K(S( S(K(S(K ISZERO))) MINUS )))K m n
= 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 m n
よって
LE = 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
LE m n = S(K(S( S(K(S(K ISZERO))) MINUS )))K m n = S( S(K(S(K ISZERO))) MINUS ) (Km) n
= S(S(K(S(K ISZERO))) MINUS)(Km)n = 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)))))))))))(Km)n
よって
LE m = 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)))))))))))(Km)
m > n のとき m-n != 0 であるから
GT m n = ISNOTZERO (MINUS n m) = S(K(S(K ISNOTZERO))) MINUS n m = S(K(S( S(K(S(K ISNOTZERO))) MINUS )))K m n
= S(K(S(S(K(S(K(S(SI(K(KK)))(K(KI))))))(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 m n
よって
GT = S(K(S(S(K(S(K(S(SI(K(KK)))(K(KI))))))(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
Raw
recursive_formula.txt
漸化式を有限リストが可能な形式で実現するのだ！！
これによって、有限リスト用の関数で漸化式を扱えるようになる。地味に便利。
<rec(F)_n><Car><Car> = <True>
<rec(F)_n>(n<Cdr>)<Car> = <F_n>
<recur> F n = <cons_> n (<recur> F (F n))
rrfn = <cons_>n(rrf(fn))
= <cons_> n (rrf(fn))
= <cons_> n (SII rf(fn))
= <cons_> n (A(SII rf)fn)
= S<cons_>(A(SII rf)f)n
S(K(S(Ka)))bcd -> a(bcd)
= S<cons_>(S(K(S(KA)))(SII) rff)n
= S<cons_>(S(K(S(K(S(KS)K))))(SII) rff)n
a(bcdd) <- a(SS(KI)(bc)d) <- a(A(SS(KI))bcd) <- S(K(S(Ka)))(A(SS(KI))b)cd
= S(K(S(K( S<cons_> ))))(A(SS(KI)) (S(K(S(K(S(KS)K))))(SII))) rfn
= S(K(S(K(S(S(K(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)))(S(K(S(SI(KK))))K))))))(S(K(SS(KI)))(S(K(S(K(S(KS)K))))(SII))) rfn
= SII(S(K(S(K(S(S(K(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)))(S(K(S(SI(KK))))K))))))(S(K(SS(KI)))(S(K(S(K(S(KS)K))))(SII)))) fn
<recur> = SII(S(K(S(K(S(S(K(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)))(S(K(S(SI(KK))))K))))))(S(K(SS(KI)))(S(K(S(K(S(KS)K))))(SII))))
テストしてみる。
# K(<ret_list>(SII(SII(S(S(KS)K)I)))(<recur><SUCC>(KI)))
K(
# <ret_list>
S(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
# <256>
(SII(SII(S(S(KS)K)I)))
(
# <recur>
SII(S(K(S(K(S(S(K(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)))(S(K(S(SI(KK))))K))))))(S(K(SS(KI)))(S(K(S(K(S(KS)K))))(SII))))
# <SUCC> <0>
(S(S(KS)K)) (KI)
# <*3> <1>
(S(K (S(S(KS)K)(S(S(KS)K)I)) )) I
)
)
おｋ。
Raw
ski_combinators_list.csv
We can make this file beautiful and searchable if this error is corrected: It looks like row 20 should actually have 5 columns, instead of 6. in line 19.
Kab,``kab,a,a,"[a]Car, True, 0, 2引数の選択"
SKab,```skab,b,b,"[b]Cdr, False, 2引数の選択"
KIab,```kiab,b,b,"[b]Cdr, False, 2引数の選択"
SS(K(K(SK)))ab,````ss`k`k`skab,ab(sk),``ab`sk,"[ab<True>]AND"
SS(K(K(KI)))ab,````ss`k`k`KIab,ab(ki),``ab`ki,"[ab<True>]AND"
S(K(SI))KKab,`````s`k`sikkab,akb,``akb,"[a<True>b]OR"
S(SI(K(SK)))(KK)a,```s``si`k`sk`kka,a(sk)k,``a`skk,"[a<False><True>][<Cons><False><True>]NOT"
S(SI(K(KI)))(KK)a,```s``si`k`ki`kka,a(ki)k,``a`kik,"[a<False><True>][<Cons><False><True>]NOT"
I,i,I,i,"1"
SKK,``skk,I,i,"Iコンビネータ(η簡約)"
S(S(KS)K)n,``s``s`kskn,"<n+1>",,"[n+1]後継数(+1)"
SI(K(S(S(KS)K)))mn,````si`k`k``s`kskmn,"<m+n>",,"[m+n]加算"
m(S(S(KS)K))n,``m`s``s`kskn,"<m+n>",,"[m+n]加算"
S(KS)Kmn,````s`kskmn,"<m*n>",,"[m*n]乗算"
S(Km)n,``s`kmn,"<m*n>",,"[m*n]乗算"
mn,`mn,"<n^m>",,"[n^m]累乗"
SIIn,```siin,"<n^n>",,"[n^n]累乗"
SII(S(K(S(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK))))(S(K(SIK(S(S(KS)K))))(SII)))(KI),,,,"チャーチ数のリスト[0,1,2,3,...]"
SII(S(K(S(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK))))(S(K(SIK(S(S(KS)K))))(SII)))n,,,,"チャーチ数のリスト[n,n+1,n+2,...]"
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)))))))n,```s`k`s`k`s`k``si`ki``s`k``s``s`ks``s`kks`kk``s`k``s``s`ksk`k``s`kkk``si`k``s`k`s`k``s`k`sik``ss`kin,,,"[n-1]減算(-1)",``s`k`s`k`s`k``si`ki``s`k``s``s`ks``s`kks`kk``s`k``s``s`ksk`k``s`kkk``si`k``s`k`s`k``s`k`sik``ss`ki
S(K(SI(KK)))(S(SI(K(SI(K(KI)))))(K(S(SI(K(KI)))(K(SII(S(K(S(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK))))(S(K(SIK(S(S(KS)K))))(SII)))(KI))))))n,```s`k``si`kk``s``si`k``si`k`ki`k``s``si`k`ki`k````sii``s`k`s``s``s`k``s`ksk``s`ks``s`k`sik`kk``s`k```sik`s``s`ksk``sii`kin,,,"[n-1]減算(-1)",``s`k``si`kk``s``si`k``si`k`ki`k``s``si`k`ki`k````sii``s`k`s``s``s`k``s`ksk``s`ks``s`k`sik`kk``s`k```sik`s``s`ksk``sii`ki
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)))))))))mn,```s`k``s`k`s`k`s`k``si`ki``s`k``s``s`ks``s`kks`kk``s`k``s``s`ksk`k``s`kkk``si`k``s`k`s`k``s`k`sik``ss`kimn,,,"[n-m]減算"
n(K(KI))K,``n`k`kik,,,"[n==0]数値比較(0判定)"
S(SI(K(K(KI))))(KK)n,,,,"[n==0]数値比較(0判定)"
n(KK)(KI),``n`kk`ki,,,"[n!=0]数値比較(非0判定)"
S(SI(K(KK)))(K(KI))n,,,,"[n!=0]数値比較(非0判定)"
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)))))))))))))Kmn,,,,"[m<=n]数値比較"
S(K(S(K(S(SI(K(KK)))(K(KI))))))(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))))))))))mn,,,,"[m<n]数値比較"
S(K(S(S(K(S(K(S(SI(K(KK)))(K(KI))))))(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)))))))))))))Kmn,,,,"[m>n]数値比較"
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))))))))))mn,,,,"[m>=n]数値比較"
S(Ka)I,``s`kai,a,a,"簡約"
S(S(KS)(KI)),,K(SI),`k`si,"簡約"
SIIa,```siia,aa,`aa,"[aa]1引数の複製"
S(K(SI))Kab,,,ba,"[ba]2引数の逆転"
SI(Ka)b,,ba,`ba,"[ba]2引数の逆転"
SSKab,````ss`kiab,aba,``aba,"[aba]2引数の編集"
SS(KI)ab,````sskab,abb,``abb,"[abb]2引数の編集"
S(S(KS)(S(KK)S))(KK)abc,,acb,``acb,"[acb]3引数の交換"
Sa(Kb)c,```sa`kbc,acb,``acb,"[acb]3引数の交換"
S(K(Sa))Kbc,,acb,``acb,"[acb]3引数の交換"
S(K(SI(Ka)))bc,,bca,"``bca,[bca]3引数の循環"
S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)abc,,cab,``cab,"[cab]Cons, 3引数の循環"
S(SI(Ka))(Kb)c,,cab,``cab,"[cab]Cons, 3引数の循環"
S(K(S(SI(Ka))))Kbc,,cab,``cab,"[cab]Cons, 3引数の循環"
S(KS)Kabc,`````s`kskabc,a(bc),`a`bc,"[a(bc)]関数適用"
S(Ka)bc,```s`kabc,a(bc),`a`bc,"[a(bc)]関数適用"
S(K(S(K(SI))K))abc,````s`k``s`k`sikabc,c(ab),`c`ab,"[c(ab)]3引数の交換"
SI(K(ab))c,```si`k`abc,c(ab),`c`ab,"[c(ab)]3引数の交換"
S(K(S(K(S(K(SI))K))))(S(K(SI))K)abc,,c(ba),`c`ba,"[c(ba)]3引数の交換"
S(KK)Kabc,`````s`kkkabc,a,a,"[a]3引数の変更"
K(Ka)bc,```k`kabc,a,a,"[a]3引数の選択"
KKabc,````kkabc,b,b,"[b]3引数の選択"
K(KI)abc,````k`kiabc,c,c,"[c]3引数の選択"
S(KS)(KK)abc,`````s`ks`kkabc,c(bc),`c`bc,"[c(bc)]3引数の編集"
SSabc,````ssabc,bc(abc),``bc``abc,"[bc(abc)]3引数の編集"
S(K(SI))abc,````s`k`siabc,c(abc),`c``abc,"[c(abc)]3引数の編集"
S(S(KS)K)abc,````s``s`kskabc,b(abc),`b``abc,"[b(abc)]3引数の編集"
S(S(KS)K)I(S(KS)K)abcd,```````s``s`kski``s`kskabcd,a(bcd),`a``bcd,"[a(bcd)]4引数の交換、BBB (B = S(KS)K)"
S(K(S(Ka)))bcd,,a(bcd),`a``bcd,"[a(bcd)]4引数の交換"
S(S(K(S(KS)K))a)(Kb)xy,,ax(by),``ax`by,""
S(K(S(KS)))(S(KK))abcd,,ab(cd),``ab`cd,"[ab(cd)]4引数の交換"
S(KS)(S(KK)a)bcd,,ab(cd),``ab`cd,"[ab(cd)]4引数の交換"
S(S(KS)(KS))abcd,,cd(abcd),``cd```abcd,"[cd(abcd)]4引数の編集"
S(K(S(Ka)))(S(Kb))cd,,a(b(cd)),`a`b`cd,"[a(b(cd))]4引数の交換"
S(Ka)(S(Kb)c)d,,a(b(cd)),`a`b`cd,"[a(b(cd))]4引数の交換"
S(S(KS)a)bcd,,acd(bcd),```acd``bcd,"[acd(bcd)]4引数の編集"
K(S(KK)K)abcd,`````k``s`kkkabcd,b,b,"[b]4引数の選択"
S(K(S(KS)K))(S(Ka)b)cde,,a(bc)(de),``a`bc`de,"[a(bc)(de)]5引数の交換"
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment