[Coq] How to Find Unreachable Nodes
Personal memorandum for studying functional languages, theorem proving, and formal verification. But other topics might be included. Written in Japanese (Shift-JIS Encoding). 不正な状態遷移を見つけるアルゴリズム @ kencobaの日記経由。 答えを出すだけならこんなのでもOK? 元の問題の規模が判らないが、この程度に小さな問題なら auto で探索出来る。 Axiom O A B C D E F G H I:Prop. Axiom OA : O -> A. Axiom AB : A -> B. Axiom BC : B -> C. Axiom CB : C -> B. Axiom CA : C -> A. Axio
Coq で遊ぶその4: Coq の変なところ色々。簡約。宣言と定義。型。 - 言語ゲーム
Coq in a Hurry ではこの後 Inductive Types の話になりますが、難しすぎてついてゆけないのでInteractive Theorem Proving and Program Development (Coq'Art) isbn:3540208542でゆきます。この本は重くて固くて取っ付きにくいですが、基本的な事から順番に書いてあるので、他のチュートリアルより内容は簡単です。今日は証明から離れて プログラミング言語としての Coq の側面を見てゆきます。 評価(簡約)の変なところ Coq はプログラム実行環境ではなく、プログラム開発を支援する為の設計環境としてデザインされています。だから変な所が沢山あります。たとえばたかが 3 + 4 を計算するのに、 Coq < Check 3 + 4. 3 + 4 : nat としても駄目で、 Coq < Eval cbv de
無限ストリームで幅優先探索 - keigoiの日記
参考：http://d.hatena.ne.jp/yoshihiro503/20100119#p1 証明すげー。 あと、幅優先探索で見つけたパスを無限ストリームで並べているのを見てこれは面白いと思った。枝刈り付きBFSとゴールの発見手続きを独立に書けているのか。なるほど！ ストリームを使ったプログラミングはHaskellでもよくあるし、モジュール性を向上させるというのもどこかで読んだけど、実際に目の当たりにするととても面白い。そしてストリームで書いたことによるプログラムの独立性が証明の簡潔さにつながっている(たぶん)のはとても興味深い。いや私はアルゴリズム苦手だし、関数型プログラムでパズルを解く人たちにはストリームなんて当然のことなのかもしれない。でもとにかく、感銘を受けたのでちょっとアルゴリズムを勉強しなおそうと思った。プログラムのエレガントさは、きっと証明のしやすさに影響するのだ。 一
迷路の試験問題を解いてみた - にわとり小屋でのプログラミング
参考：人材獲得作戦・４ 試験問題ほか: 人生を書き換える者すらいた。 Lv4に評価されるためには、最短性の完全なチェックが必要だったのでCoqで証明してみた。 まず、accessiblesという関数を定義し、以下の性質を証明した。 ここでplengthはパスの長さを計る関数で、Path x pはpがxを起点としたパスであるという述語。endofはパスの終点を求める関数。 Fixpoint accessibles (start : node) (len : nat) : list path := match len with | O => (PUnit start) :: nil | S n' => div_equiv path_equiv_dec @@ (flat_map expand @@ accessibles start n') end. この関数はstartから始まってlenの長さ
検索エンジンの常識をApache Solrで身につける
表のような転置インデックス完成後は、クエリに対する結果を返す処理は簡単です。例えば、ユーザーが「Vim」というクエリを発行すると、検索エンジンは「Vim」を含む文書IDリストを返します。表では文書IDの「2」を返します。 検索エンジンを取り巻く7つの技術 検索エンジンのコア技術は前節で紹介したインデックスです。しかし実際に、検索インデックスだけで構成する検索エンジンから、検索サービスを構築するには多大なコストが掛かります。以下の節で検索エンジンを利用したシステム、検索サービスを構築する際に便利なコンポーネントを紹介します。 これらの機能のいくつかは、多くの検索エンジンが組み込んでいます。一方で、簡素な検索エンジンは、以下で紹介するコンポーネントをサポートしていないため、ユーザーが独自に開発するか、その機能を持つコンポーネントを組み込む必要があるものもあります。 【1】トークナイザ 検索エン
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
nineties - Overview