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

这称为高阶抽象语法.

第一个解决方案:使用Haskell的lambda.数据类型可能如下所示:

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)

您可以将公式编写为:

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

这在Monad Reader文章中有详细描述.强烈推荐.

二解决方案:

使用像

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功能).缺点是你必须在碰撞(~α转换)和替换(~β转换)上写更改名称.在这两种解决方案中,您可以使用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数字.看我不是数字 - 我是一个自由变数.