2013-02-07から1日間の記事一覧

無限リストと証明じゃないCoqの話

Haskellではじめて無限リストのコードを見たときはとても驚いた。遅延評価など知らないから、どうみても無限ループに陥りそうなプログラムがちゃんと動いているのが不思議だった。無限に続くデータさえ表現できる遅延データ構造はとても強力だ。大量のデータ…