함수가 "없음"대신 "솔루션 없음"을 반환합니다

Question

나는 술어 논리의 수식을 나타내는 표준 데이터 형식을 사용합니다. 분리에 대한 자연 공제 제거 규칙을 나타내는 기능과 같습니다

d_el p q = 
    if p =: (Dis r s) && q =: (Neg r) then Just s else 
    if q =: (Dis r s) && p =: (Neg r) then Just s else 
    Nothing where r,s free 

x =: y = (x =:= y) == success 

대신에 통일이 실패하면 Nothing으로 평가, 기능이 PACKS에 어떤 솔루션을 반환 :

내가 놓친 게 무엇

logic> d_el (Dis Bot Top) (Not Bot) 
Result: Just Top 
More Solutions? [Y(es)/n(o)/a(ll)] n 
logic> d_el (Dis Bot Top) (Not Top) 
No more solutions. 

, 통합 실패시 el은 Nothing으로 평가되지 않는 이유는 무엇입니까?

Answer 1

등식 제약 조건을 사용하는 가장 좋은 방법은 아닌 것 같습니다. a =:= b이 실패하면 complete function 절도 실패합니다. 완전히 기능 xx 제 절 종료 3 (되지 7)에 7 =:= 5 때문에
예컨대 :

xx x = if (x =:= 5) == success then 1 else x 
xx x = 3 

평가 결과 xx 7.

나는 코드는 다음과 같이해야한다고 생각 :

이

d_el p q = case (p,q) of 
    (Dis a s, Neg b) -> if a == b then Just s else Nothing 
    (Neg a, Dis b s) -> if a == b then Just s else Nothing 
    _ -> Nothing