函數返回「無解」而不是「無」

我有一個標準的數據類型表示謂詞邏輯的公式。代表的脫節自然演繹排除規則的函數可能看起來像：函數返回「無解」而不是「無」

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？

來源

2011-09-30 danportin

我使用的語言是咖喱，功能性，邏輯編程的langauge（見標籤）。 – danportin

哦 - 對不起....無知可能會很尷尬...... – Carsten

正如你可能知道的，「咖喱」也是一個在其他語言中有意義的詞（比如Haskell），所以也許你應該[將一些內容添加到''curry'標籤的Stack Overflow wiki頁面（http://stackoverflow.com/edit-tag-wiki/45806）。 – MatrixFrog

看來這不是使用等式約束的最佳方式。當a =:= b失敗時，則完成功能子句也失敗。
例如爲：

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

評價xx 7導致3（未7），因爲7 =:= 5完全終止xx函數的第一條款。

我認爲代碼應該是這樣的：

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

來源

2011-12-03 10:13:35

函數返回「無解」而不是「無」

回答

相關問題