sml의 논리 단순화

Question

sml에서 논리 단순화 프로그램을 만들고 있습니다. 하지만이 입력에 대한 문제가 있습니다.

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

그리고 무한 루프에 있습니다. X는 Y는 더 간단 할 수없는 경우

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

기본적으로, Simplify x 및 Simplify y가 반환합니다 정말 의심스러운 세 가지 경우가 있습니다

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

: 여기

내 코드입니다 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을 가졌으므로 외부 수준으로 전파하려는 것입니다. 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 :

난 당신이 정말없는 하향식 (top-down) 접근 방식을 사용하려고 생각 적당한. 내가 가지고있는 경우

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