#	Pagina
attuale pagina	/open-h2020/projects/195559/results.html

Report

Teaser, summary, work performed and final results

Periodic Reporting for period 1 - HORIP (Higher-Order Rewriting for Intensional Properties of Programs and Circuits)

Teaser

Summary

\"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.
\"

Work performed

In the primary line of work, we have studied the expressive power of cons-free higher-order term rewriting systems with varying restrictions, but always allowing for non-deterministic choice. This has led to a range of new insights, some of them highly surprising. The key results:

* Cons-free first-order term rewriting, limited to Kth-order systems, characterises ETIME^K. In contrast, it was known that cons-free first-order functional programs of order K characterise EXPTIME^{K-1}. Thus, this characterisation of a new series of classes not covered by earlier work was quite unexpected, and provides interesting insights on the role of an evaluation strategy in the expressive power of a language.

* Cons-free first-order term rewriting with call-by-value evaluation characterises PTIME: essentially, if no functional data is considered, then non-determinism does not add any expressiveness. This is in line with earlier results on functional programming with a non-deterministic choice operator.

* Cons-free higher-order term rewriting with call-by-value revaluation characterises ELEMENTARY, for any type order above 1. Essentially, if even minimal functional data is considered, non-determinism allows for a construction that makes the expressiveness of cons-free term rewriting shoot up dramatically. This result, which extends to functional programming with a non-deterministic choice construction, is highly surprising: previously, it was assumed that -- like in the first order -- expressiveness would not be affected by merely adding non-deterministic choice. It also provides an exciting new view on the way non-determinism and higher types fit together which are likely to transfer to other approaches in implicit complexity, especially where higher-order logics are concerned.

Beyond this, we have developed more robust proof methods for reasoning about cons-free programs and term rewriting systems, demonstrated how cons-free term rewriting can provide a new diagonalisation-based proof that EXPTIME^K always differs from EXPTIME^{K+1}, and explored the expressive power of alternative changes such as product types and explicit lambda-abstraction.

In the secondary line of work, we have built on earlier studies to define a practically relevant notion of complexity for conditional term rewriting, along with transformation-based techniques to analyse this complexity. This can be used for the analysis of advanced declarative programming languages like Maude. We have also completed the theoretical basis to use term rewriting for equivalence analysis of imperative programs. Although this work only seeks to lay a foundation for such verification, it already provides enough proving power to handle equivalence problems beyond the previous state-of-the-art. We have also made alterations to the theoretical core of the HACS compiler generator, and discussed the consequences in a meeting with a mixture of people from business (primarily IBM and TwoSigma) and academia.

All results have been disseminated through multiple talks at workshops, conferences and seminars, as well as many personal discussions with other researchers in the field. Due to the highly theoretical nature of most of the work, communication within academia has been the primary form of dissemination.

Final results

As explained above, the project has progressed the state of the art in various directions. Most pertinently, the new results on the interplay of non-determinism and higher type orders are both highly unexpected, and likely to have significant repercussions in the field also where it concerns non-rewriting-related higher-order approaches to implicit complexity.

The project has also identified some errors in older (published) papers, and made significant (but yet unpublished) progress towards combining tail-recursion with cons-free term rewriting (for characterising the deterministic and non-deterministic SPACE complexity classes). Despite the project\'s ending, we are planning to also complete these lines of work.