recursion - 在SML中递归二元决策图

在我上大学的一门课中，我们正在通过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);

最佳答案

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

涉及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模式可以更轻松地整体引用参数。）

其余两个案件留作练习。

关于recursion - 在SML中递归二元决策图，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/35164602/