Haskell - 实现一阶逻辑表达式

Question

我正在尝试使用Haskell实现FOL.一阶逻辑可以是与And和Or等连接词连接在一起的命题形式.还有量词在表达式中的范围有限.

到目前为止我所做的是:

import Data.List

data Prop 
    = Not Prop
    | Prop And Prop
    | Prop Or Prop
    | Prop Impl Prop
    | Prop Equiv Prop
    | ForAll String Prop
    | Exists String Prop
    deriving (Eq, Ord)

但是我收到了这个错误:

 Multiple declarations of ‘Prop’

Answer 1

您试图Prop多次使用构造函数名称(第一个单词始终是构造函数名称).看来,要使用中缀构造And,Or和其他人.为了编写中缀,你需要将构造函数名称放在反引号中.

data Prop
    = Not Prop
    | Prop `And` Prop
    ...

Answer 2

声明代数数据类型时,声明的右侧是此类型的可能构造函数的"列表".但是,构造函数只是函数,这意味着它们用于前缀表示法.您尝试以And中缀方式使用eg 构造函数,但不起作用.

以下代码运行良好:

data Prop
    = Not Prop
    | And Prop Prop
    | Or Prop Prop
    | Impl Prop Prop
    | Equiv Prop Prop
    | ForAll String Prop
    | Exists String Prop
    deriving (Eq, Ord)

但是,您可以定义模仿构造函数的函数,例如 -

propAnd :: Prop -> Prop -> Prop
propAnd a b = And a b

并使用反引用以中缀方式使用这些:a `propAnd` b. 正如评论中所建议的那样,这不是必需的,因为And已经可以在中缀方式中使用:a `And` b

另一种选择是以中缀方式定义构造函数:

data Prop
    = Not Prop
    | Prop `And` Prop
    | Prop `Or` Prop
    | Prop `Impl` Prop
    | Prop `Equiv` Prop
    | ForAll String Prop
    | Exists String Prop
    deriving (Eq, Ord)

然后这两个a `And` b和And a b工作.

注意:您的数据类型是无限的,因为所有构造函数都使用一个或多个Props.我认为你还应该包括一些"原子"构造函数.