Prolog をべんきょうしています
先週の木曜日、大学の図書室で『Think CでMacintoshプログラミングとか何年前ｗｗｗ』『TAOCPがある……!!』などと暇を潰していたら、大量のProlog本に混じり『Prologの技芸 (以下 TAOP*1 )』を発見。すぐさま「ひとは若いうちにScheme, Prolog, Haskell に触れなければならない！」と云う電波を受信し、その電波の導くままにPrologの勉強を決意したのでした。
ちなみに、図書室にには三冊のTAOPがあって、浮世絵の表紙が生存しているのは一冊だけで、残りはカバーがないのが一冊、更に背が死んでいて図書室が貼り替えたものが一つ。
次の日、MacBookを学校に持ち込み、TAOPを早速借りながら勉強をはじめる。表紙が生き残ってるのを借りる。しかし、前読んだ人の書き込みや髪の毛が大量に含まれていてびっくりする。
しかし、id:pi8027から何故か早朝に『類推論できました』と云う報告を貰ったので、まずはYadorigi*2さんを苛める。バグをひとつ見付ける。すぐ修正される。
授業がハネて暇だったので、恰度ぱいさんが秋葉原に向かっているとのことで、人生第三回目の秋葉原に足を踏み入れる。そして初リナカフェなう。
リナカフェのトイレが電波がわるくて悲しかった。あとFONとか云う公衆無線LANに接続しようとするも、一旦登録したIDで接続出来なくて、もういっかい登録しようとボタンを押してもログイン画面に引き戻されてしまい、けっきょく接続できない。万死。
そんなこんなしている内にぱいさんがくる。やどりぎさんまわりと類推論・型推論のはなしをきく。ユニフィケーションとモナドとか、モナドの中での不純なデバグ方法など。あと色々裏話をきく。Typing Haskell in Haskell は読むべきと云う情報をもらう。ありがとうぱいさん。
やどりぎさんを苛めるぞ！とおもったけど、ちゃんと
type S f g x = f x (g x) type K f g = f type I = S K K
が正しく推論されていてぼくは感動する。感動してもうバグを見付けられなくなる。僕のまけです。
型理論のはなしの流れで、いけがみさんがついったーで紹介していた論文(CiNii 論文 - 型理論I (<特集>関数型プログラミングと計算の基礎), CiNii 論文 - 型理論II, CiNii 論文 - 型理論III, CiNii 論文 - 型理論IV)で読んだことを掻い摘んではなそうとするも、掻い摘みすぎてちゃんと説明できなかった……。
で、この論文に載っているλ-Cubeを実装したいなぁ、と思い立つ。Haskellでやると大変そうなので、そうだ、こういう公理から推論させるならユニフィケーションもあるPrologで実装しよう！と、モチベーションがさらにあがる。
あと、ぱいさんにSandS入力の洗脳を受け、左Shiftキーを殺される。結果、入力に非常に時間が掛かる様になり発狂、その様子をみたぱいさんが爆笑しやがる。今回の会合でわかったことは、ぱいさんの沸点が異常に低いということである。っていうかテスト期間中に徹夜で類推論書いてる高校生とか終わってますね……！！変態さんめ。
その後id:nihaさんと合流して、おいしい親子丼やさんにいく。とてもおいしい。どのくらいおいしいのかと云うと、にはさんが『高いだけのことはある』を連発していてみもふたもない。あとにはさんが一番場数ふんでるくせに、道に迷いやがる。mjspに行くときも迷っていたので、にはさんは迷う才能があると思う。
で、親子丼やさんではCurry-Howardが すごいなぁというはなしとか、Template Haskell のはなしとか、なんかそういうはなしをする。
ぱいさんは後半からAgdaを勉強しはじめていて、にはさんが依存型について説明をする。ぱいさんが「こんさんもAgdaやりましょう」と云うのだけど、ぼくにはHaskellと云う伴侶がいるし、Prologに浮気しはじめたばかりなのに三股をかけるのはちょっと……と思ったので心に止めておくに留める。
「Prologで型推論書いたら簡単そうなので書こうと思います」と云ったらにはさんに「それは簡単すぎるなー」みたいなことを云われたので、口惜しいからHaskellでPrologを実装することを心に誓う。
と云うわけで、Haskell で Prolog を実装しその上で型推論を実装するべくPrologを勉強しています。
練習問題を解いてみた答えは GitHub - konn/TAOP-Exercises: The Answer code for "The Art Of Prolog(2nd Ed)" Exercises. に忘れなければ同期してあります。更新されてなかったらサボってると思ってせっついてもかまいません。せっつかなくてもかまいません。自明ですね。
「アセンブリに始まり、Fortran、Algol、Pascal、そしてAdaへと居たる言語発達史の主流をなす言語は……」と云う記述があって、時代を感じた。もうCはある時代の筈なんだけど……
実際のところ、ユニフィケーションが型推論の中心らしいので、Prologを実装しちゃえば半分は仕事終わりで、残りは規則を記述するだけになるわけで。たのしみである。
あと、野望としては、Haskell で実装した Prolog で実装した Scheme で Haskell を書きたいのだけど、多分 Scheme 止まりになる気がしている。っていうかそもそも Scheme まで根気が保つかわからない。
まあそんなこんな。
