この記事はQiitaからの移転記事です

大学の講義で LK を習ったので、定理証明支援系を書こうと思った。 その前段階として、取り敢えず論理式に推論規則を適用する仕組みを作ることにした。(後はひっくりかえすだけ)

折角なので、推論規則を書いたら勝手に函数を生成してくれる準クォートを定義してそいつをつかってみた。 こんな感じに書ける。

{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-unused-imports #-}
module LKRules where
import Data.List
import LKDataTypes
import LKMacros

type Rule = [Sequent] -> Maybe Sequent

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

[rule|
# Cut

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

# Contract
 A, A, Γ |- Δ
--------------- contractL
    A, Γ |- Δ

 Γ |- Δ, A, A
--------------- contractR
 Γ |- Δ, A


# Weakening
    Γ ├ Δ
------------- weakenL
 A, Γ ├ Δ

 Γ ├ Δ
------------- weakenR
 Γ ├ Δ, A

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

      A, Γ ├ Δ
------------------ andLeftR
  A ∧ B, Γ ├ Δ

      A, Γ ├ Δ
------------------ andLeftL
  B ∧ A, Γ ├ Δ

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

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

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

# Rules for Implies
  A, Γ ├ Δ, B
-------------------------- implRight
     Γ ├ Δ, A → B

  Γ ├ Δ, A   B, Σ ├ Π
--------------------------- implLeft
  A → B , Γ, Σ ├ Δ, Π

# Rules for Not
 A, Γ ├ Δ
------------------ notRight
    Γ ├ Δ, ¬ A

      Γ ├ Δ, A
------------------ notLeft
 ¬ A, Γ ├ Δ
|]

swap s1 s2 ss = 
    let [start, end] = sort [s1, s2]
        (ls, a:rs)   = splitAt start ss
        (ls', b:rs') = splitAt (start-end+1) rs
    in ls ++ b : ls' ++ a : rs'

permutationL :: Int -> Int -> Rule
permutationL s1 s2 [ ss :|- ds ] | max s1 s2 < length ss = Just $ swap s1 s2 ss :|- ds 
permutationL _ _ _ = Nothing

permutationR :: Int -> Int -> Rule
permutationR s1 s2 [ ss :|- ds ] | max s1 s2 < length ds = Just $ ss :|- reverse (swap s1 s2 $ reverse ds)
permutationR _ _ _ = Nothing

流石に可換法則はそのまま書くのはむずかしそうなのでやめた。 準クォートにしておくと、今度は逆向きのを自動生成する機能を付けたときに Rules を一切弄らなくてすむので楽だ。 上式にない変数が下式に出て来たら、引数として外側に括り出すようにする処理とかもやっている。あと、上式に同じ文字列が出て来たらガード節をくっつけてそいつらの値が一致する、と云う条件も入れるようにしている。

GHCi で動かしてみるとこんな感じになる。

例として二重否定除去を示す。

残りのソースは以下の通り。パーザ周りにまだ繰り返しているコードがあるのでそこを今度何とかする。

{-# LANGUAGE TemplateHaskell, ViewPatterns #-}
module LKMacros where
import LKDataTypes
import Language.Haskell.TH
import Language.Haskell.TH.Quote
import Data.Char
import Data.Generics
import Control.Applicative
import Text.Parsec
import Data.List
import Data.Foldable (foldrM)
import Control.Monad.State
import qualified  Data.Map as M

lkseq :: QuasiQuoter
lkseq = QuasiQuoter { quoteType = undefined
                    , quoteDec  = undefined
                    , quoteExp  = lkSeqExp
                    , quotePat  = lkSeqPat
                    }

lkSeqExp str = dataToExpQ (mkQ Nothing anti) $ parseSequent str
  where
    anti :: [Formula] -> Maybe ExpQ
    anti gs = Just [| concat $(listE $ map (appE [| toFormulaList |] . dataToExpQ (mkQ Nothing trans)) gs) |]
    trans (Var s) | isFree s = Just $ varE (mkName s)
    trans (Var (c:cs))
        | Just prfx <- lookup c greeks = Just $ varE $ mkName $ prfx:"s"
    trans _ = Nothing
lkSeqPat str = dataToPatQ (mkQ Nothing anti) $ parseSequent str
  where
    anti :: [Formula] -> Maybe PatQ
    anti fs = Just $ foldr1 (\a b -> infixP a ('(:)) b) $ map (dataToPatQ (mkQ Nothing trans)) fs
    trans (Var str) | isFree str = Just $ varP $ mkName str
    trans (Var (c:cs))
        | Just prfx <- lookup c greeks = Just $ varP $ mkName $ prfx:"s"
    trans _ = Nothing

seqs :: QuasiQuoter
seqs = QuasiQuoter { quoteType = undefined
                   , quoteDec  = undefined
                   , quoteExp  = seqsExp
                   , quotePat  = seqsPat
                   }

isFree s = not (null s) && isLower (head s)

greeks = zip "ΓΔΣΠΘΛΞΦΩ" "gdsptlxfw"

seqsExp str = dataToExpQ (mkQ Nothing anti) $ run (sequent `sepBy` spaces) str
  where
    anti :: [Formula] -> Maybe ExpQ
    anti gs = Just [| concat $(listE $ map (appE [| toFormulaList |] . dataToExpQ (mkQ Nothing trans)) gs) |]
    trans (Var s) | isFree s = Just $ varE (mkName s)
    trans (Var (c:cs))
        | Just prfx <- lookup c greeks = Just $ varE $ mkName $ prfx:"s"
    trans _ = Nothing
seqsPat str = dataToPatQ (mkQ Nothing anti) $ run(sequent `sepBy` spaces) str
  where
    anti :: [Formula] -> Maybe PatQ
    anti fs = Just $ foldr1 (\a b -> infixP a ('(:)) b) $ map (dataToPatQ (mkQ Nothing trans)) fs
    trans (Var str) | isFree str = Just $ varP $ mkName str
    trans (Var (c:cs))
        | Just prfx <- lookup c greeks = Just $ varP $ mkName $ prfx:"s"
    trans _ = Nothing

lkf :: QuasiQuoter
lkf = QuasiQuoter { quoteType = undefined
                      , quoteDec  = undefined
                      , quoteExp  = formulaExp
                      , quotePat  = undefined
                      }

formulaExp str = dataToExpQ (const Nothing) $ parseFormula str

rule :: QuasiQuoter
rule = QuasiQuoter { quoteType = undefined
                   , quoteExp  = undefined
                   , quotePat  = undefined
                   , quoteDec  = ruleDec
                   }

ruleDec str = do
  let rules = run (many1 deducRule) str
  concat <$> mapM build rules
  where
    arrow a b = [t| $(a) -> $(b) |]
    build (from, name, to) = do
      (from', dic) <- runStateT (everywhereM (mkM renamer) from) M.empty
      pattern <- listP $ map (dataToPatQ (mkQ Nothing pat)) from'
      body    <- dataToExpQ (mkQ Nothing expq) to
      let pnames = everything (++) (mkQ [] extractName) from
          enames = everything (++) (mkQ [] extractName) to
          unknown = enames \\ pnames
          guards = patG $ map (noBindS . appE [| \xs -> and $ zipWith (==) xs (tail xs) |] . listE . map (varE . mkName . normalizeName) . snd) $ filter (not. null . drop 1 . snd) $ M.toList dic
      sig <- sigD (mkName name) $ foldr arrow [t| [Sequent] -> Maybe Sequent |] $
         map (const [t| Formula |]) unknown
      fun <- funD (mkName name) [ clause (map (varP . mkName) unknown++[return pattern])
                                  (guardedB [liftM2 (,) guards $ appE [|Just|] (return body)])
                                  []
                         , clause (wildP:map (const wildP) unknown) (normalB [|Nothing|]) []
                         ]
      return [sig, fun]
    expq :: [Formula] -> Maybe ExpQ
    expq gs = Just [| concat $(listE $ map (appE [| toFormulaList |] . dataToExpQ (mkQ Nothing $ trans varE)) gs) |]
    pat :: [Formula] -> Maybe PatQ
    pat fs = Just $ foldr1 (\a b -> infixP a ('(:)) b) $
               map (dataToPatQ (mkQ Nothing $ trans varP)) fs
    trans var (Var str) = Just $ var $ mkName $ normalizeName str
    trans _ _ = Nothing
    normalizeName [c]
        | Just prfx <- lookup c greeks = prfx : "s"
    normalizeName xs = map toLower xs
    extractName (Var v) = [normalizeName v]
    extractName _       = []
    renamer (Var name) = do
      dic <- get
      case M.lookup name dic of
        Nothing -> do
          put $ M.insert name [name] dic
          return $ Var name
        Just xs -> do
          name' <- show <$> lift (newName name)
          put $ M.insert name (name' : xs) dic
          return $ Var name'
{-# LANGUAGE DeriveDataTypeable, RecordWildCards, FlexibleInstances #-}
module LKDataTypes where
import Text.Parsec.Expr
import Text.Parsec
import qualified Text.Parsec.Token as T
import Text.Parsec.String
import Data.List
import Control.Applicative hiding (many, (<|>))
import Data.List
import Data.Either
import Data.Data (Typeable, Data)

infix  6 :|-
infixr 7 :->:
infixl 8 :\/:
infixl 9 :/\:

data Formula = Var String
             | Not Formula
             | Formula :\/: Formula
             | Formula :->: Formula
             | Formula :/\: Formula
               deriving (Read, Eq, Ord, Data, Typeable)

data Sequent = (:|-) { lefts :: [Formula], rights :: [Formula] }
             deriving (Eq, Ord, Data, Typeable)

instance Show Formula where
  showsPrec _ (Var v)    = showString v
  showsPrec d (Not f)    = showString "¬" . showsPrec 11 f
  showsPrec d (l :\/: r) = showParen (d > 7) $ showsPrec 8 l . showString " ∨ " . showsPrec 8 r
  showsPrec d (l :->: r) = showParen (d > 6) $ showsPrec 7 l . showString " → " . showsPrec 7 r
  showsPrec d (l :/\: r) = showParen (d > 8) $ showsPrec 9 l . showString " ∧ " . showsPrec 9 r

instance Show Sequent where
  showsPrec d (l :|- r) = showParen (d > 10) $ showsFs l . showString " |- " . showsFs (reverse r)
    where
      showsFs fs = foldr (.) id $ intersperse (showString ", ") $ map shows fs

greek = oneOf "ΓΔΣΠΘΛΞΦΨΩ"

lang :: T.LanguageDef ()
lang = T.LanguageDef { T.commentStart = "{-"
                     , T.commentEnd   = "-}"
                     , T.commentLine  = "#"
                     , T.nestedComments = True
                     , T.identStart     = letter <|> greek
                     , T.identLetter    = alphaNum <|> greek <|> char '\''
                     , T.opStart        = empty
                     , T.opLetter       = empty
                     , T.reservedNames  = []
                     , T.reservedOpNames = ["", "->", "\\/", "/\\", "⊃", "|-"
                                           ,"¬", "→", "∧", "∨", "^", "v", "├"
                                           ]
                     , T.caseSensitive   = True
                     }

T.TokenParser {..} = T.makeTokenParser lang

formula :: Parser Formula
formula = buildExpressionParser table term
      <?> "formula"

term = parens formula
   <|> Var <$> identifier

table = [ [ Prefix $ Not   <$ choice (map reservedOp ["", "¬"])]
        , [ Infix  ((:/\:) <$ choice (map reservedOp ["∧", "/\\", "^"])) AssocLeft ]
        , [ Infix  ((:\/:) <$ choice (map reservedOp ["∨", "\\/", "v"])) AssocLeft ]
        , [ Infix  ((:->:) <$ choice (map reservedOp ["→", "->", "⊃"])) AssocRight ]
        ]

sequent = (:|-) <$> fs <* (choice $ map reservedOp ["|-", "├"])
                <*> (reverse <$> fs)
  where
    fs = formula `sepBy` comma

parseSequent = run sequent
parseFormula = run formula

run p src =
    case parse (whiteSpace *> p <* eof) "" src of
      Left err -> error $ show err
      Right ans -> ans

class FormulaListable a where
  toFormulaList :: a -> [Formula]

instance FormulaListable Formula where
  toFormulaList = pure

instance FormulaListable [Formula] where
  toFormulaList = id

deducRule = (,,) <$> (sequent `sepBy` whiteSpace)
                 <*  lexeme (skipMany1 (char '-'))
                 <*> identifier
                 <*> sequent

Comments