Order-Sorted Dependency Pairs

Author

Salvador Lucas and José Meseguer

Abstract

Types (or sorts) are pervasive in computer science and in rewriting-based programming languages, which often support subtypes (subsorts) and subtype polymorphism. Programs in these languages can be modeled as order-sorted term rewriting systems (OS-TRSs). Often, termination of such programs heavily depends on sort information. But few techniques are currently available for proving termination of OS-TRSs; and they often fail for interesting OS-TRSs. In this paper we generalize the dependency pairs approach to prove termination of OS-TRSs. Preliminary experiments suggest that this technique can succeed where existing ones fail, yielding easier and simpler termination proofs.

Keywords

Dependency pairs, program analysis, term rewriting, termination