日々の流転

λ. 計算機言語で定理証明 (Proof Party.JP)

計算機言語で定理証明とかいう、なんだか良く分からないし怖そうなイベントに参加してきた。

Agdaについては池上さんやranhaさんが紹介してくれるだろうから、対話型定理証明器をdisって、自動定理証明器の素晴らしさを語ろうと思っていたのだが準備が間に合わず、会場でずっとごにょごにょ作業していた。あんまり他の人の話を聞いてなくて済みません m(_ _)m

しかし、対話型定理証明器をdisろうと思っていたのだけど、私がそんなことをする以前にAgdaはフルボッコだった。 一方、Coqはやっぱり凄いなぁ、と思った。

お題

以下、作ったものとか色々。

さんすう

• 自然数(エンコーディングは問わず)の加算での可換法則、結合法則、分配法則を証明。
• (1 + 2 + ... + n) = n*(n+1) / 2 の証明

自動定理証明器である The E Equational Theorem Prover (eprover)に証明させてみた(nat.tptp)。 帰納法が必要なのだけど、普通の自動定理証明器は公理型(axiom schema)を書けないので、帰納法のインスタンスを個別に書く必要があって面倒くさい。 また、割り算の定義が面倒くさかったので、(1 + 2 + ... + n) = n*(n+1) / 2 の代わりに両辺をニ倍した (1 + 2 + ... + n)*2 = n*(n+1) を扱っている。

おまけに、Jahobでも証明をしてみた(Nat.java)。 実行結果(jahob-nat.txt)。 (1 + 2 + ... + n) = n(n+1) / 2 の証明に関しては、ホーア論理 - ヒビルテ(2003-05-16)も参照。

すうがく

• Bolzano–Weierstrassの定理(収束するとかいうヤツの方)
• 中間値の定理(The Intermediate Value Theorem)
• むしろ実数の構成周辺を埋める?

時間がなくて手を出せず。

kikxさんがCoqで華麗に証明していて痺れた。

アルゴリズムの性質

• concat(l1,concat(l2,l3)) = concat(concat(l1,l2),l3)を証明する。
• reverse (reverse list) = list : リストのリバース　のリバースが元のリストと等しい事を証明する。
• あるソート関数がちゃんとソートする事を証明?(ソート関数が何かはご自由)

concatとreverseに関する証明は「さんすう」と同様にeproverに証明させた(list.tptp)。 この問題は「さんすう」よりも遥かに簡単。

ソートに関しては、バブルソートの部分正当性をJahobで証明した(BubbleSort.java, Node.java)。 実行結果(jahob-bubblesort.txt)。 本当は最初はクイックソートの方の証明を試みていた(Quicksort.java)のだけど、現在公開されているJahobは関数呼び出しを正しく扱えないようなので断念。 あと、論文 An Integrated Proof Language for Imperative Programs に書いてあったカッコいい機能を使いたい場面があったのだけど、現在公開されているバージョンには実装されてなくて、しょぼーんという感じだった。

それから、こないだクイックソート関数をAgdaで定義したので、これがちゃんとソートを行う関数になっていることを証明するというのも、時間があったらやってみたかった。 まあ、これは出来るのは分かりきっていて、面倒くさいだけの話だけど。

数理論理学

• 1階命題論理でresolutionが成り立つ事を示す
• 直観主義論理での二重否定除去と排中律の同値性

resolutionに関しては、自動定理証明器の基づいているものなので、まあ導出できて当然。 resolution.tptp

二重否定除去と排中律の同値性については、普通の自動定理証明器は直観主義論理ではなく古典論理に基づいているので、パス。 ところで、そういえば直観主義論理のための自動定理証明器というのは、あまり聞かないな。何でだろう……

自動定理証明以外なら「二重否定除去⇒排中律」は以前2006-04-29にHaskellで書いた。 逆の「排中律⇒二重否定除去」も一応Haskellで書いておく(こっちはかなり自明だけど)。 命題論理の範囲ならAgdaよりもHaskellの方がお手軽。

{-# LANGUAGE RankNTypes, TypeOperators #-}

type Absurd = forall a. a
type Not a = a -> Absurd
type a `Or` b = Either a b

em2callcc :: (forall x. x `Or` Not x) -> (forall x. (Not (Not x) -> x))
em2callcc em nnx =
    case em of
      Left x -> x
      Right nx -> nnx nx

パズル

• 何か簡単なモノ
• 最もスタンダードなハノイの塔で、最短の手数が(2^n)-1に成る事を示す。

時間がなくて手を出せず。

簡単では無い系

• Church-Rosserの定理(型無しλ計算の合流性証明)
• 古典一階命題論理の完全性証明(ヒルベルト流 Lukasiewiczの公理系)

時間がなくて手を出せず。ただ、これは自動定理証明器では難しそうだ。

Church-Rosssrの定理は以前Agda1で書いて、去年の Haskell Hackathon in 2008 September のときにAgda2向けに書き直した(ただし未公開)のだけど、束縛を nested types で表した関係で素直な再帰にならなくて、停止性検査を通っていない状態なので、この機会になんとかするというのもやってはみたかったんだけど……

その他

• お昼:
• Domino On Acid - Natural Deduction Visualized As A Game Of Dominoes
• カタン
• 焼肉

関連リンク

• #proofparty
• Proof Party の問題をCoqで挑戦 - にわとり小屋でのプログラミング日記 (2009-10-23)
• Haskell Not 98 - Yet Another Ranha (2009-10-23)
• 定理証明の会で実演した中間値の定理の証明 - 菊やんの雑記帳 (2009-10-26)
• 計算機言語で定理証明#1 - Yet Another Ranha (2009-10-27)