我一直在使用以下数据结构来表示 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 的好方法是什么?
我见过的版本 - 几乎 - 上面的扩展,以及基于更经典的上下文无关语法的版本。有没有这方面的文献,可以推荐?
最佳答案
这被称为 higher-order abstract syntax .
第一个解决方案:使用 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))))
这在 The 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
函数)。缺点是您必须在碰撞(~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
...
第三种解决方案 :使用数字表示变量的绑定(bind)位置,较低的表示较深。例如,在 ForAll (Exists (Equals (Num 0) (Num 1))) 中,第一个变量将绑定(bind)到 Exists,第二个变量将绑定(bind)到 ForAll。这被称为 de Bruijn 数字。见 I am not a number - I am a free variable .
关于haskell - Haskell 中的谓词逻辑,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/3228856/