Study on Inversion of Term Rewriting Systems — 項書換え系の逆計算に関する研究 — 2000

Content Provider	Semantic Scholar
Author	Nishida, Naoki
Copyright Year	2002
Abstract	There are many cases that we need a (conditional) term rewriting system (written as (C)TRS, for short) which computes the inverses of the functions defined by another (C)TRS. Such a CTRS is called an inverse system. Inverse systems are useful in such a case that a CTRS cannot compute the proper values of given terms while it seems natural and correct. That is, inverse functions may be used to transform the CTRS to an equivalent CTRS which can compute the proper values of all terms. For example, consider the rule f(x + y, y) → f(x, y), which cannot apply to any integer because the first argument of f in the left-hand side contains + and no integer contains +. This rule can be transformed equivalently to f(z, y) → f(z−y, y) by replacing the first argument x+y of f in the left-hand side with a fresh variable z and the first argument x of f in the right-hand side with z−y, where − is the inverse of +y defined as +y(x) = x+y. In this example, we fortunately know the CTRS which computes − i.e., the inverse of +y, and can do the transformation mechanically. However, we cannot assume that all definitions of necessary inverse functions are given. Therefore, it is desirable to automatically construct a CTRS of inverse functions from a given CTRS. This paper proposes a method that constructs an inverse system of a given constructor TRS. The inverse systems that our method constructs are generally CTRSs. We present a transformation of our inverse CTRSs into equivalent TRSs. We also show a result on termination of the inverse systems obtained by our method. We finally show an application of inverse systems to CTRS transformation.
File Format	PDF HTM / HTML
Alternate Webpage(s)	https://www.sakabe.i.is.nagoya-u.ac.jp/~nishida/DB/pdf/nishida02mthesis.pdf
Language	English
Access Restriction	Open
Content Type	Text
Resource Type	Thesis