在 Haskell 中解析形式逻辑

Question

我正在尝试解析以下语言。

formula ::=  true  
         |  false  
         |  var  
         |  formula & formula  
         |  ∀ var . formula
         |  (formula)

    var ::=  letter { letter | digit }*

我一直在 Haskell wiki 上关注 this article，并使用 Parsec 组合器创建了以下解析器。

module LogicParser where

import System.IO
import Control.Monad
import Text.ParserCombinators.Parsec
import Text.ParserCombinators.Parsec.Expr
import Text.ParserCombinators.Parsec.Language
import qualified Text.ParserCombinators.Parsec.Token as Token

-- Data Structures
data Formula = Var String
             | TT
             | FF
             | Con Formula Formula
             | Forall String Formula
               deriving (Show)

-- Language Definition
lang :: LanguageDef st
lang =
    emptyDef{ Token.identStart      = letter
            , Token.identLetter     = alphaNum
            , Token.opStart         = oneOf "&."
            , Token.opLetter        = oneOf "&."
            , Token.reservedOpNames = ["&", "."]
            , Token.reservedNames   = ["tt", "ff", "forall"]
            }


-- Lexer for langauge
lexer = 
    Token.makeTokenParser lang


-- Trivial Parsers
identifier     = Token.identifier lexer
keyword        = Token.reserved lexer
op             = Token.reservedOp lexer
roundBrackets  = Token.parens lexer
whiteSpace     = Token.whiteSpace lexer

-- Main Parser, takes care of trailing whitespaces
formulaParser :: Parser Formula
formulaParser = whiteSpace >> formula

-- Parsing Formulas
formula :: Parser Formula
formula = conFormula
        <|> formulaTerm
        <|> forallFormula

-- Term in a Formula
formulaTerm :: Parser Formula
formulaTerm = roundBrackets formula
            <|> ttFormula
            <|> ffFormula
            <|> varFormula

-- Conjunction
conFormula :: Parser Formula
conFormula = 
    buildExpressionParser [[Infix (op "&" >> return Con) AssocLeft]] formula

-- Truth
ttFormula :: Parser Formula
ttFormula = keyword "tt" >> return TT

-- Falsehood
ffFormula :: Parser Formula
ffFormula = keyword "ff" >> return FF

-- Variable
varFormula :: Parser Formula
varFormula =
    do  var <- identifier
        return $ Var var

-- Universal Statement 
forallFormula :: Parser Formula
forallFormula = 
    do  keyword "forall"
        x <- identifier
        op "."
        phi <- formulaTerm
        return $ Forall x phi

-- For running runghc
calculate :: String -> String
calculate s = 
    case ret of
        Left e ->  "Error: " ++ (show e)
        Right n -> "Interpreted as: " ++ (show n)
    where 
        ret = parse formulaParser "" s

main :: IO ()
main = interact (unlines . (map calculate) . lines)

问题是 & 运算符，我试图在 how the article parses expressions 上对其建模，使用 Infix 函数并将其传递给运算符列表和解析器来解析术语.但是，解析器没有按预期运行，我无法弄清楚原因。以下是所需行为的一些示例：

true                         -- parsing -->      TT
true & false                 -- parsing -->      Con TT FF
true & (true & false)        -- parsing -->      Con TT (Con TT FF)
forall x . false & true      -- parsing -->      Con (Forall "x" FF) TT

但是目前解析器没有产生任何输出。感谢任何帮助。

Answer 1

您的代码中的问题是，您尝试解析 formula 而第一次尝试是解析 formulaCon。然后这首先尝试解析一个 formula，即你创建一个无限递归 而不消耗任何输入 .

要解决这个问题，您必须构建语法。像这样定义您的术语（请注意，所有这些术语在递归返回 formula 之前都会消耗一些输入）：

formulaTerm = ttFormula
          <|> ffFormula
          <|> varFormula
          <|> forallFormula
          <|> roundBrackets formula

forallFormula = do
  keyword "forall"
  x <- identifier
  op "."
  phi <- formula
  return $ Forall x phi

公式可以是单个术语，也可以是由术语、运算符和另一个公式组成的连词。为确保解析所有输入，首先尝试解析连词，如果失败，则解析单个术语：

formula = (try formulaCon) <|> formulaTerm

最后一个formulaCon可以这样解析：

formulaCon = do
  f1 <- formulaTerm
  op "&"
  f2 <- formula
  return $ Con f1 f2

此解决方案的缺点是连词现在是右结合的。

Answer 2

我想我通过改写语法设法解决了问题，连词仍然是左结合的：

formula :: Parser Formula
formula = conFormula
        <|> formulaTerm

formulaTerm :: Parser Formula
formulaTerm = roundBrackets formula
            <|> ttFormula
            <|> ffFormula
            <|> varFormula
            <|> forallFormula

conFormula :: Parser Formula
conFormula = 
    buildExpressionParser [[Infix (op "&" >> return Con) AssocLeft]] formulaTerm

这成功解析了以下内容。

在 Haskell 中解析形式逻辑

Parsing a Formal Logic in Haskell

parsing

haskell

parsec