Haskell - 命题逻辑答案

【问题标题】：Haskell - propositional logic [duplicate]Haskell - 命题逻辑
【发布时间】：2019-01-04 22:08:18
【问题描述】：

我有以下几点：

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")

我要做的是：通过将 Prop 设为 Show 类的实例，将 Not、:|: 和 :&: 替换为 ~、/ 和 /\，这样以下内容就会成立：

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")

输出：p/\q

但是

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

输出：函数显示中的非详尽模式

【问题讨论】：

标签： forms haskell logic logical-operators

【解决方案1】：

您应该只匹配公式的一个“层”，即只匹配一个构造函数，并利用子公式的递归。例如，

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

将适用于以否定开头的任何公式，即使在该否定下存在非可变子公式。

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

【讨论】：

【解决方案2】：

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

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

【讨论】：