Haskell

Question

我有以下内容：

type Name = String
data Prop
= Var Name
| F
| T
| Not Prop
| Prop :|: Prop
| Prop :&: Prop
deriving (Eq, Read)
infixr 2 :|:

类型 Prop 表示一个命题公式。 p、q等命题变量可以用Var"p"和Var"q".

表示

F 和 T 是 False 和 True 的常量布尔值。

Not代表否定(~或¬)

:|: 和 :&: 代表析取（/）和合取（/\）

我们可以写出逻辑命题：

( Var "p" :|: Var "q") :&: ( Not (Var "p") :&: Var "q")

我要做的是：将 Not、:|: 和 :&: 替换为 ~、/ 和 /\，方法是使 Prop 成为 class Show 的一个实例，这样下面的内容就会成立:

test_ShowProp :: Bool
test_ShowProp =
show (Not (Var "P") :&: Var "Q") == "((~P)/\Q)"

这是我目前的实现：

instance Show Prop where
    show (Var p) = p 
    show (Not (Var p)) = "(~" ++ p ++ ")" 
    show (Var p :|: Var q) = p ++ "\/" ++ q
    show (Var p :&: Var q) = p ++ "/\" ++ q

但这并没有涵盖所有情况，只是基本情况。我应该如何继续实施，以便它处理任何命题公式，而不仅仅是硬编码的公式？因为此刻

(Var "p" :&: Var "q")

outputs: p/\q

但是

Not (Var "p" :&: Var "q")

outputs: Non-exhaustive patterns in function show

Answer 1

您想在定义中递归调用 show。所以 Not 的例子是

show (Not p) = "(~" ++ show p ++ ")"

Answer 2

您应该只匹配公式中的一个 "layer"，即只有一个构造函数，并利用子公式的递归。例如，

show (Not f) = "(~" ++ show f ++ ")"

将应用于任何以否定开头的公式，即使在该否定下有一个非变量子公式。

正确使用括号可能很棘手。您需要大方地使用括号或定义 showsPrec。如果你是初学者，我会推荐前者，它不需要应付优先级。

Haskell - 命题逻辑

Haskell - propositional logic

forms

logic

logical-operators