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

YoshihiroMatsuno

February 14, 1997

Abstract

E-unicationisaproblemtondasubstitutionthatmakessandtequalonamoduloof

equationaltheoryEfoetermssandt. Tosolveanequationeciently,narrowingwasintro duced.

Intheeldofdeclarativeprogramming,E-unicationhasrecievedsp ecialattentionrecently,

since it has become clear that E-unication is the key computation mechanism in integrat-

ing functional and logic programming. Programming method that integrates functional and

logic programmingis called functional-logicprogramming. Namely, oneof the mostpromising

approach to the integration is equation solving as a computational model of functional-logic

programming.

Narrowingwasrststudiedinthecontextof anecient waytondE-unier. Atrst, Fay

proposeditandHullotrenedit. Theyshowedthatnarrowingisacompletemetho dforsolving

equations in the conuent and terminating term rewriting system. Completeness means that

narrowingcan nd general solution for anysolution to concerning equations. It is knownthat

narrowing with resp ect to normalized substitution is complete. we can drop the condition of

termination. Inother words,narrowingis completeforconuenttermrewritingsystems.

In general,narrowingtakes largesearchspace. In order to reduce search space, Hullot pro-

posed to basic narrowing. He showed that basic narrowing is complete for conuent and ter-

minatingtermrewritingsystems. Basicnarrowingis notcompleteforconuent termrewriting

systemswithrespecttonormalizedsubstitution. Thisnarrowinghasparticularformsofnarrow-

ingsequence. Certainsubtermsofsand termobtainedfromsbynarrowing,arenevernarrowed

themselves. Aartshowedthatbasicnarrowingiscompleteforrightlineartermrewritingsystem

withrespecttonormalized substitution.

Narrowingworkson equational theory and logicprogrammingon hornlogic, butb oth nar-

rowingandlogicprogramminguseunicationtocalculate. Becauseofthis,thesedaysthereare

much interest in incorporating thefunctional programming paradigms and logic programming

paradigms.

For example, programming language ALF uses inner most narrowing instead of logic pro-

gramming'sderivation. Tousenarrowinginsteadofderivation,wecanamalgamebothfunctional

programmingparadigmandlogicprogrammingparadigm. Recently,thisareaisstudiedbyusing

lazynarrowinginsteadof narrowing. Examples includean abstract machine LNAM.

But narrowingis nondeterminstic asregards tochoices of rewrite rule and redexies, and in

generalnarrowingis inecient. sovariousstrategies forreducing searchspace are prop osed.

Thisstudy'saim istondredexintermspeedy. So ,byusingtree paternmatching'sidea ,

thewaytocreatean automaton forunication

On one hand, many speedy methods to Tree pattern matching have b een prop osed. For

several patterns, eectively patterns are matched by using these methods. So, subterms that

Copyright c

1997byYoshihiroMATSUNO

uniabletopatterns. So,thismethodwerwabletouseinnarrowingprocess,itisexp ectedthat

itmakes narrowingeective .

So in this study ,we make improvements on the sp eedy method for tree pattern matching

andmakepossibletoapplyuniication. We madenarrowingeectivebyusingtreeautomaton.

Inactually,wemadeexperimentswithnewmethodbyusingworkstation,anditwasrealized

that in the case that many pattern are used,this study's unication method is more eective

thanother methods.

According to this fact, we presupose that patterns and object terms are linear. And by

using this study's algorithm, we pickup patterns and sub object terms that have an abilityof

unication,and those patterns and termsare regardedasuniable candidates,it makegenaral

unicaiton algorithm apply those candidates . This metho d decides problems with nonlinear

patterns.

In fact, experienceson workstationmake usrealize thatthis method iseective.

This paperdiscussfollowing two items:

Constructionofautomatontondoutunifableoccurrence. byusingtreeautomatonsp eed

up thewaytond uniableoccurrence.

to establish a way to combine basicnarrowing and tree automaton to nd out uniable

o ccurrence.

Tree automaton's inputeddata areobjectterms and patterns arelinear.An evaluation was

made to this study's algorithm and Alberto Martell and Ugo Montanari'salgorithm . Results

areshownnext.

Therun timeofthis studyalgorithm is fasterthanAlberto's algorithm.

A precomputing time for making trasitional rules is under the inuence of pattern set's

character.

In thecase of that object termis big and table is repeatedly used, the overhead is small

thanrunning time'smerit.