模式匹配（例如，在Prolog，ML族語言和各種專家系統shell中找到）通常通過按嚴格順序將查詢與數據元素按元素進行匹配來操作。與關聯運算符和交換運算符匹配的模式
然而，在像自動定理證明這樣的領域中，要求考慮到一些操作符是關聯和交換的。假設我們有數據
A or B or C
和查詢
C or $X
通過表面的語法，這並不符合去，但在邏輯上應該與$X勢必A or B匹配，因爲or是聯想和交換。
是否有任何現有的系統，在任何語言，做這種事情？
聯合交換模式匹配自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 ，而且我仍然不確定是否可以在它們上面構建模式匹配。
編輯：它看起來像伊莎貝爾的function功能（而不是fun）將讓你定義複雜的非構造模式，除了那麼你必須證明他們一貫使用，並且不能再使用的代碼生成器。
編輯2：我實現了類似的功能在n交換，關聯和傳遞的運營方式是這樣的：
我的詞條形式A | B | C | D的，而查詢是形式B | C | $X，其中$X被允許匹配零或更多的東西。我使用詞法排序對這些進行了預先排序，這樣變量總是出現在最後一個位置。
首先，您構建所有配對匹配，忽略現在的變量，並記錄根據您的規則匹配的匹配項。
{ (B,B), (C,C) }
如果你把它當作一個二分圖，那麼你基本上是做一個perfect marriage問題。有找到這些的快速算法。
假設你找到一個，那麼你收集起來，不上你的關係的左側出現的一切（在這個例子中，A和D），你把它們塞進變量$X，和你的對手是完成。顯然，在這裏的任何階段你都可能失敗，但是如果RHS上沒有任何變量，或者LHS上存在一個與任何東西沒有匹配的構造函數（阻止你找到完美匹配），這將主要發生。
對不起，如果這有點混亂。自從我寫這段代碼以來已經有一段時間了，但我希望這可以幫助你，即使有一點點！
有記錄，這個可能不是一個好方法在所有情況下。我在子項上有非常複雜的「匹配」概念（即不是簡單的相等），所以構建集合或任何東西都不起作用。也許這會適用於你的情況，你可以直接計算不相交的聯合。
我同意，到目前爲止，我如何實現這個想法是將基於元組的表示轉換爲集合表示，以便能夠合理有效地執行此類查詢。不過，我認爲這是值得檢查，看看是否有人已經先發明瞭這個特定的輪子。 – rwallace
我在模型檢查器中爲bigraphs實現了類似的東西。 bigraphs的並行組合是可交換的，所以我必須實現這個功能。我必須說，實施起來非常可怕。代碼是可用的，但我懷疑它不會有幫助，因爲它與其他bigraph匹配代碼非常緊密，並且不太可能有用的可重用。我會編輯我的答案，以描繪我實施它的方式。 – Gian
謝謝！ Upvoted;我不知道downvote是從哪裏來的。 – rwallace
我不知道我與你的Prolog的模式匹配與ML模式匹配混爲一談同意。 ML模式匹配純粹是句法，在Prolog中，我不相信這是事實。 – Gian
我不是說他們是一樣的東西，只是他們有共同的元素比較嚴格的順序。 – rwallace
我假設像Otter這樣的專門的定理證明軟件已經這樣做了，將邏輯公式放在一個正常的形式中，並將這些子句作爲集合數據結構來處理，這會使創建和驗證花費O（n log n）時間。實際上，我假設他們已經爲關聯和交換等屬性的操作進行了預編程優化。 –