Parallelization of Termination Checkers for Algebraic Software


  • Rui Ding
  • Haruhiko Sato
  • Masahito Kurihara



Termination Check, Algebraic Software, Term Rewriting System, Parallelization


Algebraic software is modeled as a set of equations representing its specification, and when each equation is directed either from left to right or from right to left, the resultant set of directed equations (or rewrite rules) is called a term rewriting system, which can be interpreted as a functional program executed by the pattern matching and term rewriting. In the field of formal verification of information systems, most of the properties of such a system are formalized as inductive theorems, which are equations over terms which hold on recursively-defined data structure such as natural numbers, lists and trees. Well-known as a method for inductive theorem proving is the Rewriting Induction (RI) proposed by Reddy. Recently, this method was extended by Sato and Kurihara to the Multi-context Rewriting Induction with termination checker (MRIt), which is a variant of RI to try to find a suitable context for induction automatically. However, MRIt should perform a large amount of termination checking of term rewriting systems, causing a significant efficiency bottleneck. In this paper, we propose a method of parallelizing the termination checkers used in MRIt to improve its efficiency by focusing on the well-known typical termination checking method based on the lexicographic path orders. For implementation, we used the functional concurrent programming language Erlang. We discuss the efficiency of our implementation based on the experiments with the standard set of termination problems.


Baader, F and Nipkow, T. Term Rewriting and All That, Cambrdge University Press, 1998.

Reddy, U. Term Rewriting Induction, Proc. of 10th International Conference on Automated Deduction, Lecture Notes in Computer Science, Vol. 449, pp. 162-177, 1990.

Aoto, T. Rewriting Induction Using Termination Checker, Proceedings of JSSST 24th Annual Conference, 3C-3, 2007.

Sato, H and Kurihara, M. Muti-Context Rewrting Induction with Termination checkers, IEICE Transactions on Information and Systems, vol. E93-D, no. 5, pp. 942-952, 2010.

Kurihara, M and Kondo, H. Completion for Multiple Reduction Orderings, Journal of Automated Reasoning, vol. 23, no. 1, pp. 25-42, 1999.

Arts, T and Giesl, J. Termination of Term Rewriting Using Dependency Pairs, Theoretical Computer Science, vol. 236, no. 1-2, pp. 133-178, 2000.

Armstrong, J. Programming Erlang: Software for a Concurrent World, Second Edition, Pragmatic Bookshelf, 2013.

Kurihara, M and Kondo, H. Efficient BDD Encodings for partial order constraints with application to expert systems in software verification, Proceedings of 17th International Conference on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems, Lecture Notes in Artificial Intelligence, vol. 3029, pp.827-837, 2004.

Hirokawa, N and Middeldorp, A. Tyrolean Termination Tool: Techniques and Features, Information and Computation, vol. 205, no. 4, pp. 474-511, 2007.




How to Cite

Ding, R., Sato, H., & Kurihara, M. (2014). Parallelization of Termination Checkers for Algebraic Software. Transactions on Engineering and Computing Sciences, 2(4), 102–114.