形式化正交重写系统的合流性

正交性是一种编程规范，它以语法方式保证函数规范的决定性。本质上，正交性一方面避免了非确定性的固有歧义，禁止存在指定相同函数且可能同时应用的不同规则（非歧义性），另一方面消除了这些规则左侧出现变量重复的可能性（左线性）。在项重写系统（TRS）理论中，决定性由众所周知的合流性性质捕获，该性质基本上表明，每当从一个项出发可能进行不同的计算或简化时，计算出的答案应该一致。尽管证明在技术上很复杂，但合流性众所周知是正交性的结果。因此，正交性是递归函数规范所固有的重要数学规范，自然应用于函数式编程和规范。从在证明助手PVS中形式化TRS理论开始，本文描述了如何基于对并行归约步骤中涉及的规则、位置和替换的性质的公理化，在PVS中形式化正交TRS的合流性。一些类似但受限的性质的证明，例如非歧义且（左和右）线性TRS的合流性，已被完全形式化。