rwa*_*ace 6 language-agnostic pattern-matching theorem-proving
模式匹配(例如在Prolog,ML系列语言和各种专家系统shell中找到)通常通过严格按顺序将元素的查询与数据匹配来进行操作.
然而,在诸如自动化定理证明之类的领域中,需要考虑到一些运算符是关联的和可交换的.假设我们有数据
A or B or C
和查询
C or $X
通过表面语法,这不匹配,但逻辑上它应该与$X绑定匹配,A or B因为or是关联和可交换的.
是否有任何语言的现有系统可以做这种事情？
联想对易模式匹配已经出现了自1981年及更早版本,并且仍然是一个热门话题的今天.
有很多系统可以实现这个想法并使其有用; 这意味着当关联性或可交换性可用于使模式匹配时,您可以避免编写复杂的模式匹配.是的,它可能很贵; 更好的模式匹配器会自动执行此操作,而不是手动操作.
您可以在重写系统中查看使用我们的程序转换系统实现的代数和简单微积分的示例.在此示例中,要处理的符号语言由语法规则定义,并且标记具有AC属性的那些规则.通过解析符号语言生成的树上的重写将自动扩展为匹配.