http://swrc.ontoware.org/ontology#Article
Conjuring Fusion Laws via Relational Calculus
en
[通常論文] free theorem, conjuring lemma, function fusion, relational calculus
The University of Tokyo
Akimasa Morihata
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 ofInformation Processing(JIP). This preprint should not be cited. Thisarticle should be cited as: Journal of Information Processing Vol.31(2023) (online)------------------------------
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 ofInformation Processing(JIP). This preprint should not be cited. Thisarticle should be cited as: Journal of Information Processing Vol.31(2023) (online)------------------------------
AA11464814
情報処理学会論文誌プログラミング（PRO）
15
5
2022-12-15
1882-7802