2009-10-01から1ヶ月間の記事一覧

一番長いファイル名を探すプログラム

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

ディレクトリ・トラバース用ユーティリティ

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

今日のCoq: InductiveなProp

Coq

定理の中で使う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…

今日のCoq: Inversion of the typing relation補題とUniqueness of types定理

Coq

今日も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 (* …

今日のCoq: Inversion of the typing relation補題

Coq

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

ScalaでSEND+MORE=MONEY

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

今日のCoq: 型づけ規則とそれに関する補題

Coq

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

今日のCoq: eval

Coq

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

ITプランニングってすごいですね

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

let*と名前付きletをマクロで

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

今日のCoq: ラムダ式とsubstitute

Coq

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

watchコマンドを作ってみた

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

WikiHubがすごい!

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

Games::Puzzles::SendMoreMoneyを試してみた

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

複利計算、再び

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

来年まであと何日?

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

git blog: gitレポジトリからブログ記事のテンプレートを生成するコマンドを作りました

何ができるの? gitのコミットログから、こんな感じのブログ記事を生成します。 生成される記事の内容は「今日の作業の要約」と「今日のコミット一覧(githubへのリンク付き)」です。 ダウンロード/インストール git blog: generate blog template from git re…

リストのシャッフル

30分プログラム、その676。リストのシャッフルをやってみました。 簡単に書けると思いきや、意外と落とし穴にはまりました。 乱数が生成できない! FAQによると、Randomというアンドキュメントなstructureがあるらしい。 List.sortがない。 自分で書いた。 fs…

簡易HTTPサーバ

30分プログラム、その675。簡易HTTPサーバ。 Helloとしか返さない簡単なWebサーバです。Javadocとにらめっこしてたら30分なんてあっという間です。 使い方 $ fsc server.scala $ scala Main ソースコード import java.net.ServerSocket import java.io.Print…

リストの上で集合っぽい演算

30分プログラム、その674。リストの上で集合っぽい演算を定義してみました。 みなさん、知ってます? Rubyって配列を集合みたいに扱えるんです。 >> [1,2,3] - [3,4,5] => [1, 2] [1,2,3] & [3,4,5] => [3] >> [1,2,3] | [3,4,5] => [1, 2, 3, 4, 5] ホントの…

Twitterの流量を計算してみよう

30分プログラム、その673。Twitterの流量を計算してみました。 Twitterには"流量"という概念があるらしいです。よく分かんないんですが、「自分のTLで、1時間あたり何回発言が行なわれたか」というニュアンスみたいです。 わりとおもしろそうなネタなので、…

コマンドラインでストップウォッチ

30分プログラム、その672。コマンドラインで動作するストップウォッチを作ってみた。 perl stopwatch.plで起動すると、経過時間を延々と表示してくれます。 操作方法は、Enterを押せばラップタイム、C-cで終了、C-zで一時停止、ということにしといてください…

並列ダウンローダっぽい何か

30分プログラム、その672。サーバごとにスレッドを立ち上げて、並列でダウンロードするダウンローダを目指してみた。実際は、スレッドを立ち上げるとこまでしかやっていない。 Webからファイルをダウンロードするときは、なるべく並列化して効率をあげたい。…

Scalaでls

30分プログラム、その671。Scalaでファイル一覧の取得をやってみました。 最初は、ScalaのAPIドキュメントを読んでいたんだけれども、どこにもファイル一覧を取得する関数が載ってない。 どうすんだよー、としばらく悩んでいたけど、JavaのAPIを使えばいいこ…

Writerモナドを試してみた

30分プログラム、その670。Writerモナドを試してみました。 前回がReaderモナドだったので、今回はWriterモナドを試してみました。 The Writer monadには、Writerモナドは裏でログをとったりするのに便利だと書いてあったので、関数の呼び出しを記録してみま…