Haskell で LK の定理証明系を書いた

数学基礎論の講義で Gentzen の LK を習ったので、ここ数日間ずっと定理証明支援系を書いてました。単に書いただけなら普通な気がするんですが、興が乗って Template Haskell、準クォート、GADTs、型族、DataKinds などをフル活用した無駄にリッチなものが出来てしまったので紹介します。DataKinds や Supeclass equality を使っている関係上 GHC 7.4.* でないと動かないです。

ソースコード一式はこちら。

簡単な紹介

LKの推論規則を定義しているのが LKRules.hs です。以下そこからの一部抜粋。

{-# LANGUAGE QuasiQuotes, UnicodeSyntax #-}
module LKRules where
import SequentTypes
import SequentMacros

isInitial :: Sequent -> Bool
isInitial [lkseq| a |- b |] = a == b

[rule|
# Cut
  Γ |- Δ, A   A, Σ |- Π
--------------------------- cut
       Γ, Σ |- Δ, Π

# Contraction
 Γ |- Δ, A, A
--------------- contractR
 Γ |- Δ, A

# Rules for AND
 Γ ├ Δ, A   Σ ├ Π, B
-------------------------- andRight
  Γ, Σ ├ Δ, Π, A ∧ B

# Rules for OR
 A, Γ ├ Δ   B, Σ |- Π
-------------------------- orLeft
  A ∨ B, Γ, Σ |- Δ, Π

 Γ ├ Δ, A
---------------- orRightR
 Γ ├ Δ, A ∨ B

# Rules for Implies
  Γ ├ Δ, A   B, Σ ├ Π
--------------------------- implLeft
  A → B , Γ, Σ ├ Δ, Π

# Rules for Not
      Γ ├ Δ, A
------------------ notLeft
 ¬ A, Γ ├ Δ
|]

はい。ご覧の通り、規則の定義をそのまま書き下す だけで、各規則をシーケントに適用/逆適用する函数を 自動生成 してくれます。これぞ準クォートの威力！スバラシイ。推論規則の図から実際のコードを生成しているのが SequentMacros.hs です。

では、これを読み込んで推論規則の型を見てみましょう。

ghci> :l LKRules.hs
Ok, modules loaded: LKRules, SequentTypes, SequentMacros.

ghci> :t cut
cut
  :: Rule
       ([] *)
       ((:)
          * Formula ((:) * (Index 'Z 'LHS) ((:) * (Index 'Z 'RHS) ([] *))))

うへえ、混み合ってますね。これを読み易く整理するとこうなります。

ghci> :t cut
cut
  :: Rule [] [Formula, Index Z LHS, Index Z RHS]

これは、「正順に適用する場合は何も引数を取らず、逆適用する場合は論理式と、最初の式の左辺から取り出すの論理式の長さ、右辺から取り出す論理式の長さを引数にとる推論規則」と読みます。どういうこと？ Cut の推論図を引用しましょう。

  Γ |- Δ, A   A, Σ |- Π
--------------------------- cut
       Γ, Σ |- Δ, Π

要は三段論法¹です。上から下を推論する場合は曖昧性の問題はないですが、下から上を導出する際には、

間に挟まれている A に何を使うか？
ΓとΣ、ΔとΠの境界はどこか？

といったことを指定してやる必要性があります。そこで、逆適用の際にはAに当る論理式、ΓとΠの長さを引数として取るので、そのことが型に残されています。

因みに、Rule の定義は以下の通りです。

type family   (:~>) (a :: [*]) (f :: *)
type instance '[] :~> f = f
type instance (a ': b) :~> f = a -> b :~> f

data Rule :: [*] -> [*] -> * where
  Rule :: { ruleName :: String
          , apply   :: as :~> ([Sequent] -> [Sequent])
          , unapply  :: bs :~> ([Sequent] -> [Sequent])}
       -> Rule as bs

型のリストから実際に適用/逆適用を行う函数の型を生成しているわけです。

他の推論規則の型を見てみるとこうなります。

ghci> :t implLeft
implLeft :: Rule [] [Index 'Z 'LHS, Index 'Z 'RHS]

ghci> :t andLeftR
andLeftR :: Rule [Formula] []

ghci> :t notRight
notRight :: Rule [] []

いい感じですね！

簡単な証明支援系

上のライブラリを使って書いた証明支援系が、assistant.hsです。まだひたすら進んでいくだけの簡単な機能しかなくて、例えば適用の取消をしたりすることは出来ませんが、一通り動きます。

例えば、Peirce の法則 $((P \to Q) \to P) \to P$ の証明は次のように行います。

$ ./assistant
|- ((P->Q)->P)->P
----------------------
Goal:  |- ((P → Q) → P) → P
> right
----------------------
Goal: (P → Q) → P |- P
> contractR
----------------------
Goal: (P → Q) → P |- P, P
> left () (P)
----------------------
Goal:  |- P, P → Q
> right
----------------------
Goal: P |- P, Q
> weakenR
complete: P |- P
complete: P |- P
["right","contractR","left () (P)","right","weakenR"]

最後のゴールから逆算して逆適用していくわけです。曖昧性のないときは、適用規則の名前を略すことが出来ます。例えば、最初の right は implRight の、二番目の left は implLeft のことです。

こうして全部のシークエントが始式 $A \vdash A$ まで還元されたら証明終了となって、最後に左下から順に適用した規則の列が出力されます。

めくるめく型の応酬

ところで、先程の left つまり implLeftの引数を見てみると、長さを取る筈なのに left () (P) と式の列を取っていますね？こうしたことを可能にしているのが RuleArgument 型クラスの toArg 函数です（SequentTypes.hs にあります）。Human readable なように左端から論理式列をマッチさせて、その長さを返すような処理をしています。データ表現としては左辺の式は正順のリストですが、右辺式はリストを反転して右側がリストの先頭になるようにしていて左辺と右辺とでする処理がちがうので、型にLHSやRHSでタグ付けをしている訳です。

今のところ論理式の列は規則中に高々二つしか出て来ないので、全部左端から一致する形で同一化しています。なので、新たに $\Delta, \Gamma, \Sigma \vdash A$ のような形のシーケントを扱う規則を追加した場合、一々同じ部分を書く必要性があります。例としては、

$A, B, C, D, E \vdash F$

みたいなシーケントが与えられたとき、 $\Delta = (A, B), \Gamma = C, \Sigma = (D, E)$ として推論規則 rule を適用したい場合は

rule (A,B) (A,B,C)

などと重複して指定してやる必要性があります。多分。²

SequentTypes.hs では、 assistant を書く時に便利なように

unapplyList :: (ListToVector (Length b), ApplyVec (Length b) b)
            => Rule a b -> [String] -> [Sequent] -> Maybe ([Sequent] -> [Sequent])
applyList :: (ListToVector (Length as), ApplyVec (Length as) as)
          => Rule as b -> [String] -> [Sequent] -> Maybe ([Sequent] -> [Sequent])

と云う二つのヘルパ函数を定義しています。型からもわかるとおり、これは文字列（=引数）のリストをルールに適用ないし逆適用する函数です。途中で長さ付きベクトルに変換して、それから適用しています。

この函数を使ってassistant.hs ルールを一括適用しているところを見てみましょう。

case words cmd of
  ("cut":args) -> unapplyList cut args [fm]
  ("permutationL":args) -> unapplyList permutationL args [fm]
  ("permutationR":rest) -> unapplyList permutationR rest [fm]
  ("contractL":rest) -> unapplyList contractL rest [fm]
  ("contractR":_) -> Just $ unapply contractR
  ("weakenL":_) -> Just $ unapply weakenL
  ("weakenR":_) -> Just $ unapply weakenR
  ("andRight":args)
    | [lkseq| as |- gs, a ∧ b |] <- fm -> unapplyList andRight args [seqs| as |- gs |]
  ("andLeftR":_) -> Just $ unapply andLeftR
... many other lines...

実は、ちょっとこれは不正をしています、妙ちきりんな型エラーが出て仕舞うので、ベクトルを [*] :> fs に適用する為の型クラス ApplyVec を見てみましょう。

class (List len ~ xs) => ApplyVec len xs where
  type List (len :: Nat) :: [*]
  applyVec :: (xs :~> a) -> [Sequent] -> Vector String len -> Maybe a

instance ApplyVec Z '[] where
  type List Z = '[]
  applyVec f _ VNil = Just f

instance (RuleArgument x, ApplyVec len xs) => ApplyVec (S len) (x ': xs) where
  type List (S len) = List (S len)
  applyVec f s (VCons x xs) =
      case f <$> toArg s x of
        Just f' -> applyVec f' s xs
        Nothing -> Nothing

スーパークラスで型同値判定を使っているので、これは関数従属性とほぼ同値です。関数従属性で定義しなおすと、ApplyVecの頭部は

class ApplyVec len xs | len -> xs where

と書き換えることが出来ます。しかし、これでは具合が悪いです。何故ならこれでは「型リストの長さによって内容が一意に決定される」と云う意味になってしまって、実際 GHC 7.0.* 系ではLKRules.hsのコンパイルが通らなくなります³。これは、permutationL と permutationR の型を見てみると、

ghci> :t permutationL
permutationL :: Rule [Index 'Z 'LHS] [Index 'Z 'LHS]

ghci> :t permutationR
permutationR :: Rule [Index 'Z 'RHS] [Index 'Z 'RHS]

となって、長さ1のリストなのに LHS と RHS で要素となる型が食い違ってしまって一意性を破ってしまうからです。

なので、この版では関連型の List len を循環定義にして、かつそれをどこでも陽には呼ばないことで誤魔化しています。いずれの場合にせよ、型推論の停止性を脅かす虞れがあるので、UndecidableInstances 拡張を有効にする必要があります。UndecidableInstances を使わないで実現する方法があるぞ！と云う方は是非教えて頂けると嬉しいです。

……とまで書いて、この版を GHC 7.4.1 に喰わせてみたら何故か関数従属性版もコンパイル通っちゃいました orz これは何でだろう……？型族+スーパークラス文脈型同値性に desugar されるからとかかなあ。うーむ。

今後の展望

今後改良すべきところがあるとすれば以下の感じでしょうか。

述語論理に対応する
- 置換や変数の出現を陽に扱う必要性があるので、自動生成は難しそう……。
命題論理の範囲での自動定理証明
- これは出来ることが証明されていますし、アルゴリズムも非常に簡明なので実装するだけです。推論規則だけ与えてそこから自動証明系を生成するのは無理ですが……。ただ、全部複製しないで必要なものだけ複製するようにするとか、左辺の $\wedge$ や右辺の $\vee$ を単なるコンマにバラすのを一々処理として書き下そうとか厳密にルールだけで記述しようと思うと面倒そうです。
assistant に undo 機能を付ける
推論規則のヘルプ機能
論理式だけでなくて、簡単なL-論理式を扱えるようにしたい
- これは大変そう……。

まあ自動定理証明が一番今からやろうとうするには簡単そうですね。この場合、上で作り上げてきた機能は余り使わなそうですが……。

命題論理の自動定理証明のアルゴリズムは、風呂入りながら「交換規則と弱化規則と縮約規則を駆使して全式を引き回して、左右辺の $\wedge$ や $\vee$ をバラすのを自動で挿入するようにすればいいな」とすぐに思い浮かびました。思い浮かんだ後で「あれ？これどっかで見たことあるぞ……？」と思ったら次の本でした。

これは、中高生〜大学一年向けの数学読み物シリーズの『アウト・オブ・コース』シリーズの一つで、僕も小六か中学時代に読んだんですが、これに出て来る「○×ゲーム」と云うものが、本質的には LK を使った命題論理の定理自動証明と等価なものです。

公式ページによると

高校生・大学生に贈る数学入門シリーズやさしい！　面白い！　ためになる！三拍子そろった課外読み物。最近の数学をもう一度学び直したいという社会人にも好適！　四六判並製

とのことなので、中高生に限らず興味のある方は是非読まれては如何でしょうか。豊富なパズル（何と犯人当てみたいなものもある！）の例や平易な説明を通して、記号論理学に親しめるインフォーマルな入門書として最適な一冊だと思います。興味を持たれた方は是非。

厳密には三段論法ではないので、これを三段論法と呼ぶと（数理でない）論理学者に怒られるらしい↩︎
多分、と云うのは実際にそういうルールで試してない、と云う意味です。↩︎
また、GHC 7.0.* には DataKinds がないので、その場合は EmptyDataDecls などを使って頑張る必要があります。↩︎

Haskell で LK の定理証明系を書いた konn-san.com

簡単な紹介

簡単な証明支援系

めくるめく型の応酬

今後の展望

Comments