首页> 外文期刊>Mathematical structures in computer science >On proving the correctness of program transformations based on free theorems for higher-order polymorphic calculi
【24h】

On proving the correctness of program transformations based on free theorems for higher-order polymorphic calculi

机译:基于自由定理证明高阶多态结石程序变换的正确性

获取原文
获取原文并翻译 | 示例

摘要

A number of program transformations currently of interest can be derived from Wadler's 'free theorems' for calculi approximating modern functional languages. Although delicate but fundamental issues arise in proving the correctness of free theorems-based program transformations, these issues have usually been left unaddressed in the correctness proofs appearing in the literature. As a result, most such proofs are incomplete, and most free theorems-based transformations are applied to programs in calculi for which they are not actually known to be correct.The purpose of this paper is three-fold. First, we raise and clarify some of the issues that must be addressed when constructing correctness proofs for free theorems-based program transformations. Second, we offer a principled approach to developing such proofs. Third, we use Pitts' recent work on parametricity and observational equivalence to show how our approach can be used to give the first proof that transformations based on the Acid Rain theorems preserve observational equivalence of programs in a polymorphic lambda calculus supporting FPC-style fixpoints and algebraic data types. Correctness of the foldr-build rule, the destroy-unfoldr rule, and the hylofusion program transformation for this calculus follows immediately. The same approach is expected to yield complete correctness proofs for free theorems-based transform at ions in calculi that even more closely resemble languages with which programmers are concerned in practice.
机译:当前感兴趣的许多程序转换都可以从Wadler的“自由定理”中推导出,以近似计算现代功能语言。尽管在证明基于自由定理的程序转换的正确性时出现了微妙但基本的问题,但是这些问题通常在文献中出现的正确性证明中没有得到解决。结果,大多数这样的证明都是不完整的,并且大多数基于定理的自由变换都被应用到计算程序中,而对于这些程序而言,实际上并不知道它们是正确的。本文的目的是三方面的。首先,我们提出并阐明了为基于自由定理的程序转换构造正确性证明时必须解决的一些问题。其次,我们提供了开发此类证明的原则方法。第三,我们使用Pitts最近在参量和观测等效性方面的工作来展示我们的方法如何可以用来提供第一个证明,即基于酸雨定理的变换在支持FPC样式固定点的多态Lambda微积分中保留了程序的观测等效性。代数数据类型。随之而来的是fold-build规则,destroy-unfoldr规则以及此程序的hylofusion程序转换的正确性。预计将使用相同的方法为基于自由定理的演算中的离子生成完全正确的证明,该演算与程序员在实践中所关注的语言更加相似。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号