在Haskell中将命题逻辑扩展为模态逻辑 [英] Extending propositional logic to modal logic in Haskell

问题描述

我已经在Haskell中编写了一些代码，用于对命题逻辑进行建模

I have written some code in Haskell for modeling propositional logic

data Formula = Prop {propName :: String} 
            | Neg Formula 
            | Conj Formula Formula 
            | Disj Formula Formula
            | Impl Formula Formula 
            | BiImpl Formula Formula 
    deriving (Eq,Ord)

但是，由于数据类型是封闭的，因此没有自然的方法可以将此扩展到Modal Logic.因此，我认为我应该改用类.这样，以后我可以轻松地在不同的模块中添加新的语言功能.问题是我不知道该怎么写.我想要以下类似的东西

However, there is no natural way to extend this to Modal Logic, since the data type is closed. Therefore, I thought I should use classes instead. That way, I can easily add new language features in different modules later on. The problem is that I don't exactly know how to write it. I would like something like the following

type PropValue = (String,Bool) -- for example ("p",True) states that proposition p is true
type Valuation = [PropValue]    

class Formula a where
    evaluate :: a -> Valuation -> Bool

data Proposition = Prop String

instance Formula Proposition where
    evaluate (Prop s) val = (s,True) `elem` val 

data Conjunction = Conj Formula Formula -- illegal syntax

instance Formula Conjunction where
    evaluate (Conj φ ψ) v = evaluate φ v && evaluate ψ v

错误当然是在连接词的定义中.但是，我不清楚如何重写它才能使其正常工作.

The mistake is of course in the definition of Conjunction. However, it is unclear to me how I could rewrite it so that it works.

推荐答案

这应该有效:

data Conjunction f = Conj f f

instance Formula f => Formula (Conjunction f) where
    evaluate (Conj φ ψ) v = evaluate φ v && evaluate ψ v

但是，我不确定类型类是否是您要实现的目标的正确工具.

However, I am not sure type classes are the right tool for what you are trying to achieve.

也许您可以旋转使用显式类型级别的仿函数并对其进行重复操作:

Maybe you could give a whirl to using explicit type level functors and recurring over them:

-- functor for plain formulae
data FormulaF f = Prop {propName :: String} 
            | Neg f
            | Conj f f
            | Disj f f
            | Impl f f
            | BiImpl f f

-- plain formula
newtype Formula = F {unF :: FormulaF Formula}

-- functor adding a modality
data ModalF f = Plain f
             | MyModality f
-- modal formula
newtype Modal = M {unM :: ModalF Modal}

是的，这并不是十分方便，因为诸如 F，M，Plain 之类的构造函数有时会妨碍您的工作.但是，与类型类不同，您可以在此处使用模式匹配.

Yes, this is not terribly convenient since constructors such as F,M,Plain get sometimes in the way. But, unlike type classes, you can use pattern matching here.

另一种选择是使用GADT:

As another option, use a GADT:

data Plain
data Mod
data Formula t where
   Prop {propName :: String} :: Formula t
   Neg  :: Formula t -> Formula t
   Conj :: Formula t -> Formula t -> Formula t
   Disj :: Formula t -> Formula t -> Formula t
   Impl :: Formula t -> Formula t -> Formula t
   BiImpl :: Formula t -> Formula t -> Formula t
   MyModality :: Formula Mod -> Formula Mod 

type PlainFormula = Formula Plain
type ModalFormula = Formula Mod

这篇关于在Haskell中将命题逻辑扩展为模态逻辑的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！