概要 Agda2 で挿入ソート関数を定義して、それがほんとにリストをソートすることを証明してみました。試すには Agda の標準ライブラリ(The Agda Wiki - Standard Library)が必要です。 冗長な証明になっている可能性は大いにあります。Agda のサンプルコード…
2010-09-26 を見て同じ命題を Agda2 で証明してみた。 Functional Programming Memo: [Coq] Coq-99 : Part 1 agda-mode が証明するのを手伝ってくれるのでお気楽です。 module Practice1 where data True : Prop where tt : True data False : Prop where da…
iPad 買いました。おもしろいです。土日は iPad を持って外出してましたが、電池切れになることはありませんでした。あとは Evernote をプレミアムアカウントにしてローカルにファイルを保存できるようにすれば、今週は寮に MacBook を持ってく必要がないか…
f(n) = n*n + an + b, |a|素数が連続して最も長く出現するような a, b の値を求めよ。 こっちもがっちり C で。何も考えなくても Haskell より速い。素敵。 #include <stdio.h> #define MAX 1000 int isPrime(int x){ int i; for (i=2;i</stdio.h>
現在は工場実習中で毎日肉体労働をしてるので、休日くらいはプログラムを書きたくなります。というわけで超久しぶりに Project Euler をやってみたよ。 問題23。正の整数 n の約数の和が n をより大きいとき、 n を過剰数(abundant number)という。2つの過剰…
背景 修論で追い詰められた学生が、「twitter クライアントはたくさんあるけど、実際ブラウザで十分なんじゃね。他の拡張と組み合わせれば、かえって操作性が上がるかもしれない。」と思いつき、嫌だ力を駆使して集中力が切れるたびに少しずつ書いた拡張機能…
LablGTK(http://wwwfun.kurims.kyoto-u.ac.jp/soft/lsl/lablgtk.html) は、OCaml のための GUI ライブラリです。素敵です。 背景 研究のためにサンプルプログラムを書く必要があった マルチスレッドと GUI のライブラリが必要だった Haskell + wxHaskell で…
スクリーンショット "nikki" で日記が検索できています! 内容 最近 Chrome の拡張を書くのがマイブームです。 Google Chrome で Hit a Hint - zyxwvの日記 で自分としてはだいぶ便利になったのですが、ページのどこかにある日本語のリンクをクリックしたい…
経緯 最近 Chrome を使っています。現状の Mac 版(4.0.245.0)だとブックマークの管理すらできず、ちょっと厳しいものがあるのですが、 windows でも linux でも動いて、簡単に拡張も書けるのでおすすめです。 で、拡張で遊んでみました。リンクをキーボード…
研究室の一部の人が uppaal で解こうとしていた問題。 オオカミとヤギとキャベツを対岸に移動させたいけど、オオカミとヤギ、あるいはヤギとキャベツを残したまま人が対岸に行ってはダメ、というやつ。 最初は prolog でやってやろうとしたけど、くじけて Ha…
起動時 拡大! CSS でなんか作ってみた第二弾。画像を3次元空間に配置してぐるぐるさせることができます。例によって対応ブラウザは webkit 系だけです。-webkit-* を -moz-* にかえれば Firefox でもきっと動きます。デモ: http://www.agusa.i.is.nagoya-u.…
CSS と Coq の記事が並ぶというシュールな展開ですが、これも嫌だ力のなせるわざです。今日の証明では SearchPattern とか eapply がでてくるよ! 本日のお題は、 filter 関数を2回適用しても結果のリストの長さが変わらないという性質 FilterLength の証明…
Coq などの定理証明系に興味を持っている人は少なくないと思うのですが、やっぱり最初の一歩を踏み出すのは大変。web 上の Coq チュートリアルは、Coq 処理系の機能を説明しているだけで、数学の素養がない人(普通の情報系の学生)が実際に関数の性質を証明す…
一覧表示 スライドショー中 ちょっと前に最近の CSS のおもしろさを知ったので、プレゼンテーションを作れるライブラリ的なものを作ってみた。ページの切り替えや一覧表示のときにぬるっと動きます。id:amachang さんの作った s6 と比べると、(CSS さえ書け…
寝る前に OCaml でなんか書いてみるか、と思って書いてみた。 exception Unexpected_char let interpret str = (* バッファ *) let buf = Array.create 3000 0 in (* 対応する右括弧(])を探しに行く *) let rec rp idx n = match String.get str idx with | …
ボタンをいくつか縦に並べたメニューをライブラリに移したんだけど、うまく動かなかった。メニューにはそれぞれ違った背景画像を使うんだけど、その画像が表示されない。どうやら埋め込まれていないのが原因らしい。プロジェクトのプロパティで、swc に含め…
FlexBuilder で開発していた某Eラーニングのサイトをシリーズ化することになったので、共通部分をライブラリ化することにした。 FlexBuilder で新しく"ライブラリプロジェクト"ってのを作って、そのライブラリを使うプロジェクトのプロパティから FlexBuilde…
予想外に5分でできた。というか選択されたテキストを wikipedia で引くサンプル(http://stupidbob307.eshlook.com/jetpacks/wikipedia.html)があったので、その URL を変えただけなんですけどね。予想以上に便利だったので Opera でも使いたい。(自画自賛) j…
ポルトガル語やら中国語やらフランス語を使うことになったので、http://d.hatena.ne.jp/kagamihoge/20090425/1240648033 を見ながら Flex の ResourceBundle を使ってみることにする。 ロケールの追加 まず、ディレクトリを以下のような感じで構成し、 proje…
アルバイトをやっていて思ったことをつらつらと。 GUI アプリケーションのテストをする際に、どこが難しいのかというと、 GUI は、ユーザの指定したレイアウトを記憶することが多い。ウィンドウの表示位置とか、スクロールバーの値とか、2ペインのウィンドウ…
頑張ってブログを書こうキャンペーン中。理由は特にない。 http://ameblo.jp/programming/entry-10001721422.html のやつ。 then の中はもっと綺麗にかけるんじゃないかと思うんだけど。 deal :: Int -> [Int] -> [[Int]] deal num cards = let (h,t) = spli…
macports で入れた cabal がアップグレードできなかった。 $ sudo port upgrade hs-cabal > Configuring hs-cabal Error: Target org.macports.configure returned: shell command "cd /opt/local/var/macports/build/_opt_local_var_macports_sources_rsync…
今更ながら Flapjax を試す。というかほんとに試しただけ。 Flapjax は FRP(Functional Reactive Programming) というものを JavaScript で実現したもの。FRP は、時間に応じて変化していくような値を Behavior という特別な値で表す。Behavior の値が変更さ…
"git init --shared" は、そのリポジトリのアクセス権限を指定するオプション。例えば group とか。デフォルトではリポジトリは共有されないので、複数人で作業しようとするとはまる。 "git clone --shared" は、リポジトリを clone する際にハードリンクを…
XML データは URLLoader を使って適当に読み込もう。 <member> <person> <name>Alice</name> <age>20</age> </person> <person> <name>Bob</name> <age>22</age> </person> </member> 使いかたはこう。 var member : XML = new XML(loader.data); // member.member.person.name じゃないよ! trace(member.person.name.toString());
Python で、 UTC で表された時間から JST に変換する方法。twitter から取ってきたデータを扱うために調べた。 datetime モジュールを使う。timedelta で時間の差分を表す。ちなみに twitter の時間の表示は "Sun Jan 18 09:00:48 +0000 2009" みたいな感じ…
裏で LLVM を使ってるんだぜすごいだろ的なサンプル。Pure で副作用を使う方法がよくわからないので(できないような気もする)カウンター関数を C で作って使ってみよう。 まずは counterlib.c と counter.pure を用意します。 /* counterlib.c */ int counte…
Pure で書いてみよう第二弾。new と replication のない(!) CCS 式を実行できます。型なし Haskell みたいな書き方をしたのでとても簡単だった。やっぱり Pure を使う利点が見つからない…。
年も明けたことだし新しい言語で何か書いてみよう、ということで、書いてみた。言語は Pure (Google Code Archive - Long-term storage for Google Code Project Hosting.)。id:mzp が「HelloWorld の次に書くプログラムと言えばフィボナッチ数か階乗かエラ…
RSS 内のアイテムを1つづつローカルの HTML ファイルにするだけのスクリプト。これからもうちょっと便利になるように改良してみたいところ。あまりサンプルがないようなので貼付けておきます。git-hub とかは僕には難しすぎてよくわかりません。 例によって…