The 2D Dependency Pair Framework for Conditional Rewrite Systems—Part II: Advanced Processors and Implementation Techniques

Salvador Lucas, José Meseguer, Raúl Gutiérrez

Research output: Contribution to journalArticle

Abstract

Proving termination of programs in ‘real-life’ rewriting-based languages like CafeOBJ, Haskell, Maude, etc., is an important subject of research. To advance this goal, faithfully capturing the impact in the termination behavior of the main language features (e.g., conditions in program rules) is essential. In Part I of this work, we have introduced a 2D Dependency Pair Framework for automatically proving termination properties of Conditional Term Rewriting Systems. Our framework relies on the notion of processor as the main practical device to deal with proofs of termination properties of conditional rewrite systems. Processors are used to decompose and simplify the proofs in a divide and conquer approach. With the basic proof framework defined in Part I, here we introduce new processors to further improve the ability of the 2D Dependency Pair Framework to deal with proofs of termination properties of conditional rewrite systems. We also discuss relevant implementation techniques to use such processors in practice.

Original languageEnglish (US)
JournalJournal of Automated Reasoning
DOIs
StateAccepted/In press - Jan 1 2020

Keywords

  • Conditional term rewriting
  • Dependency pairs
  • Operational termination
  • Program analysis

ASJC Scopus subject areas

  • Software
  • Computational Theory and Mathematics
  • Artificial Intelligence

Cite this