未来言語Agda - 数学猫の生活と意見
最近Agdaを触る機会があったのだが、Agdaこそ未来のプログラミング言語ではないかという気がしてきた。ここでは行列の転置をする関数を定義することで、Agdaでのプログラミングがどんなものか紹介したい。その前に一言:Agdaは定理証明系として紹介されることが多い。これはAgdaにとって不幸なことだ。確かにAgdaの型システムは強力なので、例のカリーハワード同型により、型を命題、プログラムを証明とみなすことができる。ただし、私の印象ではAgda上は数学の証明をしやすいようにはそんなにはできていない。Agdaで証明するには、ある型をもつ定数なり関数を定義することになるわけだが、定義した関数がその型を持っているかことを型チェッカに説得するために、型チェッカの詳しい挙動について理解していなければならない。むしろ、Agdaは依存型をもつプログラミング言語と思った方がよいと思う。依存型とはなにかは例を
Lispが何故使われないか - 数学猫の生活と意見
原因のほとんどは経路依存性*1とかネットワーク効果*2によるもので、Lisp自体の性質とは無関係だと思います。と言った上で、私が何となくLisp系言語を使わない理由としては、Too dynamic: 実行時にコードが差し替えられることがすごい利点だ、と言っている人がいましたが、逆に言えば今どのコードが走っているか理解しにくい、という欠点にも繋がる。Meta programming:S式のおかげでMeta Programmingがしやすいが、Meta Programmingを多用したプログラムは理解しにくい。動的型付け:利点でもあるけど、特有のバグを引き起こす。識別子に関数と値の2種類が別々にバインドできる。これは私には非常に美しくなく感じます。主観ですが。一方でSchemeは言語仕様が弱い。(特にModule機能が標準でない)Proprietaryな実装が中心。CMU LispはStand
HatenaTailを公開します - 数学猫の生活と意見
■[HatenaTail]HatenaTailを公開します DNSの設定を間違えていたのでアクセスできませんでした。私のプロバイダからは見えるようになったので、公開します。URLのポート番号は今のところ必要みたいです。ポート番号なしでのアクセスをお願いします。 HatenaTailははてなブックマークにブックマークされたウェブページの間に関連を発見するツールです。意外なページに関係があることを発見して楽しんでいただければ幸いです。はてなユーザーの方でブックマークを公開されている方は、はてなidを使ってログインすることでおすすめページなどの機能も使うことができます。 関連の発見にはBayesian Setsを使っています。サイトの構築にはRuby on Railsを用いました。最新の情報は管理者の はてなダイアリー に掲載しています。また、ソースをdarcsリポジトリとして配布する予定です
パッチの圏 - 数学猫の生活と意見
■[数学][darcs]パッチの圏 ファイルとパッチは圏をなすことが簡単に分かる。 オブジェクトはファイル 射はパッチ 恒等射は何もしないパッチ 射の結合律は...まあよいことにしよう(パッチの同一性をどう定義するかという問題があるが)。 空ファイルがinitail/terminal objectになりそうだ。initialとterminalが同じになるのはちょっと嫌だな。pullbackはあるだろうか。この辺になると具体的な定義がないと考えづらいので、こんな風に定義してみる。 ファイルfは行の集合 パッチ p : f1→f2 はf1の部分集合からf2の部分集合へ定義された1:1-写像 こう考えるとpullbackもありそうだ。 いや、トポスにならないか*1と思ったわけだけど、トポスでinitailとterminalが等しいと何かまずかったような記憶があるから、ダメかもしれない。 いやい
Hatena Relate - 数学猫の生活と意見
Bayseian Setが面白そうだったので、これを使ってはてなブックマークの最新人気エントリをグループ分けするプログラムを書いてみました。ブックマークしたユーザーを属性と見て分類します。起動するとはてなブックマークから最新エントリを取得して、HTMLを標準出力に書き出します。Rubyプログラムです。 class AttrVector attr_reader :name def initialize(name) @name = name @attrs = Hash.new(false) end def add(attr) @attrs[attr]=true end def remove(attr) @attrs.delete(attr) end def each @attrs.each_key{|key| yield(key)} end end # require 'test/unit'
BrainScan - BrainF*ckプログラムを超高信頼化する - 数学猫の生活と意見
BrainScanというものを作ってみました。BrainFuck*1のソースコードモデル検査器です。プログラムがとり得る全状態を探索し、異常が起きないか検査します。検査できるのは、ポインタがアンダーフローしないことバッファの値が0-255を越えないかどうか(-Rまたは--rangeオプションを付けたときのみ)コード中で!でマークされた位置に到達しないかどうか(したらエラーとみなす)です。エラーを検出すると、そこまでのトレースを出力します。アルゴリズムは単純で、深さ優先探索をするだけです。バッファの状態は区間の集合として保持されています。OCamlで書かれて、コンパイルするにはfindlibとextlibが必要です。例を見てみましょう。 $ ./brainscan '[]!' ! reached. 0: [ 2: ! BrainF*ckプログラムはコマンドライン引数として与えます。この例だと
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
スルーされぢから at work - 数学猫の生活と意見
最適化しようとしたら、かえって遅くなりました - 数学猫の生活と意見
ESPer2006 秋の陣でデモを行います - 数学猫の生活と意見
真字 0.2.0 - 数学猫の生活と意見
http://d.hatena.ne.jp/yoriyuki/comment?date=20060404