SML 中的递归二元决策图

Question

在我的类大学中，我们正在通过 SML/NJ 学习函数式编程。

我接到了一项任务，要求我们对二元决策图执行一些操作。（连词、析取、非等）

基于这个道理table

我定义了以下函数

fun IfThenElse(p,q,r) = 
  if p then q else r;

然后，我们声明了 BDD (ROBDD) 数据类型

datatype ROBDD = true
               | false
               | IfThenElse of string * ROBDD * ROBDD;

到目前为止，这一切都相当简单。我在实际操作 BDD 时迷失了方向，例如，创建一个代表两个 ROBDD 的结合的 ROBDD。

到目前为止，我的函数声明如下所示

infix bddAnd;
fun op bddAnd(first:ROBDD,second:ROBDD) = 
   ...

它将用两个 ROBDD 调用，类似这样

val conjunction = IfThenElse("p", true, false) bddAnd IfThenElse("q", true, false);

从这里开始，我不太确定从哪里开始。我的教授给了我们这个提示：

Of course, True bddAnd anyROBDD will be just anyROBDD. To get the ordering: If you’re asked to compute (IfThenElse(p, ϕ, ψ) bddAnd IfThenElse(q, χ, θ)) the proposition letter at the root of the resultant ROBDD will be either p or q – whichever is less. So you’ll need 3 cases: p < q, p = q, and p > q. Having determined the root, you recurse down the branches

第一部分说得有道理，但我还有两个问题。

1.我如何确定任何 ROBDD 的根？

如果只是true或false，它没有，对吧？所以应该有一个特殊情况只给一个布尔值？如果给我们一个更充实的 ROBDD，比如 IfThenElse("p", true, false)，我如何在 ROBDD 结构中访问 p？请注意，IfThenElse 的第一个参数始终是字母。

2。我如何通过 ROBDD 进行递归？

我了解 SML 中递归函数的基础知识，但与列表相比，我对如何在 ROBDD 结构中执行它感到困惑。我猜我需要构建某种柯里化函数来对 ROBDD 中的每个参数进行操作，但我真的不确定如何构造它。

很抱歉这个冗长的问题，但我真的很难理解如何在 ROBDD 结构上操作。任何解释都会很有帮助，谢谢！

编辑：

经过一些语法和重命名后，我的 bddAnd 函数现在看起来像这样

infix bddAnd;
fun op bddAnd (true, second) = second
  | op bddAnd (first, true) = first
  | op bddAnd (false, _) = false
  | op bddAnd (_, false) = false
  | op bddAnd ((left as (IfThenElse (prop1, true1, else1))), (right as (IfThenElse (prop2, true2, else2)))) = 
        if prop1 < prop2 then 
          IfThenElse (prop1, true1 bddAnd right, else1 bddAnd right)
        else if prop1 > prop2 then
          IfThenElse (prop2, true2 bddAnd left, else2 bddAnd left)
        else
          IfThenElse (prop1, true1 bddAnd right, else1 bddAnd left);

Answer 1

模式匹配通常是一个很好的起点。

涉及True和False的案例很简单：

fun op bddAnd (True, second) = second
     | bddAnd (first, True) = first
     | bddAnd (False, _) = False
     | bddAnd (_, False) = False

最后一个比较有意思：

 | bddAnd (IfThenElse (v1, t1, e1)) (IfThenElse (v2, t2, e2)) = ... what? ...

正如您的教授所暗示的，您需要考虑 v1 和 v2 的三种情况：

if v1 < v2 then ...
else if v1 > v2 then ...
else ...

查看第一个 v1 < v2，我们应该选择 v1 作为 "root"。

说服自己并不难

(IfThenElse p T1 E1) bddAnd (IfThenElse q T2 E2)

相当于

IfThenElse p (T1 bddAnd (IfThenElse q T2 E2)) (E1 bddAnd (IfThenElse q T2 E2))

也就是说，您通过递归到您选择的 IfThenElse 的两个分支，将另一棵树带入，从两个创建一个 "tree"。
递归将终止，因为 bddAnd 应用于越来越小的参数，并且只要输入已排序（我假设我们被允许假设），结果就会被排序。

匹配上面的代码，

 | bddAnd (left as (IfThenElse (v1, t1, e1))) (right as (IfThenElse (v2, t2, e2))) = 
        if v1 < v2 then IfThenElse (v1, t1 bddAnd right, e1 bddAnd right)
        else ...

（使用 as 模式更容易整体引用参数。）

剩下的两个案例留作练习。

SML 中的递归二元决策图

Recursing Binary Decision Diagrams in SML

recursion

binary-tree

sml

smlnj