哈斯克爾 - 實現一階邏輯表達式

Question

我想用Haskell實現FOL。一階邏輯可以用連接詞連接在一起的命題形式，如And和Or。還有一些量詞的表達範圍有限。

我所做的到目前爲止是：

進口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

當你聲明一個代數數據類型時，聲明的右邊是這個類型的可能構造函數的「列表」。但是，構造函數只是函數，這意味着它們用於前綴符號。您嘗試使用例如And構造函數以不中用的中綴方式。

下面的代碼工作得很好：

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都有效。

注意：你的數據類型是無限的，因爲所有的構造函數都帶有一個或多個Prop s。我認爲你還應該包括一些「原子」構造函數。

Answer 2

你說

... 
| Prop And Prop 
... 

什麼你需要說的是

... 
| And Prop Prop 
... 

（對所有其他人也是如此）。構造函數的名字必須先來第一個。

Answer 3

您試圖多次使用Prop作爲構造函數名稱（第一個單詞始終是構造函數名稱）。看起來你想使用And，Or和其他的中綴構造函數。爲了將它們寫入中綴，你需要將構造函數名稱反引號。

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