通过统一和临界对计算实现程序变换的正确性
摘要：扩展的lambda演算具有上下文语义，程序转换的正确性通常基于对重写语义的推理。一种成功的证明正确性的方法是将上下文引理与程序转换与规约规则之间的重叠计算相结合，然后再进行所谓的完备的图集的计算。该方法类似于推理系统的补全时计算临界对。我们探索了那些可以通过使用统一算法的临界对计算的一阶方式的情况。作为一个案例研究，我们将该方法应用于具有递归let表达式的lambda演算，并描述了一种有效的统一算法来确定一组转换与所有规约规则的重叠。统一算法采用多排序术语，模拟多重集的左可交换性的等式理论，不同种类的上下文变量以及一种紧凑地表示递归let表达式中绑定链的机制。
作者：Conrad Rau, Manfred Schmidt-Schau{ss}
论文ID：1012.4893
分类：Programming Languages
分类简称：cs.PL
提交时间：2010-12-23