谓词逻辑在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])