追記: 本家にマージされました。GitHub - cho45/net-irc: Ruby IRC library (Client, Server and many IRC gateways to webservice)を使ったほうがいいです。Listsに対応したtig.rbがあると便利な気がしたので、朝からがんばって改造してみました。 とても充…

30分プログラム、その695。2文字のコマンドを探してみましょう。 Unixのコマンドは、lsとかddのように短いものが多い印象があります。では、実際に1文字や2文字のコマンドは何個ぐらいあるのか調べてみました。 使い方 1文字コマンドはわりと少ない。 $ pyth…

30分プログラム、その694。パスワードジェネレータを作ってみました。 世の中には色々な基準でパスワードを作ってくれるジェネレータがありますが、今回は単純なランダムな文字列を生成するやつを作りました。 使い方 $ perl gen_pwd.pl Yncw":o-dSGRn ]L5>5…

id:mzp:20091113:passwdでパスワードジェネレータを作っといてなんだけどapgっていうパスワードジェネレータいいよ。 apg -tで発音可能なパスワード(pronounceable password)を作ってくれる。 $ apg -t UlOcKocvai (Ul-Oc-Koc-vai) gepUdifuk$ (gep-Ud-if-uk…

30分プログラム、その693。Erlangでechoサーバを作ってみた。 なにかいいネタないかなぁ、と思いつつプログラミングErlangを開いたら、ちょうどgen_tcpを解説したページだったので、Erlangでechoサーバを作ってみました。脈絡ないとか言わないで。 使い方 $ …

30分プログラム、その692。OCamlでダイクストラ法。 "OCaml ダイクストラ法"でググると、昔ボクが書いた不完全な実装がヒットしてしまう。(ダイクストラ法を実装しようとしたら、よくわからないものになった - みずぴー日記) この不完全な実装を放置するのは…

30分プログラム、その691。HOASによるラムダ式。 id:keigoiさんに、HOAS(Higher order abstract syntax)なるものを教えてもらいました。 詳しいことは、http://homepages.inf.ed.ac.uk/ratkey/unembedding.pdfに書いてあるらしいです。今のところの理解は、 …

30分プログラム、その690。中置記法から逆ポーランド記法への変換。 簡単かと思いきや、意外と難しい。とてもじゃないけど、括弧の対応はできなかった。 使い方 scala> val infix = new Infix() infix: Infix = Infix@a32e6f scala> infix += 1 scala> infix…

最近、Coqで型付きラムダ計算を定義して、ProgressやPreservationを証明するという遊びにはまっています。とてもおもしろいので、みんなもやるといいと思うよ。で、最近、substitution lemmaの証明にチャレンジして、もろくも敗れ去りました。よくよく見直し…

30分プログラム、その689。ML系の言語といえばバリアント、バリアントと言えば木構造なので、2分木を作ってみました。 そのうち、B木とかに拡張できたらいいね。 使い方 - val t = List.foldl (curry insert) empty [10,3,1,4]; val t = Branch (10,Branch (…

30分プログラム、その688。/dev/randomから読み込むプログラム。聞くところによると/dev/randomは無限に乱数が書いてある(ように見える)ファイルらしいです。 聞いたことはあっても試したことがないので、読み込むプログラムを作ってみました。数字を延々と…

30分プログラム、その687。JsonValidatorを作ってみた。 最近、とある事情で、他の人にJsonのバリデータを作らせて、そのコードレビューしてます。それはそれで楽しいけれど、やっぱり自分でコードが書きたい! というわけで、Jsonバリデータを作ってみました…

30分プログラム、その686。一番長いファイル名を探すプログラム。 とあるディレクトリでlsしたら、結果が一行で表示されてしまいました。これはきっと、すごく長いファイル名があるせいで、複数行表示ができなくなっているに違いない! というわけで、ファイ…

30分プログラム、その685。ディレクトリ・トラバース用ユーティリティ。指定したディクトリから、条件を満したファイルを探しだすコマンドを書くための、ユーティリティ関数を作りました。 loop()-> receive {T,Path} -> io:format("~p - ~p~n",[T, Path]), …

定理の中で使うProp(命題)は、関数的に定義するよりも、Inductiveに定義したほうが証明が楽らしいですよ。 要約 Inductiveに定義したPropのほうが使いやすいらしい Inductiveに定義したPropの各名前は、applyできる Inductive Xを定義するとX_indが自動で定…

30分プログラム、その684。昔にやった仲間はずれの判定を、もう一度やってみました。 問題はhttp://ja.doukaku.org/53/を参考に、前回の回答は仲間外れの判別 - みずぴー日記を見てください。 使い方 *Main> classify [1,1,1,1,1] Same 1 *Main> classify [1…

今日もTypes and Programming Languages (The MIT Press)に載っている定理の証明です。 type_dec 補題を定義する際に、以下のような定義が必要になりました。 Definition type_dec : forall t1 t2 : type, {t1 = t2} + {t1 <> t2}. で、これを証明するために…

30分プログラム、その683。シーザ暗号化をやってみました。 シーザ暗号がなんぞやかは、シーザー暗号 - Wikipediaを参考にしてください。 使い方 (* 3文字ずらす * - val (f,g) = make 3; val f = fn : string -> string val g = fn : string -> string (* …

前回までで作った型付け規則を元に、Types and Programming Languages (The MIT Press)に載っている「Inversion of the typing relation補題」の証明にチャレンジしました。Inversion of the typing relation補題は Lemma LambdaRel : forall (x : string) (…

30分プログラム、その682。ScalaでSEND+MORE=MONEYを解いてみました。 Scalaのforはモナドらしいです。モナドと言えばリストモナド、リストモナドと言えばSEND+MORE=MONEYです。 というわけで、SEND+MORE=MONEYを解いてみました。 使い方 $ fsc SendMoreMone…

とうとう、型づけ規則の定義ができました。 というわけで、簡単な補題を証明しようとしたところ、string_decがうまく扱えなくて挫折しました。証明したかった補題はTAPLに載っている「Inversion of the typing relation」という補題です。TAPL曰く、Immediat…

前回作ったラムダ式の上に、evalを定義しました。 覚えたこと 全部、末尾に「〜らしいよ」ってつけて読んでくれるとうれしいです。 再帰関数の定義は、かなり厳しい制約があるっぽい よく分からないこと 最初、termを与えると値になるまで評価するevalを書い…

ボクのアルバイト先が今までOCamlでどんなソフトウェアを開発してきたかのまとめが公開されています。 2009-10-21ボクは2007年のFX会社のサービスのあたりからアルバイトをさせてもらっているので、ほぼ全部知っているはずなんですが、こうして改めて見ると…

30分プログラム、その681。let*と名前付きletをマクロで書いてみました。 輪講のためにSICPの演習問題を解いてたら、「let*と名前付きletをコード変換で実現しろ」というのがでてきました。 そのとき、パターンマッチが使えなくてフラストレーションが溜りま…

バリアントでラムダ式を作って、その上でsubstituteを定義してみました。目指してるのは単純型付きラムダ計算です。 覚えたこと 全部、末尾に「〜らしいよ」ってつけて読んでくれるとうれしいです。 再帰のあるバリアントはInductiveで定義する 相互再帰のあ…

30分プログラム、その680。watchコマンドを作ってみました。watchコマンドって知っていますか? $ watch hogehogeとやると、一定時間ごとにhogehogeを実行して画面を更新してくれるコマンドです。 watch dateで時計変わりにしたり、watch lsでファイルが作ら…

すてきなWikiクローンはないものかと探していたら、http://wikihub.org/wiki/wikihub-wikiというのを見つけました。 Gitレポジトリに、テキストファイルをコミットするだけで、Wikiページを作れちゃいます。 素敵なポイント レポジトリにGitHubが使える Git…

30分プログラム、その679。Games::Puzzles::SendMoreMoneyを試してみた。 前に誰かが「CPANにはSEND+MORE=MONEYを解くためだけのモジュールがあるんだぜ。ちょううけるwww」と言っていたことを思いだしたので、試してみました。 サンプルコード my $solver =…

30分プログラム、その678。昔やった複利計算 - みずぴー日記をリメイクしてみました。再帰をやめて、scanlを使っているあたりに成長を感じていただければ幸いです。あ、でもうまくファイル入力ができなかったです。ダメダメですね。 使い方 1> compound:each…

30分プログラム、その677。来年まであと何日かを出力するプログラム。 恐しいことに、今年も終わりが見えてきました。 そのことについて考えるといろいろと後悔の念がでてきますが、とりあえず来年まで何日あるかを出力するプログラムを書いてみましょう。 …