An Efficient Implementation of Multi-Context Algebraic Reasoning System with Lazy Evaluation

摘要/ABSTRACT

A multi-context algebraic reasoning system is a computational system which can efficiently simulate 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. MKB handles multiple contexts each corresponding to a reduction ordering, and normally, one of them leads to a success and others cause the failure or the divergence. In this study, we present an efficient implementation of MKB, called lz-mkb, which exploits the lazy evaluation mechanism of a functional, object-oriented programming language Scala. The experiment shows that lz-mkb is more efficient than the original MKB implementation of Kurihara and Kondo.

作者/Authors

ChengCheng Ji, Masahito Kurihara, Haruhiko Sato

会议信息/Information

Lecture Notes in Engineering and Computer Science: International MultiConference of Engineers and Computer Scientists 2015, HongKong, China, pp. 201–205 (EI).

季承成 | CHENGCHENG JI