λ計算に基づいたC言語の等価性の導出

• Item type: Trans(1)
• 公開日: 1998-12-15
• タイトル: λ計算に基づいたC言語の等価性の導出
• タイトル / 言語: en
• タイトル: A Method to Derive Equivalence among C Programs Using a Lambda Calculus Representation
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 発表概要
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 電子技術総合研究所情報アーキテクチャ部
• 著者所属(英): en
• 著者所属(英): Computer Science Division, Electrotechnical Laboratory
• 著者名: 海老原, 一郎
• 著者名(英): Ichirou, Ebihara
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: C言語をλ計算に基づいた表現に変換した後でλ計算としての等価性を導出することにより C言語のソースプログラム間での等価性を導出する方法について考察した.本論文での導出方法は 等価性の導出の際にλ計算の構文的等価性以外にも公理的意味論に基づいた論理条件を自由に加えることを可能とすることにより 数論や線形代数などの公理から導かれるより高次の概念に基づいたプログラム間の等価性についても容易に記述して導出できる可能性を持つ.そのため 例えば数値計算ライブラリーと自作のプログラムとの等価性を導出するなどして ソースレベルでの大域的な最適化に役立つ可能性がある.
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: In this article a method which derives equivalence among C source programs based on a transformation from C source code into aλ-calculus representation is proposed. The method can treat any kind of equivalence in the form of logical formula in addition to syntactical equivalence ofλ-calculus, which makes it easy to control equivalence among C programs according to intuition of human beings. The method has a possibility to derive overall equivalence among C programs based on complex axioms of number theory, linear algebra and so on. In other words the method may become useful to overall optimization of C source programs, for example, using information about equivalence between an ad hoc handmade C program and a refined program of numerical computation from C libraries.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 39, 号 SIG01(PRO1), p. 84-84, 発行日 1998-12-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会