模式匹配（例如，在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）时间。实际上，我假设他们已经为关联和交换等属性的操作进行了预编程优化。 –