sml 中的逻辑简化

Question

我正在 sml 中创建逻辑简化程序。但我对此输入有一个问题：

- Or(Or(Var"x", Var"y"), Var"z");
val it = Or (Or (Var #,Var #),Var "z") : formula
 - Simplify it;

它处于无限循环中。

这是我的代码：

fun Simplify (Or(True, _)) = True
| Simplify (Or(_, True)) = True
| Simplify (Or(False, False)) = False
| Simplify (Or(x, False)) = (Simplify x)
| Simplify (Or(False, x)) = (Simplify x)
| Simplify (Or (Var (x), Var (y))) = Or (Var (x), Var (y))
| Simplify (Or (x, y)) = (Simplify (Or (Simplify x, Simplify y)))

| Simplify (And(_, False)) = False
| Simplify (And(False, _)) = False
| Simplify (And(True, True)) = True
| Simplify (And(True, x)) = (Simplify x)
| Simplify (And(x, True)) = (Simplify x)
| Simplify (And(Var (x), Var(y))) = And (Var (x), Var (y))
| Simplify (And (x, y)) = (Simplify (And (Simplify x, Simplify y)))

| Simplify (Not(Not(x))) = (Simplify x)
| Simplify (Not(True)) = False
| Simplify (Not(False)) = True
| Simplify (Not(Var (x))) = (Not (Var x))
| Simplify (Not(x)) = (Simplify (Not (Simplify x)))

| Simplify True = True
| Simplify False = False
| Simplify (Var(x)) = Var(x);

Answer 1

有三种情况确实很可疑：

| Simplify (Or (x, y)) = (Simplify (Or (Simplify x, Simplify y)))

| Simplify (And (x, y)) = (Simplify (And (Simplify x, Simplify y)))

| Simplify (Not(x)) = (Simplify (Not (Simplify x)))

基本上，如果 x 和 y 无法进一步简化，Simplify x 和 Simplify y 将返回 x > 和y。因此，您将使用与之前相同的输入调用 Simplify（Or(x, y)、And(x, y) 或 Not x） 。您可以使用一些示例来测试您的函数是否不会终止，例如： And(And(Var "x", Var "y"), Var "z") 和 Not(And (Var "x", Var "y")

简化的想法是，您希望在内部子句中传播 True 或 False。请注意，您不会尝试简化 if x 和y 是不可约的。

更新：

您的函数可以按如下方式修复：

fun Simplify (Or(True, _)) = True
    | ... (* Keep other cases as before *)
    | Simplify (Or (x, y)) = (case Simplify x of
                                True => True
                              | False => Simplify y
                              | x' => (case Simplify y of
                                         True => True
                                       | False => x'
                                       | y' => Or(x', y')))

    | Simplify (And (x, y)) = (case Simplify x of
                                 False => False
                               | True => Simplify y
                               | x' => (case Simplify y of
                                          False => False
                                        | True => x'
                                        | y' => And(x', y')))
    | Simplify (Not x) = case Simplify x of
                             True => False
                           | False => True
                           | x' => Not x'

更新 2：

我认为您尝试使用自上而下的方法，这并不适合我重写。函数使用自下而上的方法使其更短且更具可读性：

fun Simplify True = True
 | Simplify False = False
 | Simplify (Var x) = Var x
 | Simplify (Not x) = (case Simplify x of
                         True => False
                       | False => True
                       | x' => Not x')
 | Simplify (And(x, y)) = (case Simplify x of
                             False => False
                           | True => Simplify y
                           | x' => (case Simplify y of
                                      False => False
                                    | True => x'
                                    | y' => And(x', y')))
 | Simplify (Or(x, y)) = (case Simplify x of
                            True => True
                          | False => Simplify y
                          | x' => (case Simplify y of
                                     True => True
                                   | False => x'
                                   | y' => Or(x', y')))