Home Articles

UPDATE2,哈斯克尔

Asked
Viewed 1263 times
-3
  • Atom:Atom是用于描述原子句或命题的数据类型 . 这些基本上表示为字符串 .

  • 文字:文字对应原子的原子或否定 . 在此实现中,每个文字都表示为一对由布尔值组成,表示Atom的极性和实际的Atom . 因此,字面'P'表示为(True,"P"),而其否定'-P'表示为(False,"P") . 2

  • 条款:条款是文字的分离,例如PvQvRv-S . 在此实现中,它表示为文字列表 . 所以最后一个子句是[(True,"P"),(True,"Q"),(True,"R"),(False,"S")] .

  • 公式:公式是子句的结合,例如(P vQ)^(RvP v-Q)^( - P v-R) . 这是命题公式的CNF形式 . 在此实现中,它表示为子句列表,因此它是文字列表的列表 . 我们上面的示例公式将是[[(True,"P"),(True,"Q")],[(True,"R"),(True,"P"),(False,"Q")],[(False,"P"),(False) ,"P")]] .

  • 模型:(部分)模型是(部分)将真值分配给公式中的原子 . 在此实现中,这是(Atom,Bool)对的列表,即 . 原子与他们的任务 . 所以在上面的类型为Formula的例子中,如果我们将Q赋值为true而将false赋给Q则那么我们的模型将是[("P",True),("Q",False)]

好的,我写了并更新了功能

update :: Node -> [Node]

它接收一个Node并返回一个节点列表,这些节点是在一种情况下将True分配给未分配的原子而在另一种情况下分配为False(即一个案例分割) . 返回的列表有两个节点作为元素 . 一个节点包含一个公式,其中一个原子分配为True,模型使用此赋值更新,另一个节点包含公式,其中原子指定为False,模型已更新以显示此情况 . 每个节点的未分配原子列表也相应更新 . 此功能使用assign函数进行分配 . 它还使用chooseAtom函数选择要分配的文字 .

update :: Node -> [Node]
    update (formula, (atoms, model)) = [(assign (chooseAtom atoms, True) formula, (remove (chooseAtom atoms) atoms, ((chooseAtom atoms,True)) `insert` model)) , (assign (chooseAtom atoms, False) formula, (remove (chooseAtom atoms) atoms, ((chooseAtom atoms, False) `insert` model)) )]

现在我必须做同样的事情,但这次我必须实现一个变量选择启发式 . 这应该替换chooseAtom而我应该用它来编写一个函数update2

type Atom = String
    type Literal = (Bool,Atom)
    type Clause = [Literal]  
    type Formula = [Clause]
    type Model = [(Atom, Bool)]
    type Node = (Formula, ([Atom], Model))
   update2 :: Node -> [Node]
   update2 = undefined

所以我的问题是如何创建一个heurestic并将其实现到update2函数中,该函数与更新函数的行为相同?

1 Answer

  • 1

    如果我正确理解了这个问题,那么您就会问如何在命题逻辑的解析系统中实现其他选择规则 . 据推测,你正在构建一个通过为文字指定真值而得到的公式树,直到(a)已经尝试了所有可能的文字赋值组合或(b)框(空子句)已经导出 .

    假设函数chooseAtom实现了一个选择规则,你可以通过给update添加一个额外的参数并用update替换update中的chooseAtom的出现来参数化任意选择规则r上的函数更新 . 由于chooseAtom实现了一个选择规则,因此将该选择规则传递给参数r会得到所需的结果 . 如果您提供chooseAtom的实现以及要替换它的函数,则可以更轻松地验证您的实现是否正确 .

    希望这很有帮助 . 然而,目前还不清楚究竟是在问什么 . 特别是,你要求的是一个“变量选择规则” . 但是,看起来你正在为命题逻辑实现一个解决方案系统 . 通常,选择规则和变量与谓词逻辑的分辨率相关联 .

Related