言語ゲーム

とあるエンジニアが嘘ばかり書く日記

Twitter: @propella
トップ > coq > Coq で遊ぶその8: 真実とは何か?

Coq で遊ぶその8: 真実とは何か?

coq

真の定義

真実とは何でしょうか?

それは人類始まって以来の謎に満ちた疑問に思えますが、プログラムの世界では割と簡単です。真と偽を表す値と演算子を使って真偽表で判定します。例えば真理表はこんなのです。

  • 真 ならば 真 => 真
  • 真 ならば 偽 => 偽
  • 偽 ならば 真 => 真
  • 偽 ならば 偽 => 真

その背後にある考え方は、物事は真か偽のどちらかで、複雑な問題も一つ一つの要素の真偽が分かれば全体の真偽も機械的に求まるという物です。これを Tarski のやり方と言うそうです(Coq'Art P43)。しかしこれには一つ問題があります。前提となる、「物事は真か偽のどちらかである」です。命題の中には数学的にちゃんと書けるのに真偽が判定出来ない命題があるからです。

では真偽表を使わないでどう真偽を判定するかと言うと、「風が吹けば桶屋が儲かる」みたいにして真と分かっている知識から始めて、到達した知識を真、到達出来ない物を偽と呼びます。記号で書くと、P -> Q　で Q -> R なら P -> R のような推論規則になります。この証明があれば真という考え方は Heyting という人が考えたそうです。Coq では、前者に Bool 後者に Prop という別の型が使われていて、証明には Prop を使います。Prop がいわゆる真偽値では無いという部分がプログラマにとって一番引っかかる所だと思うので書いてみました。

  • Tarski 式: 普通のプログラマが真偽判定というと、真偽値とその演算(簡約)結果の事。
  • Heyting 式: Coq では、真の知識からたどり着けた奴が真

型と証明

証明が繋がっているかどうかの判定には、単にグラフを作れば良いだけのような気もしますが、Coq では関数の型チェックを使うというひねった方法をとっています(多分「桶谷が儲かる」のような個別例ではなく、「全ての自然数」のような集合を扱うのに必要なんだと思います)。証明と関数の型と言うと全然関係ないようにも思えますが、次の例を見てみましょう。

  • size : String -> Integer　(例 size("hello") => 5)
  • sqrt : Integer -> Float (例: sqrt(5) => 2.2360..)

のような関数があったら、

  • sqrt . size : String -> Float (例 sqrt(size("hello")) => 2.2360...)

なので、String や Integer のような型を命題と考えると、String -> Integer で Integer -> Float なら String -> Float という事になり、推論規則と同じです。Theorem コマンドで命題を証明する時に使う様々な戦略コマンドは Coq 内部で適当な関数合成に翻訳されます。この事を確認する為に、同じ命題を一つは直接関数を使って、もう一つは証明戦略を使って証明してみます。最初は exact コマンドと関数を使います。

Coq < Section Trivial.

Coq < Variable P Q R : Prop.

Coq < Theorem T : (P -> Q) -> (Q -> R) -> P -> R.

T < exact (fun (f : P -> Q) (g : Q -> R) (x : P) => g (f x)).

T < Qed.
exact (fun (f : P -> Q) (g : Q -> R) (x : P) => g (f x)).
T is defined

Coq < End Trivial.

同じ事を戦略コマンドでやってみます。

Coq < Section Trivial.

Coq < Variable P Q R : Prop.

Coq < Theorem T : (P -> Q) -> (Q -> R) -> P -> R.

T < intros f g x.

T < apply g; apply f; apply x.

T < Qed.
intros f g x.
apply g; apply f; apply x.
T is defined

Coq < End Trivial.

なんとなく、証明がどのように関数定義に反映されるか見ててくると思います。

今後の目標

Coq'Art p140 の例題 forall b : bool, b = true \/ b = false の証明をやる為に最初から復習しています。これから型の部分に現れる -> 以外の演算子 \/ や = などの中身に踏み込んで行きたいと思っています。本当の興味は inductive type なんだけど、なかなかそこまでたどり着けないです。

参考