Total correctness by local improvement in the transformation of functional programs
Total correctness by local improvement in the transformation of functional programs
复制标题
通过功能程序转换的局部改进实现完全正确性
DOI：
10.1145/227699.227716
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
David Sands
中科院分区：
文献类型：
--
作者：
David Sands
程序转换的目标是在保留意义的同时提高效率。最著名的变换技术之一是Burstall和Darlington的展开方法。不幸的是，展开方法本身既不能保证效率的提高，也不能保证完全正确。展开-折叠的正确性问题是一个严格的更一般问题的实例：通过局部保持等价的步骤进行的变换不一定保持(全局)等价。本文给出了递归程序转换完全正确的一个条件，这是第一次处理包括惰性数据结构在内的高阶函数语言(包括严格和非严格的)。主要的技术结果是一个改进定理，该定理指出，如果局部转换步骤受到某些优化问题(转换的一个相当自然的条件)的指导，则转换的正确性随之而来。改进定理本质上使用了形式化的改进理论；作为一个相当令人愉快的推论，它还保证转换后的程序是对原始程序的形式改进。该定理具有直接的实际效果：它是证明高阶函数式程序现有转换方法的正确性的强大工具，而不必忽略诸如记忆或折叠等关键因素，并且它产生了一种简单的语法方法，用于在一般情况下指导和约束展开折叠方法，从而始终保证完全正确(和改进)。
The goal of program transformation is to improve efficiency while preserving meaning. One of the best-known transformation techniques is Burstall and Darlington's unfold-fold method. Unfortunately the unfold-fold method itself guarantees neither improvement in efficiency nor total correctness. The correctness problem for unfold-fold is an instance of a strictly more general problem: transformation by locally equivalence-preserving steps does not necessarily preserve (global) equivalence. This article presents a condition for the total correctness of transformations on recursive programs, which, for the first time, deals with higher-order functional languages (both strict and nonstrict) including lazy data structures. The main technical result is an improvement theorem which says that if the local transformation steps are guided by certain optimization concerns (a fairly natural condition for a transformation), then correctness of the transformation follows. The improvement theorem makes essential use of a formalized improvement theory; as a rather pleasing corollary it also guarantees that the transformed program is a formal improvement over the original. The theorem has immediate practical consequences: it is a powerful tool for proving the correctness of existing transformation methods for higher-order functional programs, without having to ignore crucial factors such as memoization or folding, and it yields a simple syntactic method for guiding and constraining the unfold-fold method in the general case so that total correctness (and improvement) is always guaranteed.