ゆるふわLazy K入門会 (第KI回)

ちゅーん @its_out_of_tune

歓声がｗｗｗ #ゆるK

さかばー @saka_bar

これがうわさのLazy Kの護符…! #ゆるK

ちゅーん @its_out_of_tune

iotaコンビネータの説明は無しか(´・ω・｀) #ゆるK

さかばー @saka_bar

30分遅れで到着しました。 #ゆるK

ちゅーん @its_out_of_tune

ちょまどコンビネータkwkr #ゆるK

さかばー @saka_bar

資料見られた。 #ゆるK

ちゅーん @its_out_of_tune

関数合成 S(KS)K #ゆるK

ふみ (DJ Monad) @fumieval

30分になったら少しIotaの話します #ゆるK

ちゅーん @its_out_of_tune

LazyK系の勉強、なんやかやラムダ計算の復習に近くなる。 #ゆるK

やがてクビになる @yomi322

iotaのおはなし #ゆるK

ちゅーん @its_out_of_tune

iota=S(SI(KS))(KK)

ちゅーん @its_out_of_tune

o = λx.x K S K とすると S = o (o o) K = (o o) o #ゆるK

ちゅーん @its_out_of_tune

SとKさえあれば夕方まで遊べる人たちが集まってる会場はここですか #ゆるK

ひらい @h_hirai

意味も分からず写経してほったらかしにしてたこいつを、今日はちゃんと読み直す日にしよう……。 https://t.co/fDRpeRTrh7 #ゆるK

ふみ (DJ Monad) @fumieval

ハッカソンタイム #ゆるK

ひらい @h_hirai

lazy> \x.\y.\f.(f x y) S(K(SS(KK)))(S(K(S(KK)S))(S(K(SI))K)) lazy> \a.\b.(S(SI(Ka))(Kb)) S(K(SS(KK)))(S(K(S(KK)S))(S(K(SI))K)) うーん…… #ゆるK

ちゅーん @its_out_of_tune

comp=S(KS)K succ=λn.λf.comp f (f n) この時lazyiの3とsucc (succ 1) が異なる式になったのがちょっと気になったのだけど、 >3 f n >(succ (succ 1)) f n で外延的に等価なのが解ったのでめでたし #ゆるK

ひらい @h_hirai

http://t.co/lK36lG7TlYストリーム で、 λ x y . x = K はそのままだし λ x y . y = KI もちょっと考えれば分かるけど λ f . f a b = S(SI(Ka))(Kb) とか、どこから出てくるのか……。 #ゆるK

irori @irori___

lazier が終わらない #ゆるK

ちゅーん @its_out_of_tune

SKIの勉強会でラムダ計算についてググるとかとんでもない屈辱

さかばー @saka_bar

不動点コンビネータの戯れている #ゆるK

ちゅーん @its_out_of_tune

ふみしゃんのデスクトップの鳥さんがすっげぇこっち見てる。

irori @irori___

別の処理系でも動かしてみたい方はお試しください http://t.co/GDA9Lorvu9 #ゆるK

とむ @masquerade0324

#ゆるK 楽しそう．あとで文さんの資料見よう．

ひらい @h_hirai

えっと、cons はこんなもんであきらめて、次は succ か……、な? #ゆるK