Conjuring Fusion Laws via Relational Calculus

• Item type: Trans(1)
• 公開日: 2022-12-15
• タイトル: Conjuring Fusion Laws via Relational Calculus
• タイトル / 言語: en
• タイトル: Conjuring Fusion Laws via Relational Calculus
• 言語: eng
• キーワード / 主題Scheme: Other
• キーワード / 主題: [通常論文] free theorem, conjuring lemma, function fusion, relational calculus
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: The University of Tokyo
• 著者所属(英): en
• 著者所属(英): The University of Tokyo
• 著者名: Akimasa, Morihata
• 著者名(英): Akimasa, Morihata
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: Wadler demonstrated that several laws, called “free theorems”, about polymorphic functions can be derived from their types alone. Free theorems form the foundations of many program transformations, including function fusions particularly. Walder's approach requires systematic but cumbersome reasoning, which makes it difficult for non-experts to apply. To alleviate this problem, Voigtländer proposed a conjuring lemma. This lemma derives free theorems from an expression containing polymorphic functions but whose type does not contain polymorphic type variables. Unfortunately, it cannot derive function fusion laws. In this work, we generalize the conjuring lemma on the basis of Bird and de Moor's relational calculus. This calculus uses non-deterministic computations for uniformly describing and thereby relating specifications and implementations. To make the generalized conjuring lemma easier to use, we develop simpler corollaries by borrowing intuitions from the worker/wrapper transformations. The effectiveness of our approach is demonstrated through experiments with the derivation of three well-known fusion laws. While the original conjuring lemma cannot derive any of them, the generalization can systematically derive all.; ------------------------------; This is a preprint of an article intended for publication Journal of; Information Processing(JIP). This preprint should not be cited. This; article should be cited as: Journal of Information Processing Vol.31(2023) (online); ------------------------------
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Wadler demonstrated that several laws, called “free theorems”, about polymorphic functions can be derived from their types alone. Free theorems form the foundations of many program transformations, including function fusions particularly. Walder's approach requires systematic but cumbersome reasoning, which makes it difficult for non-experts to apply. To alleviate this problem, Voigtländer proposed a conjuring lemma. This lemma derives free theorems from an expression containing polymorphic functions but whose type does not contain polymorphic type variables. Unfortunately, it cannot derive function fusion laws. In this work, we generalize the conjuring lemma on the basis of Bird and de Moor's relational calculus. This calculus uses non-deterministic computations for uniformly describing and thereby relating specifications and implementations. To make the generalized conjuring lemma easier to use, we develop simpler corollaries by borrowing intuitions from the worker/wrapper transformations. The effectiveness of our approach is demonstrated through experiments with the derivation of three well-known fusion laws. While the original conjuring lemma cannot derive any of them, the generalization can systematically derive all.; ------------------------------; This is a preprint of an article intended for publication Journal of; Information Processing(JIP). This preprint should not be cited. This; article should be cited as: Journal of Information Processing Vol.31(2023) (online); ------------------------------
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 15, 号 5, 発行日 2022-12-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会