非二元函数的关联、交换性质和单位元

Question

我正在制作一个编译器（用于一种新语言），它通过模式匹配支持 AC 统一。 匹配算法已经有效，但是我在函数的逻辑和数学方面以及它的属性方面遇到了麻烦，这将以很好的方式定义语言的设计。我有几个关于函数属性的问题：

关联和交换属性仅适用于二元函数？

例如，如果我声明一个函数 max(a,b)，这将是可交换的，因为 max(a,b) = max(b,a) 并且是关联的，因为 max(a,max(b,c)) = max(max(a,b), c)，但我想不出任何具有两个以上参数的函数都满足这个公理。例如，我可以定义 max(a,b,c) = max(a,max(b,c)) 这将是一个三元函数，但该语言将能够将它与符合它的二元运算统一起来。

统一的工作原理是将诸如 max(a,max(b,c)) 之类的关联函数简化为可变和规范形式 max(a,b,c)，然后在此规范形式上执行模式匹配，所以所有（我认为）具有此属性且参数超过 3 个的可能函数实际上是同一个二元函数的组合

标识元素是否仅适用于二元函数？

说明： 可以有一个可变函数 f(a,b,...)（超过 2 个参数），使得存在满足 f(a,b,c,e) = f(a,b,c) 的元素 e没有直接二进制父级的函数（例如加法是二进制但编译器将加法管理为内部表示的可变函数）

在语言中仅通过删除其在函数上的 aparences 来管理诸如零之类的 Unitiy 元素，例如 add(1,2,x,0) ，它表示表达式 1+2+x+0 简化为 1+2 +x

这些问题对于在定义规则（例如 a+b = b+a）时自动识别函数属性的算法设计以及语言设计和对函数声明施加的约束具有决定性意义，这如果这些问题中的任何一个为假，则可能是不合逻辑的

Answer 1

查看 AC 和可变函数的一种方法是查看列表、袋子和集合的 cons 函数：

 cons(a, cons(b, nil)) // depicts a binary tree, a list or a set?

• 如果cons 没有公理，则它是二叉树
• 如果 cons 是关联的、不可交换的且非幂等的，则它是一个列表。
• 如果 cons 是关联和可交换的，那么它就是一个包
• 如果 cons 是关联的、交换的和幂等的，那么它就是一个集合。

现在，可变参数函数就像cons 的更好表示法：

• set(1,2,3,4) 是 cons 的“更好的符号”，即 ACI。
• list(1,2,3,4,1,2,3,4)为A
• bag(1,1,2,2,3,3,4,4) 交流电

诸如 ELAN、Maude、Tom、ASF+SDF 等支持某种“匹配模”的系统在底层使用了这种同余性：它们将具有理论的二元运算符映射到内部数据结构，例如列表、集合、通过扁平化递归应用程序、排序和消除重复项等来打包。