Japan Advanced Institute of Science and Technology

Japan Advanced Institute of Science and Technology

JAIST Repository

https://dspace.jaist.ac.jp/

Title

Author(s)

Citation

Issue Date

Type

Text version

URL

Rights

Description

Takashi Nagaya

School of Information Science,

Japan Advanced Institute of Science and Technology

January 14, 1999

Abstract

Term rewriting systems have been widely studied as a model for computation. In a

termrewriting system,theymayexistaninnitereductionsequencestartingwithaterm

havingnormalforms. Inordertoget anormalformforagiventerm,werequireanormal-

izing strategy guaranteeing to nd a normal form of terms whenever their normal forms

exist. Huet andLevy(1979) showedthat acall-by-need strategy isnormalizingfor every

orthogonal (i.e., left-linearand non-overlapping)term rewriting systems. Unfortunately,

in general a call-by-need strategy is undecidable. They formalized strong sequentiality

guaranteeing adecidable normalizingcall-by-needstrategy for orthogonalterm rewriting

system. The workof Huet andLevy has been extendedto several kinds of systems.

In this thesis we rst extend the class of left-linear term rewriting systems having a

decidable call-by-need strategy. We present the class of NVNF-sequential systems. This

classproperlyincludestheclassofNV-sequentialsystemswhichwasintro ducedbyOyam-

aguchi(1993). We provethat everyorthogonal NVNF-sequential system has adecidable

normalizingcall-by-needstrategy. Thenwegivegrowingapproximationsoftermrewriting

systemswithouttheassumptionoftheright-linearitywhereasJacuemard(1993)assumed

theright-linearity. Weshowthatourapproximationsextend theclassoforthogonalterm

rewriting systems having a decidable normalizingcall-by-need strategy.

Secondly, we investigate the normalizability of a call-by-need strategy for left-linear

overlapping term rewriting systems. We rst intro duced the notion of stable balanced

joinability. Itisshownthatacall-by-needstrategyisnormalizingforeverystablebalanced

joinable strongly sequential system. This is a generalization of Toyama's result (1992).

Wenextintro ducethe notionofNV-stablebalanced joinabilityand provethateveryNV-

stable balanced joinable NV-sequential system has a decidable normalizing call-by-need

strategy.

Finally, we apply the results on call-by-need strategy to the E-strategy adopted by

the OBJ algebraic specication languages. The E-strategy chooses a redex according to

local strategies which are given to each function symb ol. We consider how to give local

strategiestomaketheE-strategynormalizing. Forthispurpose,weintro ducedthe notion

index-transitivity and carefulness. We show that for every index-transitive orthogonal

Copyrightc 1999byTakashiNagaya

the E-strategy is normalizing.

Key Words: term rewriting system, reduction strategy, normalizability,

sequentiality