偽りのない検索と照合

Question

組み込みロジックプログラミング言語を実装せずに、Haskellで存在論文を書くための拡張性のある効率的な方法がありますか？私はアルゴリズムを実装していたときに多くの場合、私は∈がリストにオーバーロードされ

∃x.∃y.x,y ∈ xs ∧ x ≠ y ∧ p x y 

のような存在量化一次ステートメントを表現したいです。私は急いでいる場合、私は

find p []  = False 
find p (x:xs) = any (\y -> x /= y && (p x y || p y x)) xs || find p xs 

または

find p xs = or [ x /= y && (p x y || p y x) | x <- xs, y <- xs] 

のように見えます。しかし、このアプローチは、複数のアリティの値または述語や関数を返すクエリにも一般化しない明快なコードを書くかもしれません。たとえば、簡単な文でさえ、

∃x.∃y.x,y,z ∈ xs ∧ x ≠ y ≠ z ∧ f x y z = g x y z 

のような別の検索手順を書く必要があります。そして、これは相当量の定型コードを意味します。検索の両方を実行し、値を返す、かなり記法を乱用する

find(p,xs,z) = x ∈ xs & y ∈ xs & x =/= y & f x y =:= g x y =:= z 

：もちろん、狭窄または解像度エンジンた器具Curry又はPrologような言語は、プログラマのような文を書くことを可能にします。この問題は、形式的に指定されたアルゴリズムを実装するときに頻繁に発生し、多くの場合、fmap,foldr、およびmapAccumなどの関数の組み合わせによって解決されますが、ほとんどは明示的な再帰です。 Haskellでもっと一般的で効率的な、あるいは一般的で表現力豊かなコードを書く方法はありますか？

Answer 1

あなたがあなたの代わりにexistsのfindを使用することができます証人を生成する必要がある場合は、

exists (\x -> P) xs 

に

∃x ∈ xs : P 

に変換することができ、標準の変換があります。

論理型言語とは対照的に、Haskellでは抽象化のこの種を行うことの本当の迷惑は、あなたが本当にが「宇宙」のパラメータとしてxsを設定するに合格しなければならないということです。私はこれが、あなたがあなたのタイトルで参照する "騒ぎ"をもたらすものだと信じています。

もちろん、あなたが望むのであれば、あなたが探しているユニバーサルセットをモナドに入れることができます。次に、自分のバージョンをexistsまたはfindと定義して、モナド状態で動作させることができます。効率を上げるには、Control.Monad.Logicを試すことができますが、これはOlegの論文に対してあなたの頭を壊すことを含むかもしれません。

とにかく、古典的なエンコーディングは、存在量と普遍的な量指定子を含むすべてのバインディング構造体をlambdasに置き換え、適切な関数呼び出しを続けることです。私の経験では、このエンコーディングは多くの構造を持つ複雑なネストされたクエリに対しても機能しますが、それは常に気難しいと感じています。

Answer 2

多分私は何かを理解していないかもしれませんが、リスト内包表記の何が間違っていますか？ 2番目の例は次のようになります。

[(x,y,z) | x <- xs, y <- xs, z <- xs 
, x /= y && y /= z && x /= z 
, (p1 x y z) == (p2 x y z)] 

これで値を返すことができます。式が満たされているかどうかを確認するには、nullを使用してください（怠惰のために必要以上に評価されません）。