Skip to content

Instantly share code, notes, and snippets.

@lo48576

lo48576/README

Created August 16, 2012 10:17
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/3369073 to your computer and use it in GitHub Desktop.
Save lo48576/3369073 to your computer and use it in GitHub Desktop.
Download ZIP
useful combinators (for infinite lists) and memos about Lazy K
Raw
README
These files are combinators (functions) with SKI combinator for infinite lists, descriptions which shows how to make them, and useful combinators.
Now there are only files about infinite combinators and related memos.
However, these memos will NOT be UPDATED (even if some data is wrong), so you should see new version ( http://gist.github.com/3888085 ) if you would like to use combinators written in these files.
ここには無限リスト(ストリームとも?)に関するコンビネータ、あるいはその作り方のメモ、それらの作業に便利な汎用的なコンビネータを置いてあります。
しかし有限リストを実装する方法を見つけたので、新しいgist ( http://gist.github.com/3888085 ) に移行します。
何故ここを残しておくかというと、無限リストと有限リストで名前が被るコンビネータが多いからです(mapとかfilterとか諸々)。
たとえこちらに間違いがあっても、もう基本的には修正しない(新しいものを追加する可能性はあるが)ので、基本的に新しいバージョンの方を参照してください。
あと、上の英語になんか変なのがあったら、誰か指摘してくれると嬉しいです。俺の母国語は日本語なんで…
Raw
ski_combinators_list.csv
We can make this file beautiful and searchable if this error is corrected: It looks like row 2 should actually have 1 column, instead of 5. in line 1.
*** this is an old version! ***
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(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,,,,"[n-1]減算(-1)"
SI(K(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))))))))mn,,,,"[n-m]減算"
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,````sskab,aba,``aba,"[aba]2引数の編集"
SS(KI)ab,````ss`kiab,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(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(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(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引数の編集"
S(K(S(KS)K))(S(Ka)b)cde,,a(bc)(de),``a`bc`de,"[a(bc)(de)]5引数の交換"
Raw
ski_filter_inf.txt
* あてになるテストは未完了なので注意されたし(軽いテストでは意図した通りの挙動だった) *
filter_inf :: (a -> Bool) -> [a] -> [a]
p : 述語。(p elem) が TRUE = K を返すとき要素は保持され、 FALSE = KI = SK を返す場合は、戻されるリストからは削除される。
list : 無限リスト(ストリームとも)。
filter_inf p list = (p (car list)) (cons (car list)) I (filter p (cdr list))
filter_inf = ff, list = l
ffpl = p (lK) (<cons> (lK)) I (ff p (l(KI)))
= p (RKl) (<cons>(RKl)) I (ff p (R(KI)l))
= Sp<cons>(RKl) I (A(ffp)(R(KI))l)
= SS(K<cons>)p (RKl) I (A(ffp)(R(KI))l)
= SS(K<cons>)p (RKl) I (A(ffp)(SI(K(KI)))l)
S(S(K(S(KS)K))a)(Kb)xy -> ax(by)
= S(S(K(S(KS)K))(SS(K<cons>)))(K(RK))pl I (SA(K(SI(K(KI))))((SII)fp)l)
= S(S(K(S(KS)K))(SS(K<cons>)))(K(SI(KK))) pl I ( S(S(KS)K)(K(SI(K(KI)))) ((SII)fp)l)
= S(S(K(S(KS)K))(SS(K<cons>)))(K(SI(KK))) pl I ( S(K(S(K( S(S(KS)K)(K(SI(K(KI)))) )))) (SII) f p l)
(axy)I(cxy) <- RI(axy)(cxy) <- A(A(RI))axy(cxy) <- S(S(KS)(A(A(RI))a))cxy
S(S(KS)(A(A(RI))a))cxy -> S(KS)(A(A(RI))a)x(cx)y -> KSx(A(A(RI))ax)(cx)y -> S(A(RI)(ax))(cx)y -> A(RI)(ax)y(cxy) -> RI(axy)(cxy) -> axyI(cxy)
= S(S(KS)(A(A(RI)) (S(S(K(S(KS)K))(SS(K<cons>)))(K(SI(KK)))) )) (S(K(S(K(S(S(KS)K)(K(SI(K(KI))))))))(SII) f) p l
= S(S(KS)(S(K(S(K(SI(KI)))))(S(S(K(S(KS)K))(SS(K<cons>)))(K(SI(KK)))))) (S(K(S(K(S(S(KS)K)(K(SI(K(KI))))))))(SII) f) p l
= A(S(S(KS)(S(K(S(K(SI(KI)))))(S(S(K(S(KS)K))(SS(K<cons>)))(K(SI(KK))))))) (S(K(S(K(S(S(KS)K)(K(SI(K(KI))))))))(SII)) f p l
= S(K(S(S(KS)(S(K(S(K(SI(KI)))))(S(S(K(S(KS)K))(SS(K<cons>)))(K(SI(KK))))))))(S(K(S(K(S(S(KS)K)(K(SI(K(KI))))))))(SII)) f p l
= S(K(S(S(KS)(S(K(S(K(SI(KI)))))(S(S(K(S(KS)K))(SS(K( S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK) ))))(K(SI(KK))))))))(S(K(S(K(S(S(KS)K)(K(SI(K(KI))))))))(SII)) f p l
= S(K(S(S(KS)(S(K(S(K(SI(KI)))))(S(S(K(S(KS)K))(SS(K(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)))))(K(SI(KK))))))))(S(K(S(K(S(S(KS)K)(K(SI(K(KI))))))))(SII)) f p l
よって
filter_inf = SII(S(K(S(S(KS)(S(K(S(K(SI(KI)))))(S(S(K(S(KS)K))(SS(K(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)))))(K(SI(KK))))))))(S(K(S(K(S(S(KS)K)(K(SI(K(KI))))))))(SII)))
Raw
ski_map_inf.txt
map_inf :: (a -> Bool) -> [a] -> [a]
(以下の説明は ski_filter.txt のものと同じ)
p : 述語。(p elem) が TRUE = K を返すとき要素は保持され、 FALSE = KI = SK を返す場合は、戻されるリストからは削除される。
list : 無限リスト(ストリームとも)。
map_inf p list = cons (p (car list)) (map p (cdr list))
map_inf = ff, list = l
ffpl = <cons>(p(lK))(ffp(l(KI)))
= <cons>(p(RKl))(ffp(R(KI)l))
= <cons>(Ap(RK)l)(A(ffp)(R(KI))l)
= <cons>(R(RK)(Ap)l)(R(R(KI))(A(ffp))l)
= <cons>(A(R(RK))Apl)( A(R(R(KI)))A (ffp) l)
S(K(S(Ka)))bcd -> a(bcd)
= <cons>(A(R(RK))Apl)( S(K(S(K( A(R(R(KI)))A )))) ffp l)
= S(K(S(K<cons>))) (A(R(RK))A) p l ( S(K(S(K( A(R(R(KI)))A )))) ffp l)
S(S(KS)a)bcd -> acd(bcd)
= S(S(KS) (S(K(S(K<cons>)))(A(R(RK))A)) ) (S(K(S(K(A(R(R(KI)))A))))ff) p l
= S(S(KS)(S(K(S(K<cons>)))(S(K(R(RK)))(S(KS)K))))( S(K(S(K(A(R(R(KI)))A)))) f f ) p l
abb <- (ab)(KIab) <- SSKab
SSKab -> Sa(Ka)b -> ab(Kab) -> abb
SS(KI)ab -> Sa(KIa)b -> ab(Ib) -> abb
= S(S(KS)(S(K(S(K<cons>)))(S(K(SI(K(RK))))(S(KS)K))))( SS(KI) (S(K(S(K(A(R(R(KI)))A))))) f ) p l
= S(S(KS)(S(K(S(K<cons>)))(S(K(SI(K(SI(KK)))))(S(KS)K))))( (SS(KI)(S(K(S(K(S(K(R(R(KI))))(S(KS)K))))))) f ) p l
= A ( S(S(KS)(S(K(S(K<cons>)))(S(K(SI(K(SI(KK)))))(S(KS)K)))) ) (SS(KI)(S(K(S(K(S(K(R(R(KI))))(S(KS)K))))))) f p l
= S(K(S(S(KS)(S(K(S(K<cons>)))(S(K(SI(K(SI(KK)))))(S(KS)K)))))) (SS(KI)(S(K(S(K(S(K(SI(K(SI(K(KI))))))(S(KS)K))))))) f p l
= S(K(S(S(KS)(S(K(S(K( S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK) ))))(S(K(SI(K(SI(KK)))))(S(KS)K)))))) (SS(KI)(S(K(S(K(S(K(SI(K(SI(K(KI))))))(S(KS)K))))))) f p l
= S(K(S(S(KS)(S(K(S(K(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)))))(S(K(SI(K(SI(KK)))))(S(KS)K))))))(SS(KI)(S(K(S(K(S(K(SI(K(SI(K(KI))))))(S(KS)K))))))) fpl
よって
map_inf = SII(S(K(S(S(KS)(S(K(S(K(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)))))(S(K(SI(K(SI(KK)))))(S(KS)K))))))(SS(KI)(S(K(S(K(S(K(SI(K(SI(K(KI))))))(S(KS)K))))))))
Raw
ski_number_comparation.txt
*** this is an old version! ***
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
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 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
ski_pred.txt
PRED :: Church -> Church
減算(-1)を実現する
リスト [0,0,1,2,3,4,..]を利用する
PRED 0 = P(KI) -> KI
PRED 1 = PI -> KI
PRED 2 = P(S(S(KS)K)I) -> I
...
Axyz = S(KS)Kxyz -> S(Kx)yz -> x(yz)
Rxy = S(K(SI))Kxy -> SI(Kx)y -> yx
SUCC n = S(S(KS)K)n = SAn
Pn = n (R<Cdr>) (S(SI(K(KI)))(K<list0>)) <Car>
= R<Car>(n (R<Cdr>) (S(SI(K(KI)))(K<list0>)) )
= SI(K<Car>) (S(SI(K(R<Cdr>)))(K(S(SI(K(KI)))(K<list0>))) n)
= S(K(SI(KK))) (S(SI(K(SI(K(KI)))))(K(S(SI(K(KI)))(K<list0>)))) n
<list><0> = [0, 1, 2, 3, 4, ...]
<list>n = S(SI(Kn))(K(<list>(S(S(KS)K)n)))
= S(SI(Kn))(K(<list>(SAn)))
<list> = ff とおく。
ffn = S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK) n (ff(SAn))
= S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK) n (A(SIIf)(SA)n)
= S( S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK) ) ( A(SIIf)(SA) ) n
= S( S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK) ) ( A(SIIf)(SA) ) n
Sa(Kb)c->acb より SA(K(SA))<list>->A<list>(SA)
SA(K(SA))(SIIf) -> A(SIIf)(K(SA)(SIIf)) -> A(SIIf)(SA)
= S( S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK) ) ( SA(K(SA))(SIIf) ) n
SIK(SA) -> I(SA)(K(SA)) -> SA(K(SA))
= S(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)) ( SIK(SA)(SIIf) ) n
= S(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)) ( A(SIK(SA))(SII)f ) n
= A (S(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK))) ( A(SIK(SA)) (SII)) fn
= S(K (S(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK))) ) ( S(K(SIK(S(S(KS)K)))) (SII)) fn
= S(K(S(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK))))(S(K(SIK(S(S(KS)K))))(SII)) fn
よって
<list> = 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)))
= S(K(S(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK))))(S(K(SIK(S(S(KS)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)))
<list><0> = <list0> = 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)
検算 <list>:
S (K(S(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)))) (S(K(SIK(S(S(KS)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))) <Car> <0> fx
S (K(S(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)))) (S(K(SIK(S(S(KS)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))) K KI fx
-> K(S(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK))) (S(K(S(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK))))(S(K(SIK(S(S(KS)K))))(SII))) (S(K(SIK(S(S(KS)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)))) K KI fx
-> S (S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)) (S(K(SIK(S(S(KS)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)))) K KI fx
-> S (S(K(S(KS)K))(S(KS)(S(K(SI))K))) (KK) K (S(K(SIK(S(S(KS)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))) K) KI fx
-> S(K(S(KS)K))(S(KS)(S(K(SI))K))K ((KK) K) (S(K(SIK(S(S(KS)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))) K) KI fx
-> S (K(S(KS)K)) (S(KS)(S(K(SI))K)) K K (S(K(SIK(S(S(KS)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))) K) KI fx
-> K(S(KS)K) K (S(KS)(S(K(SI))K)K) K (S(K(SIK(S(S(KS)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))) K) KI fx
-> S(KS)K (S(KS)(S(K(SI))K)K) K (S(K(SIK(S(S(KS)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))) K) KI fx
-> S (KS) (S(K(SI))K) K (K (S(K(SIK(S(S(KS)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))) K)) KI fx
-> KSK (S (K(SI)) K K) (K (S(K(SIK(S(S(KS)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))) K)) KI fx
-> S (K(SI)K(KK)) (K (S(K(SIK(S(S(KS)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))) K)) KI fx
-> S (SI(KK)) (K (S(K(SIK(S(S(KS)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))) K)) KI fx
-> SI(KK)(KI) (K (S(K(SIK(S(S(KS)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))) K)(KI)) fx
-> I(KI)(KK(KI)) (K (S(K(SIK(S(S(KS)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))) K)(KI)) fx
-> KIK (K (S(K(SIK(S(S(KS)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))) K)K) fx
-> I fx
-> fx
Pn = S(K(SI(KK)))(S(SI(K(SI(K(KI)))))(K(S(SI(K(KI)))(K<list0>)))) 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(KS)K))(S(KS)(S(K(SI))K)))(KK))))(S(K(SIK(S(S(KS)K))))(SII)))(KI)))))) n
P = 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))))))
つまり
P n = (- n 1)
Raw
ski_recurrence_formula.txt
<rec(F)> :: a -> [a]
F :: a -> a
PREDと同じ要領で、漸化式を実現する
F : 組み込み。外に出すのは面倒だったのでとりあえずこのままで。いつかなんとかする(かも)
n : 初期値。初項。
<rec(F)_n><Car> = <F_n>
<F_(n+1)> = F(<F_n>)
別の表現をすれば
<rec(F)_n> = [n,(F n), (F (F n)), (F (F (F n))), ...]
<rec>n = S(SI(Kn))(K(<rec>(Fn)))
<rec> = ff とおく。
ffn = S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK) n (ff(Fn))
= S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK) n (A(SIIf)Fn)
= S( S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK) ) ( A(SIIf)F ) n
= S( S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK) ) ( A(SIIf)F ) n
Sa(Kb)c->acb より SA(K(Sa))<list>->A<list>(SA)
SA(KF)(SIIf) -> A(SIIf)(KF(SIIf)) -> A(SIIf)F
= S( S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK) ) ( SA(KF)(SIIf) ) n
= S(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK))( A(SA(KF))(SII)f ) n
= A (S(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK))) (A(SA(KF))(SII)) f n
= S(K (S(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK))) ) (S(K (SA(KF)) ) (SII)) f n
= S(K(S(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK))) ) (S(K(S(S(KS)K)(KF)))(SII)) f n
= S(K(S(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK))))(S(K(S(S(KS)K)(KF)))(SII)) f n
よって
<rec(F)_n> = SII(S(K(S(S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK))))(S(K(S(S(KS)K)(K F )))(SII))) n
つまり
<rec(F)_n><Car> = n
<rec(F)_n><Cdr><Car> = F n
<rec(F)_n><Cdr><Cdr><Car> = F (F n)
...
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment