Agda で挿入ソートする

概要 Agda2 で挿入ソート関数を定義して、それがほんとにリストをソートすることを証明してみました。試すには Agda の標準ライブラリ(The Agda Wiki - Standard Library)が必要です。 冗長な証明になっている可能性は大いにあります。Agda のサンプルコード…

tmiyaさんの練習問題をラムダ式で解いてみた

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…

とりあえず JapanTimes と NYTimes をクーリエ・ジャポンみたいに見るブックマークレット(超適当)

iPad 買いました。おもしろいです。土日は iPad を持って外出してましたが、電池切れになることはありませんでした。あとは Evernote をプレミアムアカウントにしてローカルにファイルを保存できるようにすれば、今週は寮に MacBook を持ってく必要がないか…

Project Euler: Problem27

C

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: Problem23

C

現在は工場実習中で毎日肉体労働をしてるので、休日くらいはプログラムを書きたくなります。というわけで超久しぶりに Project Euler をやってみたよ。 問題23。正の整数 n の約数の和が n をより大きいとき、 n を過剰数(abundant number)という。2つの過剰…

twitter.com を改善する拡張を書いた

背景 修論で追い詰められた学生が、「twitter クライアントはたくさんあるけど、実際ブラウザで十分なんじゃね。他の拡張と組み合わせれば、かえって操作性が上がるかもしれない。」と思いつき、嫌だ力を駆使して集中力が切れるたびに少しずつ書いた拡張機能…

LablGTK で遊ぶ

LablGTK(http://wwwfun.kurims.kyoto-u.ac.jp/soft/lsl/lablgtk.html) は、OCaml のための GUI ライブラリです。素敵です。 背景 研究のためにサンプルプログラムを書く必要があった マルチスレッドと GUI のライブラリが必要だった Haskell + wxHaskell で…

Google Chrome で migemo 検索

スクリーンショット "nikki" で日記が検索できています! 内容 最近 Chrome の拡張を書くのがマイブームです。 Google Chrome で Hit a Hint - zyxwvの日記 で自分としてはだいぶ便利になったのですが、ページのどこかにある日本語のリンクをクリックしたい…

Google Chrome で Hit a Hint

経緯 最近 Chrome を使っています。現状の Mac 版(4.0.245.0)だとブックマークの管理すらできず、ちょっと厳しいものがあるのですが、 windows でも linux でも動いて、簡単に拡張も書けるのでおすすめです。 で、拡張で遊んでみました。リンクをキーボード…

オオカミとヤギとキャベツを移動させるやつ

研究室の一部の人が uppaal で解こうとしていた問題。 オオカミとヤギとキャベツを対岸に移動させたいけど、オオカミとヤギ、あるいはヤギとキャベツを残したまま人が対岸に行ってはダメ、というやつ。 最初は prolog でやってやろうとしたけど、くじけて Ha…

CSS で画像を空間に散らしてみた

CSS

起動時 拡大! CSS でなんか作ってみた第二弾。画像を3次元空間に配置してぐるぐるさせることができます。例によって対応ブラウザは webkit 系だけです。-webkit-* を -moz-* にかえれば Firefox でもきっと動きます。デモ: http://www.agusa.i.is.nagoya-u.…

プログラマのための Coq

Coq

CSS と Coq の記事が並ぶというシュールな展開ですが、これも嫌だ力のなせるわざです。今日の証明では SearchPattern とか eapply がでてくるよ! 本日のお題は、 filter 関数を2回適用しても結果のリストの長さが変わらないという性質 FilterLength の証明…

はじめての Coq

Coq

Coq などの定理証明系に興味を持っている人は少なくないと思うのですが、やっぱり最初の一歩を踏み出すのは大変。web 上の Coq チュートリアルは、Coq 処理系の機能を説明しているだけで、数学の素養がない人(普通の情報系の学生)が実際に関数の性質を証明す…

JavaScript と CSS でプレゼンするライブラリを作ってみた(二番煎じ)

一覧表示 スライドショー中 ちょっと前に最近の CSS のおもしろさを知ったので、プレゼンテーションを作れるライブラリ的なものを作ってみた。ページの切り替えや一覧表示のときにぬるっと動きます。id:amachang さんの作った s6 と比べると、(CSS さえ書け…

Brainfuck インタプリタ

寝る前に 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 にリソースが埋め込めない

ボタンをいくつか縦に並べたメニューをライブラリに移したんだけど、うまく動かなかった。メニューにはそれぞれ違った背景画像を使うんだけど、その画像が表示されない。どうやら埋め込まれていないのが原因らしい。プロジェクトのプロパティで、swc に含め…

ライブラリプロジェクト

FlexBuilder で開発していた某Eラーニングのサイトをシリーズ化することになったので、共通部分をライブラリ化することにした。 FlexBuilder で新しく"ライブラリプロジェクト"ってのを作って、そのライブラリを使うプロジェクトのプロパティから FlexBuilde…

選択されたテキストを alc で引く Firefox 拡張

予想外に5分でできた。というか選択されたテキストを wikipedia で引くサンプル(http://stupidbob307.eshlook.com/jetpacks/wikipedia.html)があったので、その URL を変えただけなんですけどね。予想以上に便利だったので Opera でも使いたい。(自画自賛) j…

Flex 3 アプリケーションの国際化

ポルトガル語やら中国語やらフランス語を使うことになったので、http://d.hatena.ne.jp/kagamihoge/20090425/1240648033 を見ながら Flex の ResourceBundle を使ってみることにする。 ロケールの追加 まず、ディレクトリを以下のような感じで構成し、 proje…

GUI アプリケーションのテスト

アルバイトをやっていて思ったことをつらつらと。 GUI アプリケーションのテストをする際に、どこが難しいのかというと、 GUI は、ユーザの指定したレイアウトを記憶することが多い。ウィンドウの表示位置とか、スクロールバーの値とか、2ペインのウィンドウ…

10分でコーディング

頑張ってブログを書こうキャンペーン中。理由は特にない。 http://ameblo.jp/programming/entry-10001721422.html のやつ。 then の中はもっと綺麗にかけるんじゃないかと思うんだけど。 deal :: Int -> [Int] -> [[Int]] deal num cards = let (h,t) = spli…

macports の hs-cabal

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 を試す。というかほんとに試しただけ。 Flapjax は FRP(Functional Reactive Programming) というものを JavaScript で実現したもの。FRP は、時間に応じて変化していくような値を Behavior という特別な値で表す。Behavior の値が変更さ…

git clone --shared と git init --shared

"git init --shared" は、そのリポジトリのアクセス権限を指定するオプション。例えば group とか。デフォルトではリポジトリは共有されないので、複数人で作業しようとするとはまる。 "git clone --shared" は、リポジトリを clone する際にハードリンクを…

ActionScript の XML のアクセス

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 で UTC2JST

Python で、 UTC で表された時間から JST に変換する方法。twitter から取ってきたデータを扱うために調べた。 datetime モジュールを使う。timedelta で時間の差分を表す。ちなみに twitter の時間の表示は "Sun Jan 18 09:00:48 +0000 2009" みたいな感じ…

Pure から C のライブラリを使ってみる

裏で LLVM を使ってるんだぜすごいだろ的なサンプル。Pure で副作用を使う方法がよくわからないので(できないような気もする)カウンター関数を C で作って使ってみよう。 まずは counterlib.c と counter.pure を用意します。 /* counterlib.c */ int counte…

Pure で CCS みたいなやつ

Pure で書いてみよう第二弾。new と replication のない(!) CCS 式を実行できます。型なし Haskell みたいな書き方をしたのでとても簡単だった。やっぱり Pure を使う利点が見つからない…。

Pure で数独

年も明けたことだし新しい言語で何か書いてみよう、ということで、書いてみた。言語は Pure (Google Code Archive - Long-term storage for Google Code Project Hosting.)。id:mzp が「HelloWorld の次に書くプログラムと言えばフィボナッチ数か階乗かエラ…

fuse-python で遊んだ

RSS 内のアイテムを1つづつローカルの HTML ファイルにするだけのスクリプト。これからもうちょっと便利になるように改良してみたいところ。あまりサンプルがないようなので貼付けておきます。git-hub とかは僕には難しすぎてよくわかりません。 例によって…