謂詞邏輯在Haskell

Question

我已經使用以下數據結構，用於在Haskell命題邏輯的表示：

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

在此結構的任何意見是受歡迎的。

但是，現在我想擴展我的算法來處理FOL謂詞邏輯。 什麼是在Haskell中表示FOL的好方法？

我見過的版本幾乎都是上述的擴展，以及基於更經典的上下文無關語法的版本。有沒有關於這方面的文獻，可以推薦？

Answer 1

這就是所謂的higher-order abstract syntax。

第一個解決方案：使用Haskell的lambda。 一個數據類型可以是這樣的：

ForAll (\x -> Exists (\y -> Equals (Add x y) (Mul x y)))) 

對此進行了詳細在The Monad Reader文章描述：

data Prop 
    = Not Prop 
    | And Prop Prop 
    | Or Prop Prop 
    | Impl Prop Prop 
    | Equiv Prop Prop 
    | Equals Obj Obj 
    | ForAll (Obj -> Prop) 
    | Exists (Obj -> Prop) 
    deriving (Eq, Ord) 

data Obj 
    = Num Integer 
    | Add Obj Obj 
    | Mul Obj Obj 
    deriving (Eq, Ord) 

，你可以寫一個公式。強烈推薦。

解決方法二：

使用字符串像

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

data Obj 
    = Num Integer 
    | Var String 
    | Add Obj Obj 
    | Mul Obj Obj 
    deriving (Eq, Ord) 

然後，你可以這樣寫

ForAll "x" (Exists "y" (Equals (Add (Var "x") (Var "y"))) 
           (Mul (Var "x") (Var "y")))))) 

優勢的公式是，你可以很容易地顯示公式（很難顯示Obj -> Prop函數）。缺點是您必須在碰撞（〜alpha轉換）和替換（〜beta轉換）時編寫更改的名稱。在兩種方案中，可以使用GADT，而不是兩個數據類型：

data FOL a where 
    True :: FOL Bool 
    False :: FOL Bool 
    Not :: FOL Bool -> FOL Bool 
    And :: FOL Bool -> FOL Bool -> FOL Bool 
    ... 
    -- first solution 
    Exists :: (FOL Integer -> FOL Bool) -> FOL Bool 
    ForAll :: (FOL Integer -> FOL Bool) -> FOL Bool 
    -- second solution 
    Exists :: String -> FOL Bool -> FOL Bool 
    ForAll :: String -> FOL Bool -> FOL Bool 
    Var :: String -> FOL Integer 
    -- operations in the universe 
    Num :: Integer -> FOL Integer 
    Add :: FOL Integer -> FOL Integer -> FOL Integer 
    ... 

解決方案三：用數字來表示，其中的變量綁定，其中較低的手段更深。例如，在ForAll（Exists（Equals（Num 0）（Num 1）））中，第一個變量將綁定到Exists，第二個綁定到ForAll。這被稱爲de Bruijn數字。見I am not a number - I am a free variable。

Answer 2

在這裏添加一個答案似乎是適當的，提及功能性珍珠Using Circular Programs for Higher-Order Syntax，由Axelsson和Claessen在ICFP 2013和briefly described by Chiusano on his blog上發佈。

該解決方案巧妙地將Haskell語法（@ sdcvvc的第一個解決方案）的簡潔用法與輕鬆打印公式（@ sdcvvc的第二個解決方案）的功能相結合。

forAll :: (Prop -> Prop) -> Prop 
forAll f = ForAll n body 
    where body = f (Var n) 
     n = maxBV body + 1 

bot :: Name 
bot = 0 

-- Computes the maximum bound variable in the given expression 
maxBV :: Prop -> Name 
maxBV (Var _ ) = bot 
maxBV (App f a) = maxBV f `max` maxBV a 
maxBV (Lam n _) = n 

該解決方案將使用一個數據類型，如：

data Prop 
    = Pred String [Name] 
    | Not Prop 
    | And Prop Prop 
    | Or  Prop Prop 
    | Impl Prop Prop 
    | Equiv Prop Prop 
    | ForAll Name Prop 
    deriving (Eq, Ord) 

但是允許你寫公式爲：

forAll (\x -> Pred "P" [x] `Impl` Pred "Q" [x])