For simply-typed term rewriting systems (STRSs) and higher-order rewrite systems (HRSs) a la Nipkow, we proposed a method for proving termination, namely the static dependency pair method. The method combines the dependency pair method introduced for first-order rewrite systems with the notion of strong computability introduced for typed λ-calculi. This method analyzes a static recursive structure based on definition dependency. By solving suitable constraints generated by the analysis, we can prove termination. In this paper, we extend the method to rewriting systems for functional programs (RFPs) with product, algebraic data, and ML-polymorphic types. Although the type system in STRSs contains only product and simple types and the type system in HRSs contains only simple types, our RFPs allow product types, type constructors (algebraic data types), and type variables (ML-polymorphic types). Hence, our RFPs are more representative of existing functional programs than STRSs and HRSs. Therefore, our result makes a large contribution to applying theoretical rewriting techniques to actual problems, that is, to proving the termination of existing functional programs.

This paper proposes a method for detecting determiner errors, which are highly frequent in learner English. To augment conventional methods, the proposed method exploits a strong tendency displayed by learners in determiner usage, i.e., mistakenly omitting determiners most of the time. Its basic idea is simple and applicable to almost any conventional method. This paper also proposes combining the method with countability prediction, which results in further improvement. Experiments show that the proposed method achieves an F-measure of 0.684 and significantly outperforms conventional methods.

Most of FPGAs have Configurable Logic Blocks (CLBs) to implement combinational and sequential circuits and block RAMs to implement Random Access Memories (RAMs) and Read Only Memories (ROMs). Circuit design that minimizes the number of clock cycles is easy if we use asynchronous read operations. However, most of FPGAs support synchronous read operations, but do not support asynchronous read operations. The main contribution of this paper is to provide one of the potent approaches to resolve this problem. We assume that a circuit using asynchronous ROMs designed by a non-expert or quickly designed by an expert is given. Our goal is to convert this circuit with asynchronous ROMs into an equivalent circuit with synchronous ones. The resulting circuit with synchronous ROMs can be embedded into FPGAs. We also discuss several techniques to decrease the latency and increase the clock frequency of the resulting circuits.

This letter has retrained an MQDF classifier on the retraining set, which is constructed by samples locating near classification boundary. The method is evaluated on HCL2000 and HCD Chinese handwriting sets. The results show that the retrained MQDF outperforms MQDF and cascade MQDF on all test sets.

The unification problem for term rewriting systems (TRSs) is the problem of deciding, for a TRS R and two terms s and t, whether s and t are unifiable modulo R. We have shown that the problem is decidable for confluent simple TRSs. Here, a simple TRS means one where the right-hand side of every rewrite rule is a ground term or a variable. In this paper, we extend this result and show that the unification problem for confluent semi-constructor TRSs is decidable. Here, a semi-constructor TRS means one where all defined symbols appearing in the right-hand side of each rewrite rule occur only in its ground subterms.

Inductive theorem proving plays an important role in the field of formal verification of systems. The rewriting induction (RI) is a method for inductive theorem proving proposed by Reddy. In order to obtain successful proofs, it is very important to choose appropriate contexts (such as in which direction each equation should be oriented) when applying RI inference rules. If the choice is not appropriate, the procedure may diverge or the users have to come up with several lemmas to prove together with the main theorem. Therefore we have a good reason to consider parallel execution of several instances of the rewriting induction procedure, each in charge of a distinguished single context in search of a successful proof. In this paper, we propose a new procedure, called multi-context rewriting induction, which efficiently simulates parallel execution of rewriting induction procedures in a single process, based on the idea of the multi-completion procedure. By the experiments with a well-known problem set, we discuss the effectiveness of the proposed procedure when searching along various contexts for a successful inductive proof.

Chiba et al. (2006) proposed a framework of program transformation of term rewriting systems by developed templates. Contrast to the previous framework of program transformation by templates based on lambda calculus, this framework provides a method to verify the correctness of transformation automatically. Tupling (Bird, 1980) is a well-known technique to eliminate redundant recursive calls for improving efficiency of programs. In Chiba et al.'s framework, however, one can not use tuple symbols to construct developed templates. Thus their framework is not capable of tupling transformations. In this paper, we propose a more flexible notion of templates so that a wider variety of transformations, including tupling transformations, can be handled.

We propose a user-defined on-demand matching strategy, called O-matching, in which users can control the order of matching arguments of each operation symbol. In ordinary matching schemes it is not important to set the order of matching, however, in on-demand matching schemes, it is very important since an input term may be changed while doing the on-demand matching process. O-matching is suitable to combine with the E-strategy, which is a user-defined reduction strategy in which users can control the order of reducing arguments. We show a sufficient condition under which the E-strategy with O-matching is correct for head normal forms, that is, any reduced term is a head normal form.

A lexicon-driven segmentation-recognition scheme on Bangla handwritten city-name recognition is proposed for Indian postal automation. In the proposed scheme, at first, binarization of the input document is done and then to take care of slanted handwriting of different individuals a slant correction technique is performed. Next, due to the script characteristics of Bangla, a water reservoir concept is applied to pre-segment the slant corrected city-names into possible primitive components (characters or its parts). Pre-segmented components of a city-name are then merged into possible characters to get the best city-name using the lexicon information. In order to merge these primitive components into characters and to find optimum character segmentation, dynamic programming (DP) is applied using total likelihood of the characters of a city-name as an objective function. To compute the likelihood of a character, Modified Quadratic Discriminant Function (MQDF) is used. The features used in the MQDF are mainly based on the directional features of the contour points of the components. We tested our system on 84 different Bangla city-names and 94.08% accuracy was obtained from the proposed system.

The goal of personal-style handwriting synthesis is to produce texts in the same style as an individual writer by analyzing the writer's samples of handwriting. The difficulty of handwriting synthesis is that the output should have the characteristics of the person's handwriting as well as looking natural, based on a limited number of available examples. We develop a synthesis algorithm which produces handwriting that exhibits naturalness based on the probabilistic character model.

A static dependency pair method, proposed by us, can effectively prove termination of simply-typed term rewriting systems (STRSs). The theoretical basis is given by the notion of strong computability. This method analyzes a static recursive structure based on definition dependency. By solving suitable constraints generated by the analysis result, we can prove the termination. Since this method is not applicable to every system, we proposed a class, namely, plain function-passing, as a restriction. In this paper, we first propose the class of safe function-passing, which relaxes the restriction by plain function-passing. To solve constraints, we often use the notion of reduction pairs, which is designed from a reduction order by the argument filtering method. Next, we improve the argument filtering method for STRSs. Our argument filtering method does not destroy type structure unlike the existing method for STRSs. Hence, our method can effectively apply reduction orders which make use of type information. To reduce constraints, the notion of usable rules is proposed. Finally, we enhance the effectiveness of reducing constraints by incorporating argument filtering into usable rules for STRSs.

In equational theorem proving, convergent term rewriting systems play a crucial role. In order to compute convergent term rewriting systems, the standard completion procedure (KB) was proposed by Knuth and Bendix and has been improved in various ways. The multi-completion system MKB developed by Kurihara and Kondo accepts as input a set of reduction orders in addition to equations and efficiently simulates parallel processes each of which executes the KB procedure with one of the given orderings. Wehrman and Stump also developed a new variant of completion procedure, constraint-based completion, in which reduction orders need not be given by using automated modern termination checkers. As a result, the constraint-based procedures simulate the execution of parallel KB processes in a sequential way, but naive search algorithms sometimes cause serious inefficiency when the number of the potential reduction orders is large. In this paper, we present a new procedure, called a constraint-based multi-completion procedure MKBcs, by augmenting the constraint-based completion with the framework of the multi-completion for suppressing the combinatorial explosion by sharing inferences among the processes. The existing constraint-based system SLOTHROP, which basically employs the best-first search, is more efficient when its built-in heuristics for process selection are appropriate, but when they are not, our system is more efficient. Therefore, both systems have their role to play.

Proofs written in algebraic specification languages are called proof scores. The proof score approach to design verification is attractive because it provides a flexible way to prove that designs for systems satisfy properties. Thus far, however, the approach has focused on safety properties. In this paper, we describe a way to verify that designs for systems satisfy liveness properties with the approach. A mutual exclusion protocol using a queue is used as an example. We describe the design verification and explain how it is verified that the protocol satisfies the lockout freedom property.

This paper describes a method for recognizing romanized Japanese words in learner English. They become noise and problematic in a variety of systems and tools for language learning and teaching including text analysis, spell checking, and grammatical error detection because they are Japanese words and thus mostly unknown to such systems and tools. A problem one encounters when recognizing romanized Japanese words in learner English is that the spelling rules of romanized Japanese words are often violated. To address this problem, the described method uses a clustering algorithm reinforced by a small set of rules. Experiments show that it achieves an F-measure of 0.879 and outperforms other methods. They also show that it only requires the target text and an English word list of reasonable size.

The photo-mask cost of standard-cell-based ASICs has been increased so prohibitively that low-volume production LSIs are difficult to fabricate due to high non-recurring engineering (NRE) cost including mask cost. Recently, user-programmable devices, such as FPGAs are started to be used for low-volume consumer products. However, FPGAs cannot be replaced for general purpose because of its lower speed-performance and higher power consumption. In this paper, we propose the user-programmable architecture called VPEX (Via Programmable logic device using EXclusive-or array), in which the hardware logic can be programmed by changing layout patterns on 2 via-layers. The logic element (LE) of VPEX consists of complex-gate-type EXclusive OR (EXOR) and Inverter (NOT) gates. The single LE can output 12 logics which include NOT, Buffer (BUF), all 2-inputs logic functions, 3-inputs AOI21 and inverted-output multiplexer (MUXI) by changing via-1 layout pattern. Furthermore, via-1 layout is optimized for high-throughput EB direct writing, so mask-less programming will be realized in VPEX. We compared the performance of area, speed, and power consumption of VPEX with that of standard-cell-based ASICs and FPGAs. As a result, the speed performance of VPEX was much better than FPGAs and about 1.3-1.6 times worse than standard-cells. We believe that the combination of VPEX architecture and EB direct writing is the best solution for low-volume production LSIs.

This paper describes a method of producing segmentation point candidates for on-line handwritten Japanese text by a support vector machine (SVM) to improve text recognition. This method extracts multi-dimensional features from on-line strokes of handwritten text and applies the SVM to the extracted features to produces segmentation point candidates. We incorporate the method into the segmentation by recognition scheme based on a stochastic model which evaluates the likelihood composed of character pattern structure, character segmentation, character recognition and context to finally determine segmentation points and recognize handwritten Japanese text. This paper also shows the details of generating segmentation point candidates in order to achieve high discrimination rate by finding the optimal combination of the segmentation threshold and the concatenation threshold. We compare the method for segmentation by the SVM with that by a neural network (NN) using the database HANDS-Kondate_t_bf-2001-11 and show the result that the method by the SVM bring about a better segmentation rate and character recognition rate.

There are two methods of writing servo signals with high speed in a perpendicular magnetic recording medium by magnetic duplication: bit printing (BP) and edge printing (EP). In this study, the influence of spacing between master and slave media on duplication characteristics in both BP and EP has been investigated by the three-dimensional finite-element method. The results show that the duplication characteristic in each method is deteriorated with a large spacing. Also, the influence of a small spacing is stronger in BP than in EP.

The completeness (i.e. confluent and terminating) property is an important concept when using a term rewriting system (TRS) as a computational model of functional programming languages. Knuth and Bendix have proposed a procedure known as the KB procedure for generating a complete TRS. A TRS cannot, however, directly handle higher-order functions that are widely used in functional programming languages. In this paper, we propose a higher-order KB procedure that extends the KB procedure to the framework of a simply-typed term rewriting system (STRS) as an extended TRS that can handle higher-order functions. We discuss the application of this higher-order KB procedure to a certification technique called inductionless induction used in program verification, and its application to fusion transformation, a typical kind of program transformation.

Writing/non-writing of composite conducting polymer (polypyrrole/poly(3-hexylthiophene)) have been investigated using composite conducting polymer. Writing has been made in two processes: pretreatment and dropping ethanol. The unipolar signal (10 Vp-p, 10 Hz+5 VDC) has worked as a circuit signal. The conductivity at the path of the composite conducting polymer network has depended on the passed signal. It was confirmed using the Y-type and H-type composite conducting polymer. It has been confirmed that rewriting of composite conducting polymer is possible to develop a memory or a neural network device of conducting polymer.

We propose a shot reduction technique of character projection (CP) Electron Beam Direct Writing (EBDW) using combined cell stencil (CCS) or the advanced process technology. CP EBDW is expected both to reduce mask costs and to realize quick turn around time. One of major issue of the conventional CP EBDW, however, is a throughput of lithography. The throughput is determined by numbers of shots, which are proportional to numbers of cell instances in LSIs. The conventional shot reduction techniques focus on optimization of cell stencil extraction, without any modifications on designed LSI mask patterns. The proposed technique employs the proposed combined cell stencil, with proposed modified design flow, for further shot reduction. We demonstrate 22.4% shot reduction within 4.3% area increase for a microprocessor and 28.6% shot reduction for IWLS benchmarks compared with the conventional technique.