Yuji Sugiyama, Ichiro Suzuki, Kenichi Taniguchi, Tadao Kasami

Research output: Contribution to journalArticlepeer-review


The meaning of each statement in an algebraic specification language can be defined simply. The verification of a description in such a language can be treated in the same framework of the language itself. However, in general, there is no efficient method for implementing the language. In this paper, the authors introduce an algebraic specification language which is a subclass of strongly sequential term rewriting systems (TRSs for short) with constructors of HUET-LEVY, called completely sequential TRSs. For a TRS of this class, one can determine easily the needed radices of a given term. An efficient algorithm is presented for computing, for any substitution s of constants to variables of t, the constant normal form of s(t) in R, where R is a given completely sequential TRS and t is a given term with variables. In the algorithm, directed acyclic graph (dag) representation of terms allows one to avoid the repeated computation for identical terms. Computation is carried out only when it is necessary, and a straightforward dag copy is avoided. A method for compiling dags into programs which run efficiently is presented.

Original languageEnglish
Pages (from-to)22-30
Number of pages9
JournalSystems, computers, controls
Issue number4
Publication statusPublished - Jan 1 1982

ASJC Scopus subject areas

  • Engineering(all)


Dive into the research topics of 'EFFICIENT EXECUTION IN A CLASS OF TERM REWRITING SYSTEMS.'. Together they form a unique fingerprint.

Cite this