Haskell - 命题逻辑

Geo*_*nat 1 forms logic haskell logical-operators

我有以下内容:

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

Prop类型代表命题公式.命题变量,例如p和q可以用Var"p"和Var"q"表示.

F和T是False和True的常数布尔值.

不代表否定(〜或¬)

:|:和:&:表示析取(/)和结合(/ \)

我们可以写出逻辑命题:

( Var "p" :|: Var "q") :&: ( Not (Var "p") :&: Var "q")
Run Code Online (Sandbox Code Playgroud)

我要做的是:通过使Prop成为Show类的实例,替换Not,:|:和:&:with~,/和/ \,以便以下内容为真:

test_ShowProp :: Bool
test_ShowProp =
show (Not (Var "P") :&: Var "Q") == "((~P)/\Q)"
Run Code Online (Sandbox Code Playgroud)

这是我到目前为止的实现:

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
Run Code Online (Sandbox Code Playgroud)

但这并不包括所有情况,只包括基本情况.我应该如何继续实施,以便解决任何命题公式,而不仅仅是硬编码公式?因为此刻

(Var "p" :&: Var "q")
Run Code Online (Sandbox Code Playgroud)

输出:p /\q

但

Not (Var "p" :&: Var "q")
Run Code Online (Sandbox Code Playgroud)

输出:功能中的非详尽模式显示

chi*_*chi 5

您应该只匹配公式的一个"层",即只匹配一个构造函数,并利用子公式的递归.例如,

show (Not f) = "(~" ++ show f ++ ")"
Run Code Online (Sandbox Code Playgroud)

将适用于以否定开头的任何公式,即使在该否定下存在非变量子公式.

正确地获得括号可能会很棘手.你需要慷慨的括号或定义showsPrec.如果你是初学者,我会推荐前者,它不需要处理优先级.