Lazy Evaluation Schemes for Efficient Implementation of Multi-Context Algebraic Completion System

摘要/ABSTRACT

Lazy evaluation is a computational scheme which delays the evaluation of an expression until its value is needed, trying to improve the performance particularly when dealing with large data structure. In this paper, we apply this mechanism to a multi-context algebraic reasoning system which, on a large data structure called the nodes, efficiently simulates parallel processes each executing an algebraic reasoning procedure under a particular context (or a premise). In particular, the multi-completion system MKB simulates the parallel Knuth-Bendix completion procedures, which, given a set of equations and a set of reduction orderings, try to generate a complete (i.e., terminating and confluent) term rewriting system equivalent to the input equations. Exploiting the lazy evaluation, we present an efficient implementation of MKB, called lz-mkb, and implement it in a functional, object-oriented programming language Scala which features the lazy evaluation mechanism. The experiments with standard sample problems show that lz-mkb is more efficient than the original MKB implementation of Kurihara and Kondo.

作者/Authors

ChengCheng Ji, Masahito Kurihara, Haruhiko Sato

期刊信息/Information

IAENG International Journal of Computer Science, vol.42, no.3, pp. 282–287 (EI).

季承成 | CHENGCHENG JI