Dag Representation and Optimization of Rewriting

@misc{li_dag_nodate,
	title = {Dag {Representation} and {Optimization} of {Rewriting}},
	abstract = {In all applications of term rewriting systems, computing the normal forms of  terms is the fundamental step. In this paper, we propose a directed acyclic  graph (dag) representation for term and term rewriting. The rewriting on dags  is much more efficient than the rewriting on trees. We design several efficient  strategies for rewriting on dags. By dag representation, we can even obtain  efficient rewriting strategies for non-left-linear rewriting systems.  This research was supported in part by the National Science Foundation under grant number CCR-89-6949.  1 Introduction  In any application of term rewriting systems (TRSs for short), computing normal form of terms is a basic procedure. In language application, the semantics of a term is its normal form [Der85]. In solving word problem [KB70], to test equivalence of two terms t and s, the normal forms of t and s are computed. To unify terms in an equation theory, the equations are transformed to a terminating and confluent TRS and t...},
	author = {Li, Ke},
	url={https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.43.6572&rep=rep1&type=pdf}
}

Abstract

• DAGとして正規化するとrewritingしやすくなる

Introduction

• 項書換えシステム(Term Rewriting System)の応用では項の正規形を計算することが基本的な手続き
• 言語の応用では、項の意味論はその正規形である[Der85]
• 単語問題の解法[KB70]では、2つの項tとsの等価性を調べるために、tとsの正規形が計算される
• 方程式論の項を統一するために、方程式を終端一致のTRSに変換し、項の正規形を計算する[Hu80]
• 論理型言語と関数型言語の結合では、ホーン節にTRSを付加し、節の単一化の際に正規形を計算する [SY86][GM86]

よって, 正規形を効率的に計算することは項書換えアプリとして重要

DAG上の効率的な変形じゃなくて効率的な正規形への変換