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