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

Munehiro Iwami

School of Information Science

Japan Advanced Institute of Science and Technology

March 1999

Abstract

Higher-order rewriting is a natural extension of rst-order term rewriting systems to

reason with higher-order equations. Higher-order rewrite systems havebeen widely used

asa model of higher-order functionaland logic programming languages and as abasis of

higher-order theorem provers.

In term rewriting systems, several sucient conditions for proving the termination

property have b een successfully developed in particular cases. These techniques can be

classied into two approaches: semantic methods and syntactic methods. Simplication

orderings are representativesof syntacticmethods. Many simplicationorderings, for in-

stance,therecursivepathordering,theimprovedrecursivedecompositionordering andso

on,havebeenprop osedfortermrewritingsystems. Theimprovedrecursivedecomposition

ordering is one of the most powerful simplicationorderings.

In higher-order rewrite systems, Jouannaud and Rubio gave a denition of recursive

path ordering for higher-orderrewrite systems by intro ducing anordering on typ e struc-

ture recently.

In this thesis, we study the termination of higher-order rewrite systems by syntactic

approaches.

First,we extendtheimprovedrecursivedecompositionorderingtohigher-orderrewrite

systems for proving termination. Our extensionis inspiredfrom Jouannaud and Rubio's

idea. This ordering iscalled the higher-order improved recursive decompositionordering.

Further, we show that this ordering is more powerful than the Jouannaud and Rubio's

ordering.

Next, we intro duce the notion of simplication orderings for higher-order rewrite sys-

tems. More precisely, we dene the simplication ordering on algebraic terms where an

algebraicterm is-long-normalformwithout-abstractions. Bythisdenition, wecan

analyze the termination of higher-order rewrite systems in abstract level. Further, we

dene a new recursive path ordering for higher-order rewrite systems, called the higher-

order recursive path ordering. Our ordering extends Jouannaud and Rubio's ordering,

which doesnot allow comparingtwo typ e incompatibleterms. We show through several

systems to whichJouannaud and Rubio's ordering cannot b eapplied.

Finally,weextendthe persistentpropertyofterminationtoordersortedtermrewriting

systems. First-order term rewriting systems are special cases of higher-order rewrite

systems. So we analyze the termination of rst-order term rewriting systems using the

notion of persistence. Zantema showed that termination is persistent for term rewriting

systems without collapsing or duplicating rules. We show that Zantema's result can be

extended to order sorted term rewriting systems, i.e, termination is persistent for order

sorted term rewriting systems withoutcollapsing, decreasing or duplicatingrules.

Key Words: higher-order rewritesystem, termrewriting system,termina-

tion, simplication ordering, improved recursive decomposi-

tion ordering, recursive path ordering, persistence