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

項書き換えシステム（TRS）とは等式論理に基づく計算モデルの1つである．条件付き項書き換えシステム（CTRS）は，関数型プログラムのモデル化に適したモデルといわれている．しかし，非決定的な計算による簡約化によって正規形を求めるTRSと，関数型プログラムとの間には大きなギャップがある．また，そのギャップも対象とする関数型言語によって様々である．近年，関数型言語の部分的な機能に対するTRSへの変換や，手続き型言語から制約付き項書き換えシステム（LCTRS）への変換については報告されているが，関数型言語からTRSへの具体的な変換手法についてはあまり詳細には議論されていない．本発表では，関数型言語であるML言語を取り上げ，TRSとMLプログラムとの変換を考察する．両者の違いとして，前者は第1階の関数しか用いないのと対照的に，後者では，高階の関数が用いられているという点がある．このため，高階の関数プログラムを第1階の関数に変換するDefunctionalizationを適用した後に得られるMLプログラムを出発点として，TRSへの変換を考える．MLプログラムの評価規則を素直に対応させるために，変換先のTRSの体系として，論理制約付き条件付き項書き換えシステム（LCCTRS）を用いることを提案する．MLプログラムのラージステップ意味論に基づく評価と，変換によって得られたLCCTRSの簡約に基づく評価との対応関係について考察する．

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.