非述語的多相型付けを用いたプログラム融合変換

使用非谓词多态类型的程序融合转换

• 批准号: 17700012
• 负责人: 西村 進
• 金额: $ 1.6万
• 依托单位: Kyoto University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Young Scientists (B)
• 财政年份: 2005
• 资助国家: 日本
• 起止时间: 2005 至 2007
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-17700012/
• 关键词: プログラム変換; 関数融合; プログラム論理; 詳細化; 型; 論理

ヒープに割り当てられたデータ構造の書き換えを含むプログラムの変換方法についての研究を行った。このようなプログラムはポインタの操作を直接的に扱わなければならないが、ポインタ操作を含むプログラムの変換はそうでないものの変換よりも格段に難しく、その変換手法については系統的なものはあまり知られていなかった。本年度の研究では、形式的技法の分野で研究されてきているプログラムの詳細化の手法を、ポインタやヒープに関する性質を記述するための論理体系のひとつであるSeparation Logicで拡張した。これによって、プログラム中のポインタ操作がすべて、Separation Logicにおける中核的な2種類の論理演算と対応するふたつの一般化されたポインタ操作の組み合わせで表せることが明らかとなった。これら二つの操作に関する変換規則を整備して適用することにより、ポインタ操作を含むプログラムの系統的な変換手法への糸口を見出した。またこの内容を定理証明系の上で実装し、これを用いて正しさの保証されたポインタ操作を含むプログラムの変換を行うことができることを示した。これらの結果は、いくつかの国内の研究集会で発表され、また2008年7月にフランスで開催される国際会議Mathematics of Program Construction(MPC'08)でも発表予定である。また、勝股審也氏との共同研究による、モノイド準同型を用いた代数的手法に基づいた累積変数を持つ関数プログラムの融合変換手法についての共著論文が著名雑誌Journal of Functional Programmingに近日掲載されることが決定した。この論文は2006年に国際会議ICFP'06において発表したものを拡張しまとめたものである。

我们对如何转换程序进行了研究，包括重写分配给堆的数据结构。尽管此类程序必须直接处理指针操作，但是包含指针操作的程序的转换比转换要困难得多，尽管不是这种情况，但鲜为人知的是系统的方法。今年的研究扩展了详细的程序技术，该技术已在正式技术领域进行了研究，分离逻辑是描述指针和堆的属性的逻辑系统之一。这表明程序中的所有指针操作都可以通过在分离逻辑中的两个核心逻辑操作和两个相应的广义指针操作的组合来表达。通过准备和应用这两个操作转换规则，我们找到了用于包括指针操作的程序的系统转换方法的线索。还已经证明，该内容可以在定理证明系统上实现，并用于转换包括保证正确的指针操作的程序。这些结果将在几次国家研究会议上介绍，还将在2008年7月在法国举行的国际计划构建数学（MPC'08）上介绍。此外，还有一篇关于融合转换方法的共同作品的论文，该论文涉及与累积变量的融合转换方法，基于累积变量，基于使用MONOID SAGRISMISS的代数方法，已撰写的杂志，该法案已逐渐出现，该杂志已逐渐出现，该杂志已被刊登，该杂志已被刊登，该杂志已在该杂志上出版，该法案已在该杂志上出现，该法案已在杂志上出现，该法案已在该杂志上出版，该方法又是在逐渐出现的。与Katsumata Shinya合作的协作研究。本文是关于2006年国际会议ICFP'06国际会议上发布的内容的扩展摘要。

项目成果

Algebraic Fusion of Functions with an Accumulating Parameter and its Improvement

带累加参数函数的代数融合及其改进

• 发表时间: 2006
• 期刊: ICFP'06: Proceedings of the 11th ACMSIGPLAN International Conference on Functional Programming
• 作者: Shin-ya Katsumata;Susumu Nishimura
• 通讯作者: Susumu Nishimura