パターンマッチング（例：Prolog、MLファミリの言語およびさまざまなエキスパートシステムシェルで見られる）は、通常、厳密な順序でデータ要素とクエリを照合することによって動作します。連想演算子とパターンマッチング
しかし、自動定理証明のような分野では、いくつかの演算子が連想して可換であることを考慮する必要があります。私たちは、これが一致していませんが、or連想と可換であるため、論理的に、それはA or Bにバインド$Xと一致している必要があり、表面の構文で行くデータ
A or B or C
とクエリ
C or $X
があるとします。
このようなことを行う言語が存在するシステムはありますか？
アソシエイティブ - 相補的パターンマッチングは1981 and earlier以降であり、依然としてホットトピックtodayです。
このアイデアを実装して有用なシステムがたくさんあります。それはあなたが複雑なパターンマッチを書かないようにすることを意味します。アコスティティビティやコミュティティビリティを使ってパターンをマッチさせることができます。はい、それは高価かもしれません。パターンマッチャーが手作業で行うよりも、自動的にこれを行うほうが良いでしょう。
rewrite system for algebra and simple calculusの例は、プログラム変換システムを使用して実装できます。この例では、処理されるシンボリック言語は文法ルールによって定義され、A-Cプロパティを持つルールはマークされます。シンボリック言語の構文解析によって生成されたツリーのリライトは、自動的に一致するように拡張されます。
私はこのようなことに遭遇したことは一度もありません。
デフォルトでこれを実装しないという計算上の理由があります。パターンマッチングの前にすべての入力の組み合わせを生成するか、完全なクロス積価値の一致句を生成する必要があります。
これを実装する通常の方法は、両方のパターン（バイナリの場合）を書くこと、つまりC or $Xと$X or Cの両方のパターンを作成することだと思われます。
データの基盤となる組織（通常はタプル）に応じて、このパターンマッチングではタプル要素の順序を並べ替えることになります。それが代わりにリストであれば、あなたはより揺れ動く地にいます。ちなみに
は、私はあなたが基本的にしたい操作がセットにばらばら組合パターン、であることが疑われる例：
foo (Or ({C} disjointUnion {X})) = ...
任意の詳細セットを扱う私が見てきた唯一のプログラミング環境は以下のようになりイザベル/ HOL私はあなたがそれらの上にパターンマッチを構築することができるかどうかまだ分かりません。
編集：それはあなたが、彼らは一貫して使用されていることを証明する必要があり、その後除き、あなたは複雑な非コンストラクタパターンを定義できます（というfunより）イザベルさんfunction機能のように見える、とあなたはもうコードジェネレータを使用することはできません。
EDIT 2：クエリが一致するように許可された$X形態B | C | $Xのであった
私の用語は、フォームA | B | C | Dであった：私はn可換、連想と推移オペレータにわたって同様の機能を実現方法はこれでしたゼロ以上のもの。私はレオグラフィックの順序付けを使用してこれらをあらかじめソートしていたので、変数は常に最後の位置に発生していました。
まず、すべてのペアワイズマッチを作成し、今のところ変数を無視し、ルールに従ってマッチするものを記録します。
{ (B,B), (C,C) }
あなたは二部グラフとしてこれを扱う場合は、基本的にperfect marriage問題をやっています。これらを見つけるための高速アルゴリズムが存在する。あなたがものを見つけると仮定
は、あなたは（この例では、AとD）あなたの関係の左側に表示されないすべてのものを集めて、あなたは変数$Xにそれらを詰め込むと、あなたのマッチがありますコンプリート。明らかに、ここではどの段階でも失敗する可能性がありますが、RHSに変数がない場合や、LHS上にコンストラクタが存在する場合（ほとんどの場合、完璧な一致を見つけることができません）
これはちょっと混乱している場合は申し訳ありません。私はこのコードを書いてからしばらくしていますが、これがあなたを少しでも助けてくれることを願っています！
この場合、このはとなる可能性があります。私は、サブターム（つまり、単純な平等ではない）に「一致」するという非常に複雑な概念を持っていました。多分あなたのケースではうまくいくでしょうし、別々の組合を直接計算することもできます。
私はこれを実装する方法についてのこれまでの考え方は、このタイプのクエリを合理的に効率的に実行できるように、タプルベースの表現を前のセット表現に変換することです。私は誰もがこの特定の車輪を最初に発明したかどうかを確認する価値があると考えました。 – rwallace
私はbigraphsのためのモデルチェッカーで同様のものを実装しました。 bigraphsの並列構成は可換であるため、この機能を正確に実装する必要がありました。実装するのはほとんど恐ろしいことでしたが、私は言わなければなりません。コードは利用可能ですが、他のバイグラムマッチングコードと結びついており、有用に再利用できそうにないので、参考にならないと思われます。私はそれを実装した方法をスケッチするために私の答えを編集します。 – Gian
ありがとう！アップアップされた。私はdownvoteが誰から来たのか分からない。 – rwallace
maude用語リライタは、連想的および可換的パターンマッチングを実装します。
あなたはより具体的なリンクを与えることができますか？おそらくコード例で？ –
は私がMLのパターンマッチング対Prologのパターンマッチングのあなたの混同に同意するか分かりません。 MLパターンマッチングは純粋に構文的なものであり、Prologではこれが当てはまるとは思わない。 – Gian
私は彼らが同じものだと言っているわけではありません、彼らは厳密な順序で要素の比較を共通に持っているだけです。 – rwallace
私は、Otterのような専用の定理を証明するソフトウェアは、論理式を通常の形で配置し、そのデータ構造をO（n log n）時間の作成と検証に費やす設定データ構造として扱うことによって、実際に、私は連想性や可換性のようなプロパティの操作のための最適化を事前にプログラムしていると思います。 –