9

述語ロジックの式を表す標準データ型があります。論理和の自然演繹消去規則を表す関数は、次のようになります。

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

4

1 に答える 1

1

これは等式制約を使用する最良の方法ではないようです。a =:= b失敗すると、完全な関数句も失敗します。
例えば：

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

関数の最初の句が完全に終了するため、評価xx 7の結果は3(not 7)になります。7 =:= 5xx

コードは次のようになると思います。

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-03T10:13:35.143 に答える