この記事は、「The Monad.Reader Issue 6(PDF)」にあるDan Piponi氏のエッセイが元ネタです。Dan氏の話はもっと奥深いところまで突き進むのですが、これは、その導入部分のネタを冗長に解説したものです。
何をするのかというと
ちょっとしたお遊びなんですが、Haskellを使って、「論理式における推論規則の適用」を関数化してみます。といっても、プログラムが推論規則を自動で適用して、命題の証明を見つけ出すような高尚な話ではありません。どのように推論規則を適用するかはあくまで人間が考えるのですが、その適用を関数で表現することで、
・誤った適用をすると関数がエラーを返す。
・複数の推論規則を適用して命題を証明する様子を自動で図式化する。
という事を行います。
また、ここで使う推論規則は、初歩中の初歩である、「MP(Modus Ponens)」、すなわち、
・「A->B」と「A」が証明される時、「B」が証明される。
というものに限定します。
百聞は一見に・・・ということで、実例をお見せします。まずは、「A」「B」「A->B」の3種類の「命題（Proposition）」を定義します。
# ghci mp.hs *Main> let { prop_a :: Proposition; prop_a = Symbol "A" } *Main> let { prop_b :: Proposition; prop_b = Symbol "B" } *Main> let { prop_ab :: Proposition; prop_ab = prop_a :-> prop_b } *Main> print [prop_a, prop_b, prop_ab] [A,B,(A -> B)]
次に、「A->B」「A」の2つは、「公理（Axiom）」として証明されていることとします。
*Main> let { proof_a :: Proof; proof_a = Axiom "1" prop_a } *Main> let { proof_ab :: Proof; proof_ab = Axiom "2" prop_ab } *Main> print proof_a "1" :: A *Main> print proof_ab "2" :: (A -> B)
ここで、頭についている"1"、"2"は、それぞれの公理に付けた任意の名前です。深い意味はありません。
そして、これらの証明に推論規則（MP）を適用すると、「B」の証明が得られると言う事実を次のような計算式で表します。「@@」は、推論規則（MP）を適用するという関数（2項演算）です。
*Main> let { proof_b :: Proof; proof_b = proof_ab @@ proof_a }
最後に、この証明を表示すると次のように、推論規則適用の様子が図示されます。
*Main> print proof_b | "2" :: (A -> B) | "1" :: A | ------------------------------------------------------------------------------ | MP :: B
さらに推論を積み重ねることも可能です。
*Main> let { prop_c :: Proposition; prop_c = Symbol "C"} *Main> let { prop_bc :: Proposition; prop_bc = prop_b :-> prop_c } *Main> let { proof_bc :: Proof; proof_bc = Axiom "3" prop_bc } *Main> let { proof_c :: Proof; proof_c = proof_bc @@ proof_b } *Main> print proof_c | "3" :: (B -> C) | | "2" :: (A -> B) | | "1" :: A | | ---------------------------------------------------------------------------- | | MP :: B | | ------------------------------------------------------------------------------ | MP :: C
一方、誤って推論規則を適用すると、次のように例外が発生します。
*Main> let { proof_z :: Proof; proof_z = proof_ab @@ proof_b } *Main> print proof_z *** Exception: @@ error "2" :: (A -> B) | "2" :: (A -> B) | "1" :: A | ------------------------------------------------------------------------------ | MP :: B
実装はこちら
それでは、上記の仕組みを順番に作っていきましょう。まずは、「命題（Proposition）」のデータ型を用意します。
mp.hs
infixr 5 :-> data Proposition = Proposition :-> Proposition | Symbol String | False_ deriving (Eq) source :: Proposition -> Proposition source (a :-> b) = a source _ = False_ target :: Proposition -> Proposition target (a :-> b) = b target _ = False_ instance Show Proposition where show (a :-> b) = "(" ++ show a ++ " -> " ++ show b ++ ")" show (Symbol s) = s show False_ = "_|_" not :: Proposition -> Proposition not p = p :-> False_
命題は、記号「A」もしくは、「A :-> B」という形式の再帰的な組み合わせで定義されます。後者の形式の命題から、前提部分と結論部分を取り出す補助関数が「source」と「target」です。
続いて、「証明（Proof）」のデータ型です。
mp.hs
data Proof = MP Proof Proof -- MP a->b a | Axiom String Proposition -- Axiom Name Contents deriving (Eq)
ここでは、証明とは、公理（Axiom）に指定された命題、もしくは、既に証明された２つの命題に対する推論規則（MP）の適用として定義されます。ただし、MPを適用する証明をダイレクトに構成することは許しません。次の「@@」演算子を通して構成します。
mp.hs
{- Consequence is a target of the last axiom in the proof chain. -} consequence :: Proof -> Proposition consequence (Axiom _ p) = p consequence (MP f g) = target $ consequence f infixl 5 @@ (@@) :: Proof -> Proof -> Proof f @@ g | source (consequence f) == consequence g = MP f g | otherwise = error ("@@ error " ++ show f ++ " " ++ show g) -- f:a->b, g:a
やや複雑ですが・・・、まず、補助関数「consequence」は証明の「結論」となる命題を取り出す働きがあります。一般に「証明」は、複数の証明がMPで結合された形式になりますが、たとえば、「MP (A->B) A」という証明の場合、「B」が結論（この証明によって、証明された命題）です。
次に、「@@」演算子は、「(A->B) @@ A」という順序で適用します。この場合、第1項の前提部分（Source）が第2項と一致することが、「@@」演算子が適用できる条件になります。より一般には、第1項、第2項それぞれが、長い証明（MP結合の列）の場合、第1項の結論が「A->B」で第2項の結論が「A」という条件になります。このような条件を満たさない場合、「@@」演算子を適用した結果は、「error」になります。
そして最後に、証明を図式化して表示する部分がこちらです。
mp.hs
instance Show Proof where show a@(Axiom n t) = show n ++ " :: " ++ show t show p@(MP f x) = show' 0 p where show' :: Int -> Proof -> String show' n a@(Axiom _ _) = concat ( replicate n "| " ) ++ show a show' n p@(MP f x) = let tab depth char = concat $ replicate depth char in show' (n+1) f ++ "\n" ++ show' (n+1) x ++ "\n" ++ tab (n+1) "| " ++ tab (80-(n+1)*2) "-" ++ "\n" ++ tab (n+1) "| " ++ " MP :: " ++ show (consequence p) ++ "\n" ++ tab n "| "
