1

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

到目前为止我所做的是：

导入数据列表

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’
4

3 回答 3

6

您试图Prop多次用作构造函数名称（第一个单词始终是构造函数名称）。似乎您想对And,Or和其他人使用中缀构造函数。为了编写它们中缀，您需要将构造函数名称放在反引号中。

data Prop
    = Not Prop
    | Prop `And` Prop
    ...
于 2014-11-25T13:09:58.870 回答
6

当您声明代数数据类型时，声明的右侧是该类型的可能构造函数的“列表”。但是，构造函数只是函数，这意味着它们以前缀表示法使用。您尝试以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。我认为您还应该包括一些“原子”构造函数。

于 2014-11-25T13:11:04.737 回答
3

你说

...
| Prop And Prop
...

你需要说的是

...
| And Prop Prop
...

（对于所有其他人也是如此）。构造函数名称必须放在第一位。

于 2014-11-25T13:08:47.387 回答