Convergent Term Rewriting Systems for Inverse Computation of Injective Functions
Naoki Nishida, Masahiko Sakai, Terutoshi Kato · Institutional Repositories DataBase (IRDB) · 2007
Abstract. This paper shows a sufficient syntactic condition for constructor TRSs whose inverse-computation CTRSs generated by Nishida, Sakai and Sakabe’s inversion compiler are confluent and operationally terminating. By replacing the unraveling at the second phase of the compiler with Serbanuta and Rosu’s transformation, we generate convergent TRSs for inverse computation of injective functions satisfying the sufficient condition. 1