重写计算：基础与应用

本论文致力于研究一种描述条件重写规则及其结果在同一表示层次上的计算。我们引入了重写计算（亦称 rho 计算），它概括了一阶项重写与 lambda 计算，并能够表示非确定性。在我们的方法中，抽象运算符和应用运算符都是计算的对象。重写计算的化简结果要么是表示应用失败的空集，要么是表示确定性结果的单元素集，要么是表示非确定性选择结果的集合。本论文聚焦于使用语法匹配以将变量绑定到其当前值的值域的重写计算属性。我们定义了确保计算保序性的评估策略，并展示这些策略在限制为更简单计算（如 lambda 计算）的通用重写计算 Restrictions 时变得平凡。未加限制的重写计算在无类型情况下不具终止性，但为 simply typed 计算可获得强归约性。在引入允许测试应用失败的运算符的重写计算中，我们定义表示相对于一组重写规则的内点范性和外点范性的项。通过这些项，我们获得了条件重写的自然简洁描述。最终，从条件重写规则的表示出发，我们展示了如何使用重写计算为 ELAN 语言（该语言基于由策略控制的重写规则应用）提供语义。