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。因此，您将使用与之前相同的输入（Or(x, y)，And(x, y)或Not x）调用Simplify。你可以测试你的函数没有终止一些例子，例如：And(And(Var "x", Var "y"), Var "z")和Not(And(Var "x", Var "y")。

简化的想法是，你有一个内部子句中的True或False，你想传播它到外层。请注意，如果x和y是不可约的，则不会尝试简化。

UPDATE：

你的函数可以被确定如下：

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