Coqを使っていたら、coqcを落すコードに出会ってしまいました。 コード Require Import Sets.Ensembles. Variable (P: Prop). Variable (A: Type). Hypothesis the_hypo : forall x, exists xs, In A xs x -> P. Theorem some_theorem : P -> P. Proof. intr…

30分プログラム、その703。cursesのmvaddstrみたいにターミナルの任意の位置にテキストを出す関数を作ってみた。 エスケープシケンスを使えば、好きな位置に文字を出すぐらいなら簡単にできるということを知りました。今まで、cursesが必須だと思ってたのに!…

30分プログラム、その702。Bitmapを読んでみよう。 Erlangにはバイナリ構文なる便利なやつがあるので、それを使ってビットマップの読み込みをできるようにしてみよう。Erlangで画像処理、とかもおもしろそうだし。とりあえず、今回は読み込みのみ。そのうち…

30分プログラム、その701。プログラミングHaskellを読んでたら、Haskellにはn+kパターンってのがあるらしい。 これを使うと even (n+1) = odd n みたいにパターンの部分にn+kの形が使えるらしいです。曰く、不人気で将来のバージョンでは消えるかもしれない…

30分プログラム、その700。Scalaでhexdumpを作ってみました。hexdumpは、与えられたファイルを16進数で表示するプログラムです。 $ hexdump a.txt 0000000 61 0a 62 0a 0a 0a 0a 0000007いわゆるバイナリエディタでみれるやつです。何かと便利ですよ、これ。…

前からずっと取り組んでいた「Coqで単純型付きラムダ計算を証明してみよう」が一段落しました。 動機 let多相の実装はしたから、次は証明だろ 最近、流行っているCoqを覚えたい 扱えるラムダ式 型は、Bool型と関数型のみ。 Inductive type : Set := | BoolT …

30分プログラム、その699。いつ、どこで、誰が、何をしたジェネレータ。 ランダムに文章を生成するよ! Printfがとっても欲しいよ! 使い方 昨日、海でキミが寝たval it = () : unit - println (make ()); 昨日、地の中で知らない人が食事をした val it = () :…

30分プログラム、その698。データ構造を作ってみたシリーズ、ハッシュテーブルを作ってみた。 「ハッシュテーブルをハッシュと略すのは、ウィキペディアをウィキと略すのと同じだ」で同じみのハッシュテーブルです。「組込みのhashなんていらないぜ。自分で…

30分プログラム、その697。プログラムが140文字以内かをチェックするプログラム。 最近、140文字以内でプログラムを書くのがはやっているらしいです。とりあえず、140文字以内かどうかをチェックするプログラムを書いてみましょう。 使い方 $ perl byte-chec…

30分プログラム、その697。http://gauc.no-ip.org/awk-users-jp/blis.cgi/DoukakuAWK_239からの逆輸入です。 一番、長いコマンド名を探してみましょう。 使い方 $ python longest-command.py powerpc-apple-darwin9.7.0-gfortran-mp-4.3あー、アーキテクチャ…

下の記事で print max(append_map(os.listdir, os.environ['PATH'].split(':')), key=len) というコードを書いてるけど、これ結構読みにくくない? splitの部分はオブジェクトのメソッドなので処理が左から右に流れるけど、それ以外は関数なので処理が右から…

30分プログラム、その696。ビンゴゲーム・ジェネレータ。とはいっても、実際にシートを作るわけではく、ターミナルにテキストを吐き出すだけです。 9 34 72 74 10 93 16 36 95 61 3 12 * 32 34 64 77 64 57 2 51 24 42 92 0要するに 5x5のマス目に数字を並べ…

追記: 本家にマージされました。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バリデータを作ってみました…