これはTheorem Proving Advent Calendarの15日目の記事である。 二回目じゃないのかって？人数不足だ。気にしてはいけない。 さて、今日の記事が何に関する記事かは見れば一目瞭然。 Coqの中のtactics記述用言語Ltacについてであり、目標はあの有名なcrushを…

今b-mobileのSIMで使っていて、パケットを使いたくなかったのでDoCoMoショップに行ってみた。 聞いてみたところ、アップデートさせてくれるということで、SIMを持ってきてくれて、相手の目の前でアップデート。 無事できた。よかった。 と思ってたよ今日まで…

面倒な話である。 ソフト名はメモとるの忘れたため、詳細が全然わからない。 わかっている範囲： ans.exe*1という実行ファイルで、ユーザーのホーム\AppData\Localに実行ファイルを置いた。 32bitアプリケーションだった。 ブラウザが落とされた（侵入経路は…

先ほどの記事、12-03という日付になっているが、一応日付が変わってから公開している。 これははてなダイアリーの仕様*1なので、私に言われても困る。 *1:もちろん設定で変更可能、今はデフォルトの午前6時日付変更になっている。

これは、Theorem Proving Advent Calendarの四日目の記事である。 ぱっと見ではあまりTheorem Provingらしくないかと思われるかもしれないが、たまにはこういう話もよいだろう、ということで。 お題 今回使う道具は、Curry-Howard同型対応、直観主義で失われ…

Theorem Provingのアドベントカレンダーに参加しようと思ったのだが、現時点で参加者5人。 このままだとどうなるのだろうか・・・？ できれば参加者求む。

おめでとうございます。 ソフトバンクと書かない辺りがミソ。

今日、メールが誤判定により迷惑メールフォルダに放り込まれた。 早速動かそうとして・・・ 動かせない。 メニューにそんなコマンドがない。 ちょっと待とうよ、メールを振り分けたりしたいでしょう？ 間違ったら動かすでしょう？ 削除しか出来ないって何？ …

コード読みにOCaml global tagsというツールを使っていた。 global tagsというツールのOCaml用ラッパーだ。 しかし、これがまたいろんなエラーを出すもので、3.11以降の新しい言語機構への対応などと言うすばらしいことは一切ないわけである。 疲れそうな話…

Androidアプリの開発をしたくなったり、ちょっと変なことをしたくなると、ひとまず手元のPCにつなぐ必要が出る。 が、F-12Cの接続は面倒な面倒な・・・ そんな道のりがまっている。 手順は大体こんなところ。 android-SDKをインストールする。 F-12Cのドライ…

パワポを共有・・・というよりアップロードするサービスがあったので、アップロードしてみた。 内容は去年の夏ゼミで話したCartesian Closed Categoryの話。 もちろん（と言っていいか疑問だが）日本語。 Cartesian Closed Category View more presentations…

OCamlDebugでSetやMapで作ったモジュールが何も見えないじゃないか、というのをいろいろ調べると、「Pretty Printer作れば解決」ということがわかった。 ただし、それらを上書きしてやらないといけないが。 ちなみに実現するprint.mlは中野さんのブログで紹…

なんか今朝アクセスポイントの設定がおかしくなっていた。 テザリングをした影響か？ ちなみに普通にアクセスポイントの設定を直したら直った。

b-mobileでのテザリングができないという話を聞いたのだが、今日試したところできた。 ちなみにSIMロック解除済み。それが影響しているかは不明。 今これを書くために使っている回線がテザリング。

終わった。 まだいろいろ続くが、とりあえず一段落。 ・・・でも、昨日まで書いてたやつはまだ修正しないとな。

直近のタスクがあと一つ。 それが終われば少しは休み気分・・・ なんて暇はあったっけ・・・？

なりましたので、思いついたことがあってもここに書けません。 そのうちそのうち。

昨晩寝ようと思ったときに、ふとどこぞのブログで無限がどうこう、という話があったな、と思い出した。 少し考えてしまったおかげで寝るのが遅くなったのだが・・・ というわけで、少し考えてみる。 有限の大きさ 1個のお菓子が入った袋と2個のお菓子が入っ…

結論：あまりデータが見えないから。 理由を述べると長いので、端的に。 関数内にいるときに、引数が多相だとその引数は出力できない。 インターフェースファイル内にモジュールの型はほとんど書けない。あくまで型チェックを通せる程度であり、デバッガが実…

オワタ！しないですんだ。 よかったよかった。 でもキューにはまだまだたくさん詰まってるのでしたとさ・・・

締め切りが少し延びたー。 それだけ。

Coqのソースコードをocamldebugで追えるようにして早何日か。 結局ocamldebugを使うのは（少なくとも現時点では）諦めることにした。 理由は次の通り。 Coqが使っている構文解析器がそもそもocamlcでコンパイルするものじゃなかった*1。 多相がものすごく邪…

研究の関係上、とあるOCamlのプロジェクト――いえ、まあ、とあるもなにも、Coqだが――をいじる必要が出た。 そんなにプログラミング・・・というかプロジェクトの読み解きなどをやったことがない私は、途方にくれ・・・まではしなかった。 運がいいことに、先…

とりあえず4月1日になったようだ。 学生たちの卒業、新社会人の誕生、といいことの中で。 エイプリルフールか。 としか思わなくなっている自分が。 まあそんなものだろう。 うまくしかけられる人間になりたいものだが・・・

今日帰るはずの出張で札幌にいました。 バスの中で停車中に横にゆれたもので、「そんな馬鹿な」というレベルの印象。 そして飛行機は飛ばない。 飛ぶかと思っていたが、そんな甘いわけもなく。 ひとまず家の状況が気にはなるが、一泊延長し、明日帰る予定で…

実は、前回書いたtype class in coqの記事、ちょっと怖いことがある。 このコードを実行すると、メモリを消費したあげくに落ちる。 Check (Compile (CEConst 1)).もちろんEval computeやEval simplでも同様。 なぜかはよくわからないが、まともにCompileの計…

これから、本当にほとんどの人には興味が向かないような、その上わけがわからない記事を書く。 なので、CoqやHaskellが好きな方以外はあまり見ないことをお勧めしておきたい。 ・・・などと、こんな記事を書いて自分も何をしたいのやら。

なぜ一度で出来なかったか？ 計画性がないからさ。 さて、ではType classで先ほどの流れをもう一度作ろう。 しかし、先ほどの定義とは、様々な点で異なるので注意。 Class Exp := { Eval : nat }. Instance EConst (n : nat) : Exp := { Eval := n }. Instan…

Coq8.2からType classが導入された。 もともとType classはHaskellにあったものである。 よって、Expression problemもHaskellからやり始めるのが楽である。 だが、私は残念ながらHaskellの世界の住人ではないので、Haskellによる解決に関しては私がこれをや…