Abstracts of Papers

Ａ−81

Department of Information Engineering* nonmember
The Unification Problem for Confluent Right-Ground Term Rewriting Systems, Michio OYAMAGUCHI andYoshikatsu OHTA: Information and Computation 183, pp.187-211, 2003.
The unification problem for term rewriting system (TRS) is the problem of deciding, for a given TRS
R and two terms M and N, whether there exists a substitution θ such that Mθ and Nθ are congruent modulo R(i.e., Mθ <->*_R Nθ). In this paper, the unification problem for confluent right-ground TRSs is shown to be
decidable. To show this, the notion of minimal terms is introduced and a new unification algorithm for obtaining
a substitution whose range consists of minimal terms is proposed. Our result extends the decidability ofunification for canonical (i.e., terminating and confluent) right-ground TRSs given by Hullot (1980) in the sensethat the termination condition can be omitted.

On the Unification Problem for Confluent Monadic Term Rewriting Systems [in Japanese], Ichiro
MITSUHASHI, Michio OYAMAGUCHI, Yoshikatsu OHTA and Toshiyuki YAMADA: Trans. of IPSJ, Vol.44,
No.SIG 4(PRO 17), pp.54-66, March. 2003.
The unification problem for term rewriting systems (TRSs) is the problem of deciding, for a TRS R
and two terms M and N, whether M and N are unifiable modulo the congruence generated by R. The unification
problem is undecidable even if we restrict ourselves to the class of right-ground TRSs, which is a subclass of
TRSs. On the other hand, it has been shown to be decidable for the class of confluent right-ground TRSs by
Oyamaguchi and Ohta (2001). In this paper, we extend their algorithm and show that the unification problem isdecidable for the class of confluent TRSs consisting of not only right-ground rules but also collapsing rules.

On the Church-Rosser Property of Left-Linear Term Rewriting Systems, Michio OYAMAGUCHI andYoshikatsu OHTA: Trans. of IEICE, Vol.E86-D, No.1, pp.131-135, 2003.
G.Huet (1980) showed that a left-linear term-rewriting system (TRS) is Church-Rosser (CR) if P -|->Q for every critical pair < P, Q > where P -|-> Q is a parallel reduction from P to Q. This paper shows that
Huet's result can be generalized under the assumption that a subsystem K of TRS R (i.e., K is a subset of R) is
CR. That is, we show that R is CR if P -|->_K Q for every <P,Q> in CP(K,R-K) and P -|->_{R-K} .->*_K.<-*_K
Q for every < P, Q > in CP(R-K,R). Here, CP(R1,R2) is the set of critical pairs obtained from some rule of R1
and one of R2.

Proving Termination of Simply Typed Term Rewriting Systems Automatically, Takahito AOTO* and Toshiyuki
YAMADA: IPSJ Transactions on Programming, vol. 44 (SIG 4 PRO 17), pp. 67-77, March 2003.
Simply typed term rewriting proposed by Yamada (RTA'01, 2001) is a framework of term rewriting
allowing higher-order functions. In contrast to the usual higher-order term rewriting frameworks, simply typed
term rewriting dispenses with bound variables. In this paper, we present a method to prove termination of simply
typed term rewriting systems. We first give a transformation on term rewriting systems and show thattermination of simply typed term rewriting systems is induced from that of the first-order term rewriting systems
obtained by this transformation. We next introduce a labelling technique which facilitates termination proof of
the first-order term rewriting systems obtained by our transformation. Contrary to the semantic method proposedby Yamada (RTA'01, 2001), our technique is based on a syntactic approach; and thus one can easily automate
termination proof of simply typed term rewriting systems.

Termination of Simply Typed Term Rewriting Systems by Translation and Labelling, Takahito AOTO* andToshiyuki YAMADA: Proceedings of the 14th International Conference on Rewriting Techniques andApplications (RTA 2003), LNCS 2706, pp.380-394, June 2003.
Simply typed term rewriting proposed by Yamada (RTA 2001) is a framework of term rewriting
allowing higher-order functions. In contrast to the usual higher-order term rewriting frameworks, simply typed
term rewriting dispenses with bound variables. This paper presents a method for proving termination of simply
typed term rewriting systems (STTRSs, for short). We first give a translation of STTRSs into many-sorted
first-order TRSs and show that termination problem of STTRSs is reduced to that of many-sorted first-orderＡ−82

Abstracts of Papers

TRSs. Next, we introduce a labelling method which is applied to first-order TRSs obtained by the translation tofacilitate termination proof of them; our labelling employs an extension of semantic labelling where terms areinterpreted on a many-sorted algebra.

Proving Inductive Theorems of Higher-Order Functional Programs, Takahito AOTO*, Toshiyuki YAMADA andYoshihito TOYAMA*: Information Technology Letters, vol. 2, pp. 21-22, August 2003.
Regarding a functional program as a set of equatinoal axioms, an equational property of the program
corresponds to an inductive theorem in equational logic. Using automatic method for proving inductive theorems
in equational logic, we can efficiently verify specifications and programs. Only few attempts have been made toincorporate higher-order functions to automatic inductive theorem proving, although higher-order function is an
important feature in functional programming. Based on the framework of simply typed term rewriting system,
we propose a method to prove that a given equation is an inductive theorem of a set of exational axioms in thepresence of higher-order functions.

A Parallel Program Debugger supporting Reverse Execution [in Japanese],Masao MARUYAMA*, Shigehiro
YAMAMOTO*, Kazuhiko OHNO and Hiroshi NAKASHIMA*: Symposium on Advanced Computing Systems
and Infrastructures SACSIS2003, pp.65-72, 2003.
Reverse execution is a powerful technique of debugging. Some serious problems arise, however, inapplying it to parallel programs because of its indeterministic nature. Since a parallel programs's behavior can bedifferent from run to run, entire information for locating the bug must be checkpointed in single execution. It
causes, in most cases, the users to collect much larger set of information than really needed. It is particularly
serious when locating the inreproductive bugs. The users have to run the program repeatedly with costly
checkpointing operation until the bug appears. Therefore we propose a debugging model for parallel program
based on checkpointing/rollbacking combind with replay method to overcome these weak points. We applied it
to a parallel programming language Orgel, and developed a debugger supporting execution rollback for Orgel
programs. Our mechanism works at practical cost in execution, and can provide useful and powerful functions to
the parallel debuggers which justify some extra cost.

A Task Parallel Script Language MegaScript [in Japanese], Yasunori OHTSUKA*, Tasuku FUKANO*, Hitoshi
NISHIZATO*, Kazuhiko OHNO and Hiroshi NAKASHIMA*: Symposium on Advanced Computing Systems
and Infrastructures SACSIS2003, pp.73-76, 2003.
This paper proposes a task-parallel script language named MegaScript for megascale computing. A
MegaScript program has a tow-tier parallelism; the lower is an ordinary parallelism such as SPMD and the upperis task-level parallelism in which thousands of lower level parallel tasks are inveolved. The MegaScript provides
a hierarchical function library for lower level parallel task management, which is enough easy-to-write for end
users and also enough detailed for heavy users. Moreover, the MegaScript has a special feature formeta-programming to represent an abstracted behavior of parallel tasks. This abstracted behavior, combined withcompile-time analysis result and execution profile, is userd for optimal runtime task scheduling. The MegaScript
system consists of a translator, runtime, and scheduler. The translator builds the execution model of tasks fromthe meta-program. The runtime creates tasks and manages the communication among them. The scheduler
determines the granularity, allocation and ordering/timing of the task exection referring the model and refines themodel with the profile for future use.

High Speed Simulation of High Performance Processor [in Japanese], Takashi NAKADA*, Kazuhiko OHNO
and Hiroshi NAKASHIMA*: Symposium on Advanced Computing Systems and Infrastructures SACSIS2003,
pp.89-96, 2003.
Microprocessor simulation is indispensable not only for hardware systems design but also for softwaredevelopment of co-designed embedded systems. In both design fields, cycle accurate (or clock level) simulationof highly sophisticated microprocessor is required. However, existing simulators of out-of-order processors run
programs thousands of times slower than actual hardware. The ultimate goal of our research is to develop a fast
and accurate simulator which is capable of microarchitectural modeling and system level simulation. Here, wetoward high speed simulation of high performance processor. Our primary contribution is the computation reuseto the expensive process of simulating an out-of-order microarchitecture. We record the instruction sequence of aloop together with its behavior and the microarchitecture states resulted from the sequence. When we find aAbstracts of Papers

Ａ−83

recorded state in the out-of-order microarchitecture simulation, we skip the simulation reusing the state until we
encounter a sequence unseen previously. We evaluated the implementation using a sample program of summing
up a one dimensional array to find our technique archives 8.1-fold speed up.

Design and Implementation of Megascale simulator Anastasia [in Japanese], Syunsuke SHIBATA*, Takeo
SUZUKI*, Kazuhiko OHNO and Hiroshi NAKASHIMA*: Symposium on Advanced Computing Systems andInfrastructures SACSIS2003, pp.153-154, 2003.
We are pursuing a research project on megascale computing in which more than one million
processors are involved. This paper proposes a simulator named Anastasia which provides a virtual megascale
environment on a small to medium range PC cluster. Anastasia converts timing of megascale applications andsoftware systems on the host cluster to that on the virtual target environment. To evaluate the validity of thetiming management and scheduling, we build a prototype of Anastasia and measured its timing accuracy with asimple parallel application executed on a virtual PC cluster. The result shows that the timing error between thevirtual and real cluster is only 3.6% at most.

A Proposal of Combined Method of Evolutionary Algorithm and Heuristics for Nurse Scheduling Support
System, Takeshi INOUE*, Takeshi FURUHASHI, Hiroshi MAEDA* and Minoru TAKABA*: IEEE
Transactions on Industrial Electronics, Vol.50, No.5, pp.833-838, 2003.
The Nurse Scheduling Problem (NSP) is a combinatorial optimization problem. There is a growing
demand for practical automatic nurse scheduling systems. We have a developed nurse scheduling support systemusing the Interactive Evolutionary Algorithm. The nurse-in-chief can modify/fix parts of candidate schedules.
The system reschedules the parts that need improvement. The proposed system is required to produce
high-quality schedules with a short computation time for good human-machine interaction. This paper presents amethod that combines heuristics with genetic operations for generating good schedules quickly, especially forsatisfying the equality among nurses. This paper clarifies the effects of the proposed heuristics and also studies
effects of a combination of the proposed method and the conventional mutation operation. Experiments are
conducted to demonstrate theses effects.

Phase Transitions in Fuzzy Clustering Based on Fuzzy Entropy, Makoto YASUDA*, Takeshi FURUHASHI and
Shigeru OKUMA*: Journal of Advanced Computational Intelligence and Intelligent Informatics, Vol.7, No.3,
pp.370-376, 2003.
We studied the statistical mechanical characteristics of fuzzy clustering regularized with fuzzy entropy.
We obtained Fermi-Dirac distribution as a membership function by regularizing the fuzzy c-means with fuzzy
entropy. We then formulated it as direct annealing clustering, and determined the meanings of the Fermi-Diracfunction and fuzzy entropy from the statistical mechanical point of view, and showed that this fuzzy clustering isa part of Fermi-Dirac statistics. We also derived the critical temperature at which phase transition occurs in thisfuzzy clustering. Then, with a combination of cluster divisions by phase transitions and an adequate division
termination condition, we derived fuzzy clustering that automatically determined the number of clusters, asverified by numerical experiments.
Interpretability Issues in Fuzzy Modeling, Toshihito SUZUKI*, Takeshi FURUHASHI et.al.: Conciseness offuzzy models, Springer-Verlag, pp.568-586, 2003.
Fuzzy models are used to describe input-output relationships of unknown nonlinear systems in aninterpretable manner for humans. Interpretability is one of the indispensable features of fuzzy models, which is
closely related to their conciseness. The authors introduce the conciseness of fuzzy models, based on
observations that humans grasp the input-output relationships by granules. The conciseness measure is thenformulated by introducing De Luca and Termini’s fuzzy entropy and a new measure is derived from the analogyof relative entropy. This chapter also discusses the conflicting relationships between the conciseness and theaccuracy of fuzzy models. A fuzzy modeling with Pareto optimal solutions is presented. Numerical experiments
are done to demonstrate the effects of the conciseness measure.

Code set design for digital polarity correlators in a multiple user sonar ranging system, Reo TSUJI, Tetsuji
KODAMA, Takeshi FURUHASHI, Kenji NAKAHIRA and Hiroshi MAEDA: SICE Annual Conference 2003 in
Fukui Proceedings, 2746-2750, 2003.

Ａ−84

Abstracts of Papers

In pulsed ultrasonic distance measurement systems, the pulse compression techniques were adopted toeliminate frequent misreadings caused by crosstalk or external ultrasound sources. In this paper, we present
digital polarity correlators designed for the binary coded frequency shift keyed signals. For the multiple user
code set design, we propose the use of a combination of genetic algorithm and hill climbing.

Robust Regression Under Asymmetric or/and Non-Constant Variance Error by Simultaneously Training
Conditional Quantiles, Ichiro TAKEUCHI, Noriyuki YAMANAKA and Takeshi FURUHASHI: IJCNN 2003
Proceedings (cd-rom).
We consider regression problems under asymmetric or/and non-constant variance error. We see thisproblem in several fields such as insurance premium estimation, medical cost analysis, etc. Applying the methodof Least Squares (LS) to this problem yields unstable solution because of outliers that appears on one side ofregression surfaces. Conventional robust techniques to deal with outliers, which intend to discard or
down-weight the outliers equallyfrom both sides of regression surfaces, do not help for asymmetric error. In thispaper, we propose an robust regression estimator (an estimator of the conditional mean) under asymmetric or/and
non-constant variance error by simultaneously training conditional quantiles in multi-layer perceptron (MLP).
This is considered as a kind of learning from hint or multitask learning approach, i.e. we train the conditional
quantile estimator as hints or extra tasks to improve generalization properties of the conditional mean estimator.
Numerical experiments and an application to medical cost estimation problem have shown that our proposal has
robustness and good generalization properties.

Noise Reduction Filter of Cascaded Sandglass-type Neural Network Adaptively Controlled by Noise Intensity
for Speech Signal [in Japanese], Toshie NAMIKI*, Yuki FURUMOTO*, Hiroki YOSHIMURA*, Tadaaki
SHIMIZU*, Naoki ISU and Kazuhiro SUGATA*: IEEJ Trans. EIS, Vol.123, No.3, pp.430-439, 2003.
An adaptive noise reduction filter composed of Cascaded Sandglass-type Neural Network (CSNNRF)
is proposed to develop a hearing aid appliance. The number of unit sandglass-type neural networks (SNNs) is
controlled adaptively by noise intensity. Usually the hearing aid works outside where noise intensity is altering
all the times. An adaptive noise reduction filter controlled by noise intensity is essential to cope with thesecircumstances. Each SNN has a three-layer structure and consists of the same number of neural units in the input
and output layers and a single neural unit in the hidden layer. SNNs are connected in cascaded to be CSNNRF.
The number of unit SNNs is adaptively determined by our algorithms so that hearing intelligibility for speech
signal may be processed more preferably. To determine the number of SNNs, we regard significance on theintelligibility more than numerical value itself such as S/N ratio of speech signal.

Optimal Phonemic Environmental Range to Select VCV Instances for VCV Speech Synthesis by Rule [inJapanese], Tadaaki SHIMIZU*, Masaya KIMOTO*, Hiroki YOSHIMURA*, Toshie NAMIKI*, Naoki ISU and
Kazuhiro SUGATA*: IEEJ Trans. EIS, Vol.123, No.3, pp.467-474, 2003.
We proposed two selection methods, 1) selection method by using phonemic environmental
resemblance score (PER method), and 2) selection method by searching minimal connective distortion path
(MLD method), for small scale speech synthesis system. PER method requires phonemic environmental
information for each VCV instance in a VCV unit dictionary. This paper investigated experimentally to what
extent we can reduce the phonemic environmental information with keeping high quality of synthesized speech.
We verified that two phonemes frontward and one phoneme rearward range to a current VCV instance is enoughto synthesize similar quality of speech as five phonemes frontward and five phonemes rearward. This result
gives an experimental basis on minimizing a size of VCV unit dictionary.

Coding Method of LSP Residual Signals Using Wavelets for Speech Synthesis [in Japanese], Tadaaki
SHIMIZU*, Masaya KIMOTO*, Hiroki YOSHIMURA*, Naoki ISU and Kazuhiro SUGATA*: IEEJ Trans. EIS,
Vol.123, No.5, pp.946-952, 2003.
This paper presents a method to use wavelet analysis for speech coding and synthesis by rule. It is acoding system where LSP residual signal is transformed into wavelet coefficients. As wavelet analysis is
implemented effectively by filter banks, our method is featured to require less computation than multipulse
coding and others where complicated prediction procedures are essential. To achieve good quality speech at low
bit rates, we verified to allocate the different bits onto the wavelet coefficients, with more bits in lower

Abstracts of Papers

Ａ−85

frequencies, and less in higher. The synthesized speech by Haar wavelet with 16.538 kbits/s has nearly same
perceptual quality with 6 bits mlog PCM (66.15 kbits/s). We are convinced that coding method of LSP residual
signals using wavelet analysis is an effective approach to synthesize speech.

The Metaphorical Judgment Model for "Noun B like Noun A" Expressions [in Japanese], Takehiro TAZOE＊,
Tsutomu SHIINO*, Fumito MASUI and Atsuo KAWAI: Journal of Natural Language Processing, Volume 10,
Number 2, pp.43-58, 2003.
We have been studying for the automatic recognition and extraction of metaphor expressions inpractical sentences. This paper introduces our metaphorical judgment model for "Noun B like Noun A"
expressions. "Noun B like Noun A" expressions are classified into two usages; simile and literality. To
automatically judge whether a phrase is simile or literality, "Noun B like Noun A" expressions were classified
into six patterns depending on the semantic information of a noun, and the metaphorical judgment model wasconstructed based on these patterns. When the "Noun B like Noun A" expressions from newspaper articles were
judged by the model, and its judgment was compared with the correct judgment, it was approximately 80%
correct. Thus, the model was found to be effective in the recognition of metaphor expressions in real-lifesituations.

A Model for Distinguishing Mass and Count Nouns, Ryo NAGATA, Fumito MASUI and Atsuo KAWAI: Pacific
Association for Computational Linguistics, Halifax, Nova Scotia, Canada,pp.1-9, Aug. 2003.
This paper proposes a model for distinguishing nouns that are used only as mass nouns from the othernouns. This paper also describes a method for making a dictionary of ill-formed nouns such as `*informations'using the model. The model and the method should be useful for detecting errors of noun usage in compositions
written by Japanese learners of English. Once a corpus and a few samples of mass nouns and count nouns are
given, the model is constructed automatically. As a result of experiments, the model yielded high F-measureperformance (F=88.5), and a dictionary that contained about 1,200 ill-formed nouns was obtained.

Tissue Characterization of Local Myocardium Using Phase Frequency Spectrum of Ultrasonic RF Signal,
Hirotake ISHII, Shinji TSURUOKA, Muhammad Ibn IBRAHIMY, Fumikata KIMURA, Tetsushi
WAKABAYASHI, Wataru OHYAMA and Kiyotsugu SEKIOKA*, Proc. of IEEE EMBS Asian-PacificConference on Biomedical Engineering (IEEE EMBS APBME2003), CD-ROM, #4.4.3, pp.1-2, 2003.
In this paper, to evaluate fine myocardium structure change from ultrasonic RF signal, we propose a
new “Phase Frequency Spectrum (PFS)” analysis about a specified local myocardium during cardiac cycle. The
analysis employs the small range centering on the point tracked by our tracking system on a RF signal, andapplies time-frequency analysis (wavelet transform) to the envelope of the RF signal. The result of our analysis
is shown as the two-dimensional image between frequency spectrum and cardiac-phase. We measured thechange of the phase frequency spectrum, and we confirmed experimentally the diagnostic usefulness of ouranalysis for a lot of normal and abnormal hearts.

Study on the Improvement in Accuracy of Automatic Tracking for Regional Myocardium Using Ultrasonic RF
Echo Signal, Yoshikazu YASUMOTO, Shinji TSURUOKA, Tomohiro YOSHIKAWA, Tsuyoshi SHINOGI,
Fumikata KIMURA, Tetsushi WAKABAYASHI, Wataru OHYAMA and Kiyotsugu SEKIOKA*, Proc. of IEEE
EMBS Asian-Pacific Conference on Biomedical Engineering (IEEE EMBS APBME2003), CD-ROM, #4.10.4,
pp.1-2, 2003.
This paper describes a study on the improvement in accuracy of the automatic tracking by correlation
method with confidence (CMC) proposed by our grope. The tracking method employs the correlation
coefficients at a position as the degree of confidence of the tracking for a specified observing point. It employs
the position obtained by hierarchical correlation method for an observing points if the correlation coefficient of
the observing point is high, and it employs the mean moved position of two nearby observing points at the sametime if the correlation coefficient of the observing point is low. However, we found the unfortunate case for the
tracking method, that is, the fact that the many points have low correlation coefficients at the same time. We
found that the large movement of myocardium causes the tracking error for CMC.

Ａ−86

Abstracts of Papers

Local Myocardial Motion Tracking Based on Correlation Weighted Phase Difference Method, Wataru
OHYAMA, Norlaila Binti ISMAIL, Tetsushi WAKABAYASHI, Fumitaka KIMURA, Shinji TSURUOKA, andKiyotsugu SEKIOKA, The Institute of Electronics, Information and Communication Engineers (IEICE)Transactions (Japanese Edition), Vol.J86-A, No.9, pp.917-928, 2003

In this paper, we propose a new method for automatically tracking the motion of local region in left
ventricular myocardium by means of ultrasonic pulsed Doppler signal. This method consists of a velocity
detection procedure based on correlation weighted mean instantaneous velocity and a motion tracking procedure
employing a myocardial elastic model. Most of ultrasonic pulsed Doppler signals observed in clinical diagnosis
contain considerable amount of speckle noise, which causes detection error of velocity. The detection error isaccumulated in the motion tracking procedure and yields obviously incorrect motion trajectory. The procedure ofcorrelation weighted mean velocity is aimed to reduce the velocity detection error, and the myocardial elastic
model is used to avoid the accumulation of the error to keep track of the motion of the myocardium in reasonableaccuracy. The result of evaluation test shows that this method is able to improve the accuracy of tracking
approximately 40 % relative to a conventional CLS approach.

Mirror Image Learning for Autoassociative Neural Networks, Shusaku SHIMIZU, Wataru OHYAMA, Tetsushi
WAKABAYASHI and Fumitaka KIMURA: Seventh International Conference on Document Analysis andRecognition (ICDAR'03) Proceedings, pp.804-808, September, 2003
This paper studies on the mirror image learning algorithm for the autoassociative neural networks andevaluates the performance by handwritten numeral recognition test. Each of the autoassociative networks is firsttrained independently for each class using the feature vector of the class. Then the mirror image learningalgorithm is applied to enlarge the learning sample of each class by mirror image patterns of the confusingclasses to achieve higher recognition accuracy. Recognition accuracy of the autoassociative neural networkclassifier was improved by the mirror image learning from 98.76% to 99.23% in the recognition test for
handwritten numeral database IPTP CD-ROM1.

Accuracy improvement of automatic text classification based on feature transformation, Guowei ZU, Wataru
OHYAMA, Tetsushi WAKABAYASHI and Fumitaka KIMURA: Proc. the 2003 ACM Symposium on Document
Engineering (DocEng 03), pp.118-120, November, 2003
In this paper, we describe a comparative study on techniques of feature transformation andclassification to improve the accuracy of automatic text classification. The normalization to the relative word
frequency, the principal component analysis (K-L transformation) and the power transformation wereapplied to the feature vectors, which were classified by the Euclidean distance, the linear discriminantfunction, the projection distance, the modified projection distance and the SVM.