Programming Languages and Automated Deduction

HIROKAWA Laboratory
Associate Professor：HIROKAWA Nao

E-mail：
［Research areas］
theory of computing
［Keywords］
term rewriting, symbolic computation, declarative programming, theorem proving

Skills and background we are looking for in prospective students

Knowledge of elementary set theory and/or programming skill is essential for starting research in this field. The introductory course I120 offers necessary knowledge for the former. If you like programming languages or mathematical puzzles, this research field would be fit for you.

What you can expect to learn in this laboratory

We aim to develop both mathematical ability and programing skill. Not only for scientific researchers but also for industrial engineers, the ability to understand mathematical descriptions is crucial for their job. Through research activities in our group, we foster reading and writing skills for mathematical formulas and abilities for program reasoning.

【Job category of graduates】IT and communications companies, research institutes

Research outline

Developing powerful computation/deduction mechanisms is key for software construction and verification. Our group is extensively working in the field of term rewriting, a powerful computation model based on equations. This model underlies various applications in computer science, such as logic and/or functional programming languages, automatic theorem provers, and computer algebra systems like Mathematica.

1. Automated Deduction

In science, equations are common tools for modeling physical/chemical phenomena and computer programs. We are attempting to develop powerful and efficient methods for proving and/or solving equations automatically.

■ Proving Equations
Rewriting terms along (valid) equations is the most basic operation in equational reasoning. If both sides of a given equality become the same term by rewriting, one can conclude that the equality holds. While this very simple method has been adopted as a main deduction mechanism in current theorem provers, still many problems remain to be solved. In particular, lemma discovery for inductive theorems, and automatic generation of counterexample and countermodel are important challenging topics.

■ Solving Equations
While linear equations on reals can be solved by the Gaussian elimination, in computer science we often need to deal with equations on terms and strings.
For instance, the string equation ax=bx admits an infinite number of solutions including (x, y) = (b, a), (aab, aaa). Fortunately, in this case the most general solution exists and we can represent it as (zb, az) with parameter z. We are investigating discrimination formulas and efficient algorithms to solve equations on various data structures.

2. Theory of Computing

■ Termination Analysis
From time to time, we witness that a program freezes or crashes due to a sudden memory exhaustion. In most cases, it is caused by unexpected non-termination of the program. We are investigating powerful but efficient methods for proving termination of programs automatically.

■ Complexity Analysis
Advancing the technology of termination analysis, we are also tackling with runtime complexity analysis of programs.

Key publications

1. Teppei Saito and Nao Hirokawa: Weighted Path Orders are Semantic Path Orders. Proceedings of the 14th International Symposium on Frontiers of Combining Systems, LNAI, pp. 63-80, 2023. Best paper award.
2. Dominik Klein and Nao Hirokawa: Maximal Completion. Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, LIPIcs 10, pp. 71-80, 2011.
3. Kiraku Shintani and Nao Hirokawa: Compositional Confluence Criteria. Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction, LIPIcs 228, pp. 28:1-28:19, 2022.