有什么守卫分析的工具吗？

Question

我是一个 Haskell 菜鸟，在阅读 Haskell 道路中的 Implications 时，我遇到了以下难题。

verdict :: Bool -> Bool -> (Bool, String)
verdict p q | not result  = (False, "LIAR")
            | result && p = (True,  "telling the truth")
            | result      = (True,  "innocent unless proven guilty")
            | otherwise   = (False, "we shouldn't get here")
  where result = (not p) || q
-- map (\x -> verdict (fst x == 1) (snd x == 1)) [(1,1),(1,0),(0,1),(0,0)]

是否有工具可以警告我其他或其他类似的逻辑错误？

Answer 1

我想我会用不同的方式编写这个函数：

-- not result
verdict True  False = (False, "LIAR")
-- result && p
verdict True  True  = (True , "telling the truth")
-- result
verdict False _     = (True , "innocent unless proven guilty")
verdict _     True  = (True , "innocent unless proven guilty")
-- otherwise
verdict _     _     = (False, "we shouldn't get here")

那么不仅对于人类来说哪些子句可以被省略（最后两个）是显而易见的，而且对于机器来说也是如此； ghc 以默认警告级别表示：

test.hs:2:5: Warning:
    Pattern match(es) are overlapped
    In an equation for ‘verdict’:
        verdict _ True = ...
        verdict _ _ = ...

一般来说检查守卫重叠当然是不可判定的；而且我不知道有什么工具会尝试给出一个大概的答案。

Answer 2

这可能更清楚地表达了您的意图：

implies :: Bool -> Bool -> Bool
p `implies` q = not p || q -- The backticks allow infix usage.

-- The assumption is that p `implies` q is a known fact.
verdict :: Bool -> Bool -> (Bool, String)
verdict p q = (result, remark)
    where
    result = p `implies` q
    remark
        | not result = "LIAR"
        | p = "telling the truth"
        | otherwise = "innocent until proven guilty"

Guards 是 Bool 值模式匹配的语法糖。有关安排模式匹配的一般提示，请参阅 Daniel Wagner 的回答。

有什么守卫分析的工具吗？

Are there any tools for guard analysis?

logic

haskell