2

我正在用 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);
4

1 回答 1

3

真正可疑的有以下三种情况：

| 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返回xand y。因此，您将使用与之前相同的输入（Or(x, y)或And(x, y)）调用 Simplify Not x。您可以通过一些示例来测试您的函数是否不会终止，例如：And(And(Var "x", Var "y"), Var "z")和Not(And(Var "x", Var "y").

简化的想法是你有一个True或False在一个内部子句中，你想将它传播到外部级别。请注意，如果 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')))
于 2011-12-02T20:37:28.477 回答