{"links":{},"metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00222857","sets":["934:935:10774:11068"]},"path":["11068"],"owner":"44499","recid":"222857","title":["Conjuring Fusion Laws via Relational Calculus"],"pubdate":{"attribute_name":"公開日","attribute_value":"2022-12-15"},"_buckets":{"deposit":"7cfa1a7d-3e3c-440b-a370-dbd99115f664"},"_deposit":{"id":"222857","pid":{"type":"depid","value":"222857","revision_id":0},"owners":[44499],"status":"published","created_by":44499},"item_title":"Conjuring Fusion Laws via Relational Calculus","author_link":["585285","585284"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"Conjuring Fusion Laws via Relational Calculus"},{"subitem_title":"Conjuring Fusion Laws via Relational Calculus","subitem_title_language":"en"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"[通常論文] free theorem, conjuring lemma, function fusion, relational calculus","subitem_subject_scheme":"Other"}]},"item_type_id":"3","publish_date":"2022-12-15","item_3_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"The University of Tokyo"}]},"item_3_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"The University of Tokyo","subitem_text_language":"en"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"eng"}]},"item_publisher":{"attribute_name":"出版者","attribute_value_mlt":[{"subitem_publisher":"情報処理学会","subitem_publisher_language":"ja"}]},"publish_status":"0","weko_shared_id":-1,"item_file_price":{"attribute_name":"Billing file","attribute_type":"file","attribute_value_mlt":[{"url":{"url":"https://ipsj.ixsq.nii.ac.jp/record/222857/files/IPSJ-TPRO1505002.pdf","label":"IPSJ-TPRO1505002.pdf"},"date":[{"dateType":"Available","dateValue":"2024-12-15"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-TPRO1505002.pdf","filesize":[{"value":"208.6 kB"}],"mimetype":"application/pdf","priceinfo":[{"tax":["include_tax"],"price":"0","billingrole":"5"},{"tax":["include_tax"],"price":"0","billingrole":"6"},{"tax":["include_tax"],"price":"0","billingrole":"15"},{"tax":["include_tax"],"price":"0","billingrole":"44"}],"accessrole":"open_date","version_id":"e7e35881-bb70-4296-87e6-b4acbaebeef0","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2022 by the Information Processing Society of Japan"}]},"item_3_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Akimasa, Morihata"}],"nameIdentifiers":[{}]}]},"item_3_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Akimasa, Morihata","creatorNameLang":"en"}],"nameIdentifiers":[{}]}]},"item_3_source_id_9":{"attribute_name":"書誌レコードID","attribute_value_mlt":[{"subitem_source_identifier":"AA11464814","subitem_source_identifier_type":"NCID"}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourceuri":"http://purl.org/coar/resource_type/c_6501","resourcetype":"journal article"}]},"item_3_source_id_11":{"attribute_name":"ISSN","attribute_value_mlt":[{"subitem_source_identifier":"1882-7802","subitem_source_identifier_type":"ISSN"}]},"item_3_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"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.\n------------------------------\nThis is a preprint of an article intended for publication Journal of\nInformation Processing(JIP). This preprint should not be cited. This\narticle should be cited as: Journal of Information Processing Vol.31(2023) (online)\n------------------------------","subitem_description_type":"Other"}]},"item_3_description_8":{"attribute_name":"論文抄録(英)","attribute_value_mlt":[{"subitem_description":"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.\n------------------------------\nThis is a preprint of an article intended for publication Journal of\nInformation Processing(JIP). This preprint should not be cited. This\narticle should be cited as: Journal of Information Processing Vol.31(2023) (online)\n------------------------------","subitem_description_type":"Other"}]},"item_3_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographic_titles":[{"bibliographic_title":"情報処理学会論文誌プログラミング（PRO）"}],"bibliographicIssueDates":{"bibliographicIssueDate":"2022-12-15","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"5","bibliographicVolumeNumber":"15"}]},"relation_version_is_last":true,"weko_creator_id":"44499"},"created":"2025-01-19T01:22:47.561378+00:00","updated":"2025-01-19T13:35:56.843859+00:00","id":222857}