模式匹配（如在 Prolog、ML 系列语言和各种专家系统外壳中发现的）通常通过以严格的顺序逐个元素地匹配查询与数据来进行操作。
然而，在诸如自动定理证明之类的领域中，需要考虑一些运算符是关联的和可交换的。假设我们有数据
A or B or C
并查询
C or $X
按照表面语法，这不匹配，但从逻辑上讲，它应该与$Xbound to匹配，A or B因为or它具有关联性和可交换性。
有没有任何语言的现有系统可以做这种事情？
3 回答
6
关联交换模式匹配自1981 年及更早的时候就已经存在，并且在今天仍然是一个热门话题。
有很多系统实现了这个想法并使其有用。这意味着当可以使用关联性或交换性来进行模式匹配时，您可以避免编写复杂的模式匹配。是的，它可能很昂贵；模式匹配器自动执行此操作比您手动执行此操作要好。
您可以在使用我们的程序转换系统实现的代数和简单微积分重写系统中看到一个示例。在这个例子中，要处理的符号语言由语法规则定义，那些具有AC属性的规则被标记。通过解析符号语言产生的对树的重写会自动扩展为匹配。
于 2011-12-01T01:15:20.387 回答
5
maude 术语重写器实现了关联和交换模式匹配。
于 2012-12-02T19:38:12.663 回答
1
我从来没有遇到过这样的事情，我只是更详细地看了一下。
默认情况下不实现这一点有一个合理的计算原因 - 必须在模式匹配之前生成输入的所有组合，或者您必须生成匹配子句的完整叉积值。
我怀疑实现这一点的常用方法是简单地编写两种模式（在二进制情况下），即同时具有C or $X和的模式$X or C。
根据数据的底层组织（通常是元组），这种模式匹配将涉及重新排列元组元素的顺序，这会很奇怪（尤其是在强类型环境中！）。如果它是列表，那么你就更不稳定了。
顺便说一句，我怀疑您从根本上想要的操作是集合上的不相交联合模式，例如：
foo (Or ({C} disjointUnion {X})) = ...
我见过的唯一处理任何细节集的编程环境是 Isabelle/HOL，我仍然不确定您是否可以在它们之上构造模式匹配。
编辑：看起来 Isabelle 的function功能（而不是fun）将允许您定义复杂的非构造函数模式，除非您必须证明它们的使用一致，并且您不能再使用代码生成器。
n编辑 2：我在可交换、关联和传递运算符上实现类似功能的方式是：
我的条件是形式的A | B | C | D，而查询是形式的B | C | $X，$X允许匹配零个或多个事物。我使用 lexographic ordering 对它们进行了预排序，因此变量总是出现在最后一个位置。
首先，您构建所有成对匹配，暂时忽略变量，并根据您的规则记录匹配的那些。
{ (B,B), (C,C) }
如果你把它当作一个二分图，那么你基本上是在做一个完美的婚姻问题。存在用于找到这些的快速算法。
假设你找到了一个，然后你收集所有没有出现在你的关系左侧的东西（在这个例子中，A和D），你把它们塞进变量$X中，你的匹配就完成了。显然，您可以在此处的任何阶段失败，但是如果 RHS 上没有可用的变量，或者 LHS 上存在与任何东西都不匹配的构造函数（阻止您找到完美匹配），这通常会发生。
对不起，如果这有点混乱。我写这段代码已经有一段时间了，但我希望这对你有所帮助，哪怕是一点点！
郑重声明，这可能不是在所有情况下的好方法。我对子术语的“匹配”有非常复杂的概念（即，不是简单的相等），因此构建集合或任何东西都行不通。也许这对你的情况有用，你可以直接计算不相交的联合。
于 2011-12-01T00:57:46.057 回答