SML 中的递归二元决策图

Question

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

我被分配了一项任务，要求我们对二元决策图执行一些操作。 （合取、析取、非等）

基于这个真值表

我定义了以下函数

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);

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

当然，True bddAnd anyROBDD 将只是 anyROBDD。获得订单：如果你被要求计算 (IfThenElse(p, ϕ, ψ) bddAnd IfThenElse(q, χ, θ)) 结果 ROBDD 根部的命题字母将是 p 或 q——以较小者为准。所以你需要 3 个案例：p < q、p = q 和 p > q。确定了根之后，你就向下递归分支

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

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作为“根”。

说服自己并不难

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

等价于

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

也就是说，您可以通过递归到您选择的 IfThenElse 的两个分支中，从两个“树”中创建一个“树”，同时带上另一棵树。
递归将终止，因为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-patterns 更容易将参数作为整体引用。）

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