HORIP · Higher-Order Rewriting for Intensional Properties of Programs and Circuits

Higher-Order Rewriting for Intensional Properties of Programs and Circuits

"Computational complexity is the study of resources -- typically time and space -- needed to solve a problem. For example, the question whether a given string is a palindrome can be resolved in linear time, while the problem of finding the winning move in a chess position requires exponential time. Problems requiring certain resources are characterised into complexity classes. The best-known classes are PTIME (the decision problems which can be solved by algorithms running in polynomial time in the size of the input), PSPACE (the problems solvable by algorithms using only polynomial space), and NPTIME (the problems whose answer can be verified in polynomial time). However, it is not known whether these three classes are all distinct, or whether two (or all three) of them contain exactly the same problems. This is among the most prominent open problems in computer science, which has applications in many parts of CS. To improve the scientific understanding of these complexity classes (and hopefully resolve the equivalences), the area of ""implicit complexity"" seeks to identify classes of decision problems not by their resource use, but by their inclusion in certain logics. A landmark work defines ""cons-free"" (read-only) programs and characterises a range of complexity classes using restrictions on type order and recursion scheme; for example, PTIME consists of decision problems solvable by first-order cons-free programs, while PSPACE contains exactly those solvable by second-order tail-recursive cons-free programs. However, cons-free programs have thus far not been used to characterise non-deterministic classes such as NPTIME. The goal of this project was to use higher-order term rewriting systems as a tool to study program properties, with a particular focus on implicit complexity using cons-free term rewriting but with side work on compiler and program correctness. Term rewriting is a well-developed area of theoretical computer science, which provides a mathematically rigorous style of non-deterministic functional programming. As there are decades of scientific progress on a wide range of questions in rewriting which are closely related to questions arising in analysing programs and complexity, these fields clearly have something to offer each other. In particular, it was the hope that the native non-determinism of rewriting would aid in characterising the non-deterministic classes. However, the effect turned out to be quite different: non-determinism causes an explosion of expressiveness, leading to several new insights on the interplay of non-determinism and higher-order types, both in term rewriting and complexity. Aside from these main results, the project has contributed to a definition of complexity for conditional term rewriting and a methodology for proving equivalence of C-programs. "

Текст от CORDIS, на английски · Данни: CORDIS, © Европейски съюз