論理式のパーサ

ウカシェビッチの公理には論理結合子は次のように否定結合子と含意結合子しかない。

P1. A -> (B -> A)
P2. (A -> (B -> C)) -> ((A -> B) -> (A -> C))
P3. (¬B -> ¬A) -> (A -> B)

これはパーサを書く練習にちょうど良いと思って、Parsec で書いてみた。ソースコードは次のようになる。

module Logic where

import Text.ParserCombinators.Parsec

atom :: Parser String
atom = do {letter; return "atom"}

negation :: Parser String
negation = do {char '~'; return "not"}

imply :: Parser String
imply = do {string "->"; return "imply"}

expression :: Parser String
expression = do {try (do {term; imply; term}) <|> term; return "expression"}

term :: Parser String
term = do {do {negation; factor} <|> factor; return "term"}

factor :: Parser String
factor = do {do {string "("; expression; string ")"} <|> atom; return "factor"}

文法チェックしかしないが、次のように入れ子になった括弧も解釈できる。入れ子になった do 記法が読みにくいかもしれないが、do 記法は複数のモナドを一つのモナドにまとめるための記法だとイメージすると読みやすくなるだろう。

また、factor が再帰呼び出しになっているが、入れ子になった括弧を処理するための定型文だ。

ghci で検証した。

Prelude> :l Logic.hs

[1 of 1] Compiling Logic ( Logic.hs, interpreted )

Ok, modules loaded: Logic.

*Logic> parseTest expression "~(~a->(a->b))"

"expression"


論理だけの作業をしていると、手で動かせる実体が欲しくなる。


[PR]
by tnomura9 | 2016-09-22 10:48 | Haskell | Comments(0)
<< 完全性定理の証明についての疑問 前件肯定 modus pone... >>