デザインを変えた。 白い。 まあ白い方がいいかなあ、なんて。

ML/LL Advent Calendarのネタとしてはいくつか思いついたものがあって、 Linear Logic Linear Lisp（別のAdvent Calendarで出たようなので避けて賢明か） Module Type（Coqの） Moonlit Lo...げふんげふん なんだったか忘れたね。

この記事はLL/ML Advent Calendarの6日目の記事である。 今年はなかなかに なごやこわい なアドベントカレンダーが出てきたなあ、とかつぶやいたら気づいたら犠牲参加者になっていた。 やっぱり なごやこわい 。 LL名古屋に似たようなのがあるようだが？ あ…

これが最後の学期になりそうだ。

最後の学生生活。 ・・・最後だといいなあ。 うん、最後にしよう。

以前使ってみようとしたときにlibgmpがないことがわかっていたので、先にmingw32-libgmpを入れてみた。 だが、思わぬところ（configure）で時間かかってしまった。 bash上で./configureをすると、-lgmpがどうのこうのといってくる。 またお前か！ で、いろい…

いや、楽しいばかりじゃなくて面倒なことも多いけど。 Lavie Zを買った。 軽いなあ。 しかし、やはり今までのPCではいろいろ設定していたから何から始めていいのかわからないというのがある。 ログオン画面でユーザー選択を自動化したいとか。 ただし、パス…

ときどきTwitterで出てくる「言葉狩り」という現象についてちょっと気になったので書いている。 言葉狩りといっても、ある特定の語を禁止し、別の言葉に言い換えてしまうことがほとんどなのだが*1。 いわゆる差別用語とか、特定の侮蔑とか、言いにくいが児ポ…

ツイッターで、こんなツイートが流れてきた。 こんなの。 もちろん実体はWikipediaとか外部の情報へのリンク貼ってるだけ。 やれやれ。 が、気付いたらもう25を超えてしまった私は、少し考えて、「書いてみるか・・・？」などと思ってしまった。 これが俗に…

実は自分のデスクトップでは比較的容易にF-12Cを認識したが、ノートでは全然認識しなかった。 原因不明、意味不明だったのだが、今日ふと検索したところすばらしい記事が出て来た。 それがこれ。 本来なら、USBを刺したらFujitsu HSUSB Deviceが検出されるは…

なんだ、F-12CはUSBテザリングは無効化されてなかったのか。*1 というわけで、「PCに刺したままならテザリング可能」ということが今日わかった。 今の回線がまさにそれ。 まだ有効化の完全な内容にはなっていないけれど、とりあえずrootなしでもAuto USB Tet…

一応生存を主張。 この間、論文を書いて、終わってへばって、次の論文に向けていろいろ考え中。 アイディアは大体固まったので、もう少し詰めてからやってみるかな、という感じ。 Coqのサブセットもその一つ。 まあ、Notationないけどね！ Typeもないけどね…

Round 1Aについて。 今度はA,B,Cの三問。 前回と同じく、最後だけ解けなかった。 解けた問題だけとりあえず解説。 A パスワード入力画面で、すでに何文字か打ったが、ある時点で間違ってしまったかもしれない。 これから何文字か削除して再開するか、それと…

GCJ = Google Code Jam。Googleがやってるプログラミングコンテスト。 アカウントはちょこちょこいろんなプログラミングコンテストに登録しているのだが、まともにやったのは今回が始めて。 Qualification roundとRound 1aが終わって、とりあえずRound 2には…

LinuxやMacを使っている人は、C言語のプログラムを書くとき、時々manで関数の内容を調べたりするだろう（引数の順序とか細かい仕様とか）。 私はWindowsユーザーだが、これはほしい。 Cygwinなら入るけどそもそも極力Cygwin入れたくない。 というわけで調べ…

いや、最終的にはつかえたけれども。 つい先日1.0が出たSML#なるものを私も使ってみようと思ったわけである。 なんとご丁寧なことに、Windows用にはMinGWを使った実装がバイナリで公開されている。 いやはやありがたいことですよ。 で、動かしてみたら・・・…

パターンマッチができるってことは、extractionできるということである。 singleton definitionのパターンマッチの場合、実は非常に簡単で、そのパターンマッチ自体が消えて、結果だけが残る。 一方、empty definitionはそうも行かない。そもそもCoqのterm上…

これが誰かの何かの役に立てば幸いなのだけれども。 さて、述語に対するパターンマッチは述語以外を返してはいけない、といった。 しかし例外がある。 それは、展開する述語がsingletonまたはempty definitionとして定義されている場合。 この場合はSetやTyp…

ちょっと説明してないのもどうかと思ったので。 述語のdestructの話は、計算レベルで制限されている話で、問題になりやすいのはinversionやinductionだと思う（inductionはかなり稀か）。 「ゴールがSetやTypeに属する型であるときに、述語をinversionしたら…

これ見る人いるのかな・・・ 昨日の話と全然連続しないが、昨日のシリーズの続き。 Propに属する帰納型（以下、述語と記述）の展開の話。 Coqのマニュアルだとここの4.5.4のAllowed elimination sortsのあたり。 実際のところ、使用者からして気になる部分は…

ちょっと基本的なところから行こう。 pCICと書いているが、まあ多くの人はそんなもの知るまい。 ちなみに、Coqについてそれなりの知識を持っていることを前提に話をするので、せめて利用者としての経験を要求する。 pCICはpredicative Calculus of Inductive…

先週の発表で、「Coqをいじりたい人向けに情報をまとめておいたら役に立ちそう」という言葉をもらった。 そんなのどんだけいるんだろう・・・と思わなくもないが、実際端から端まで読んだわけでもないし（読まなくてもブラックボックスのまま使える部分も多…

少しメモ書き程度に。 研究の展望があるのに、それを実装するコストがとんでもないことに気付いた。 並列計算について少し調べたいな。並行もだけど、並列はどうなんだろう？ そういえばC言語超入門とかいうよくわからないものもあったっけ。 Coqのテキスト…

さて。rootを取り、suを仕込むのに数十分、テザリング関係は調べて数時間。 一晩中かけて調べたけれど、まったく結果が出てこない、という結果に。 とりあえずやり方は/data/data/com.android.providers.settings/databases/settings.dbを編集する方法。*1 …

いろいろ調べたが、データベースの書き換えでうまくいく機種もあるらしい、という情報を得たものの、そもそも設定がかなり違うようだ。 おそらく内部のアプリかバイナリをいじらないとうまくいきそうもない。 なお、別途アプリを導入すればテザリングはでき…

とうとうできた人が出てきた様子。 具体的にはここ。 私も試したので、以下気になることや注意書き。 ちなみにその人のやり方はこっちのやり方をそのまま適用したというもの。 さて、事前準備。 Androidの開発キットの準備。まあroot化するんだから当たり前…