Programming Languages and Automated Deduction
Associate Professor：HIROKAWA Nao
theory of computing
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
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.
- Nao Hirokawa and Georg Moser: Automated Complexity Analysis Based on the Dependency Pair Method. Proceedings of the 4th International Joint Conference on Automated Reasoning, LNAI 5195, pp. 364-379, 2008.
- Dominik Klein and Nao Hirokawa: Maximal Completion. Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, LIPIcs 10, pp. 71-80, 2011.
- 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.
Because background knowledges are not much required, this field would be suited for those who start new research in a graduate course. Although we need no broad knowledge of mathematics and computer science, concise understanding of mathematical notions is important. But don’t worry: Participating in weekly seminars and reading groups, you will eventually acquire necessary knowledges and formalization skills. Finally, there are several international competitions for automated deduction tools. Our group is encouraging our students to participate in such an event with their own tools.