パターンマッチング（たとえば、Prolog、MLファミリー言語、およびさまざまなエキスパートシステムシェルに見られる）は、通常、厳密な順序で要素ごとにクエリをデータと照合することによって機能します。
ただし、自動定理証明のようなドメインでは、一部の演算子が結合法則と可換性であることを考慮する必要があります。データがあるとします
A or B or C
とクエリ
C or $X
表面構文で見ると、これは一致しませんが、論理的には結合法則であるため、$Xバインドされたものと一致する必要があります。A or Bor
この種のことを行う既存のシステムは、どの言語でもありますか？
連想可換パターン マッチングは1981 年以前から存在しており、今日でも話題になっています。
このアイデアを実装して便利にするシステムはたくさんあります。これは、結合性または可換性を使用してパターン マッチを作成できる場合に、複雑なパターン マッチを記述することを回避できることを意味します。はい、高価になる可能性があります。パターンマッチャーがこれを自動的に行う方が、手動で行うよりも優れています。
プログラム変換システムを使用して実装された代数と単純な微積分の書き換えシステムの例を見ることができます。この例では、処理される記号言語が文法規則によって定義され、AC プロパティを持つ規則がマークされます。シンボリック言語の解析によって生成されたツリーの書き換えは、一致するように自動的に拡張されます。
私はそのようなことに遭遇したことがなく、より詳細に見ただけです。
これをデフォルトで実装しないのには、計算上の正当な理由があります。つまり、パターン マッチングの前に入力のすべての組み合わせを本質的に生成する必要があるか、一致句のクロス積に相当する完全な値を生成する必要があります。
これを実装する通常の方法は、単純に両方のパターン (バイナリの場合) を記述すること、つまり と の両方のパターンを持つことだと思いC or $Xます$X or C。
基礎となるデータの編成 (通常はタプル) によっては、このパターン マッチングにはタプル要素の順序の再配置が含まれますが、これは奇妙です (特に強く型付けされた環境では!)。それが代わりにリストである場合、あなたはさらに不安定な立場にいます.
ちなみに、あなたが基本的に望んでいる操作は、セットの素結合パターンであると思われます。たとえば、次のようになります。
foo (Or ({C} disjointUnion {X})) = ...
セットを詳細に扱う唯一のプログラミング環境は、Isabelle/HOL であり、それらに対してパターン マッチを構築できるかどうかはまだわかりません。
編集: Isabelle のfunction機能 (ではなくfun) を使用すると、複雑な非コンストラクター パターンを定義できるようになりますが、それらが一貫して使用されていることを証明する必要があり、コード ジェネレーターを使用できなくなります。
EDIT 2:n交換、連想、および推移的な演算子に対して同様の機能を実装する方法は次のとおりです。
私の用語は の形式でしたが、A | B | C | Dクエリは の形式B | C | $Xで、$Xは 0 個以上のものに一致することが許可されていました。変数が常に最後の位置に発生するように、辞書順を使用してこれらを事前に並べ替えました。
最初に、すべての対ごとの一致を構築し、ここでは変数を無視し、規則に従って一致するものを記録します。
{ (B,B), (C,C) }
これを 2 部グラフとして扱うと、本質的に完全結婚問題を実行していることになります。これらを見つけるための高速アルゴリズムが存在します。
1 つ見つかったと仮定すると、リレーションの左側 (この例ではAand D) に表示されないすべてのものを集め、それらを変数 に詰め込む$Xと、一致が完了します。明らかに、ここではどの段階でも失敗する可能性がありますが、これはほとんどの場合、RHS に解放された変数がない場合、または LHS に何にも一致しないコンストラクターが存在する場合に発生します (完全な一致を見つけることができません)。
これが少し混乱している場合は申し訳ありません。このコードを書いてからしばらく経ちましたが、少しでもお役に立てば幸いです!
記録として、これはすべての場合に適した方法ではない可能性があります。サブタームの「一致」について非常に複雑な概念 (つまり、単純な等式ではない) を持っていたので、セットの構築などは機能しませんでした。あなたのケースではうまくいくかもしれませんが、互いに素な結合を直接計算することができます。