相似签名上的项的格运算

合一与泛化是对两个项进行的操作，分别计算它们在由变量重命名下的子句序（即 $t_1\preceq t_2$ 当且仅当存在变量替换 $\sigma$ 使得 $t_1 = t_2\sigma$）准序下的最大下界和最小上界。当项的签名使得不同的函子符号可以与模糊等价（称为相似性）相关联时，这些操作可以形式化地扩展，以容忍函子名称和/或元数或参数顺序上的不匹配。我们采用声明式方法重新表述并扩展了先前的工作，将合一和泛化定义为构成完整约束规范化证明系统的公理和规则集。这些包括 Reynolds-Plotkin 项泛化过程、Maria Sessa 的具有部分模糊签名的“弱”合一及其相应的泛化，以及将这些操作扩展到完全模糊签名（即具有可能不同元数的相似函子）的新颖扩展。这种方法的一个优势是它不需要修改项和替换的传统数据结构。此外，这些声明式规范是高效可执行的条件 Horn 子句，为模糊信息处理应用提供了巨大的实用潜力。