関数型プログラムから論理制約付き条件付き項書き換えシステムへの変換

• Item type: Trans(1)
• 公開日: 2023-06-29
• タイトル: 関数型プログラムから論理制約付き条件付き項書き換えシステムへの変換
• タイトル / 言語: en
• タイトル: Conversion from Functional Programs to Logically Constrained Conditional Term Rewrting Systems
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: [発表概要, Unrefereed Presentatin Abstract]
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 新潟大学大学院自然科学研究科
• 著者所属: 新潟大学大学院自然科学研究科
• 著者所属(英): en
• 著者所属(英): Graduate School of Science and Technology, Niigata University
• 著者所属(英): en
• 著者所属(英): Graduate School of Science and Technology, Niigata University
• 著者名: 冨田, 也斗; 青戸, 等人
• 著者名(英): Kanato, Tomita; Takahito, Aoto
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 項書き換えシステム（TRS）とは等式論理に基づく計算モデルの1つである．条件付き項書き換えシステム（CTRS）は，関数型プログラムのモデル化に適したモデルといわれている．しかし，非決定的な計算による簡約化によって正規形を求めるTRSと，関数型プログラムとの間には大きなギャップがある．また，そのギャップも対象とする関数型言語によって様々である．近年，関数型言語の部分的な機能に対するTRSへの変換や，手続き型言語から制約付き項書き換えシステム（LCTRS）への変換については報告されているが，関数型言語からTRSへの具体的な変換手法についてはあまり詳細には議論されていない．本発表では，関数型言語であるML言語を取り上げ，TRSとMLプログラムとの変換を考察する．両者の違いとして，前者は第1階の関数しか用いないのと対照的に，後者では，高階の関数が用いられているという点がある．このため，高階の関数プログラムを第1階の関数に変換するDefunctionalizationを適用した後に得られるMLプログラムを出発点として，TRSへの変換を考える．MLプログラムの評価規則を素直に対応させるために，変換先のTRSの体系として，論理制約付き条件付き項書き換えシステム（LCCTRS）を用いることを提案する．MLプログラムのラージステップ意味論に基づく評価と，変換によって得られたLCCTRSの簡約に基づく評価との対応関係について考察する．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Term rewriting systems (TRSs) are a computational model based on equational logic. Conditional term rewriting systems (CTRSs) are said to be a model suitable for modeling functional programs. There is, however, a big gap between TRSs, which computes the normal form by non-deterministic rewriting and functional programming. Moreover, the gap also varies depending on the functional languages. In recent years, there have been reports on how to simulate some particular mechanism of functional languages in TRSs, and on conversion from procedural languages to logically constrained TRSs (LCTRSs). However, the transformation method has not been discussed in much detail. In this presentation, we take the functional language ML, and consider the translation between TRSs and ML programs. One of the differences between the two is that the former uses only first-order functions, while the latter uses higher-order functions. For this reason, we take, as our starting point for conversion to TRSs, ML programs obtained after applying defunctionalization, which transforms higher-order functional programs into first-order functional programs. We propose to use logically constrained conditional TRSs (LCCTRSs) as the framework of TRSs converted from ML programs, in order to reflect the evaluation rules of ML programs. We consider the correspondence between evaluation based on large-step semantics of ML programs and evaluation based on reduction of LCCTRS obtained by transformation.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 16, 号 2, p. 30-30, 発行日 2023-06-29
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会