English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Zendy Open

Presents the pdf analysis as premium feature

PDF Analysis

Insights

Presents the summarisation as premium feature

Summarisation

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the zaia usage as premium feature

ZAIA

Zendy Tools

Zendy Plus

Presents the access of premium content as premium feature

Premium Content

In [24], a new size-change principle was proposed to verify termination of functional programs automatically. We extend this principle in order to prove termination and innermost termination of arbitrary term rewrite systems (TRSs). Moreover, we compare this approach with existing techniques for termination analysis of TRSs (such as recursive path orders or dependency pairs). It turns out that the size-change principle on its own fails for many examples that can be handled by standard techniques for rewriting, but there are also TRSs where it succeeds whereas existing rewriting techniques fail. Moreover, we also compare the complexity of the respective methods. To this end, we develop the first complexity analysis for the dependency pair approach. While the size-change principle is PSPACE-complete, we prove that the dependency pair approach (in combination with classical path orders) is only -complete. To benefit from their respective advantages, we show how to combine the size-change principle with classical orders and with dependency pairs. In this way, we obtain a new approach for automated termination proofs of TRSs which is more powerful than previous approaches. We also show that the combination with dependency pairs does not increase the complexity of the size-change principle, i.e., the combined approach is still PSPACE-complete.

The size-change principle and dependency pairs for termination of term rewriting