2012-02-12

春休みの予定

1.セキュリティスペシャリストの勉強
　次の試験での合格を目指す
いまは、教科書半分位読み終わったところ
2.Schemeの勉強
　http://www.geocities.jp/m_hiroi/func/scheme.html#abcscm
↑サイトを参考にさせてもらいながら、勉強中
　春休み中にSchemeでmicro Schemeを作る、くらいまでいけるといいな　ぁ
3.TOEIC対策

2011-11-25

グラフの一筆書き判定

Python

ある連結グラフが一筆書き可能な場合の必要十分条件は、以下の条件のいずれか一方が成り立つことである（オイラー路参照）。
・すべての頂点の次数（頂点につながっている辺の数）が偶数 → 運筆が起点に戻る場合（閉路）
・次数が奇数である頂点の数が2で、残りの頂点の次数は全て偶数　→ 運筆が起点に戻らない場合（閉路でない路）
http://ja.wikipedia.org/wiki/%E4%B8%80%E7%AD%86%E6%9B%B8%E3%81%8D

ちなみに、「全ての辺を通る」が「全ての頂点を通る」になると、ハミルトン路というらしい。

とにかく、グラフが一筆書き可能かどうかは、次数が奇数であるような頂点（奇点）の個数を数えれば良いということになる。
そこで、グラフの隣接行列表現が与えられたときに、その奇点の個数を数えるプログラムをPythonで書いてみた。
最初に書いたのが次のプログラム。

def check(G):
    ctr = 0
    for i in range(len(G)):
        if sum(ls[i]) % 2:
            ctr +=1
    return ctr

Pythonのmap関数を使えばもっと簡潔にできないかなー、と思って考えているうちに、結局一行になった。

sum(map(lambda x: sum(x)%2, G))

map超便利。

2011-11-24

big-O記法の定義

$f$ と $g$ を２つの関数f,g: $\mathcal{N}\mapst\mathcal{R}^+$ とする。
全ての整数 $n\ge n_0$ に対して、正の整数cと $n_0$ が存在して、
$f(n)\le cg(n)$
であるならば、 $f(n)=O(g(n))$ という。

2011-11-24

Prologで自動定理証明?

論理学の定理は、形式論的には、公理と推論規則から導かれるものだ。
たとえば、ヒルベルト流では、

A ⊃ (B ⊃ A)
(A ⊃ (B ⊃ C)) ⊃ ((A ⊃ B) ⊃ (A ⊃ C))
(¬A ⊃ ¬B) ⊃ (B ⊃ A)

という三つの公理と、次のMP(modus ponens)という一つの推論規則を用いる。
A と (A ⊃ B) が定理ならば、Bも定理である。

で、公理を事実、推論規則をルールとしてPrologに実装してやれば、自動的に定理を証明してくれるかな?と思ったのだが...

実装例

theorem( imp( P, imp(Q,P) ) ).
theorem(imp(imp( P, imp(Q,R) ),  imp( imp(P,Q), imp(P,R)))).
theorem(imp(imp(neg(P),neg(Q)),imp(Q,P))).
theorem(B):- theorem(A), theorem(imp(A,B)).

上記のような実装でたとえば
theorem(imp(a,a)) #A ⊃ A
のようなものは証明できた。
しかし、証明できない式もたくさんある。

ヒルベルト流でなにか定理を証明しようとするとき、機械的に行うのは難しい(もしかして無理?)のようだ。
なぜなら、A ⊃ (B ⊃ A)のような形をした論理式は無数に存在する。
定理の証明のために、うまく公理をつかうには、ひらめきが必要になってしまう。
自動定理証明のためには、導出原理などの工夫が必要なようだ。