Basic completion strategies as another application of the Maude strategy language

TL;DR

This paper discusses the Maude strategy language's design and demonstrates its application in modeling completion procedures as transition rules with control, enhancing the language's utility in rewriting logic applications.

Contribution

It introduces a new case study applying Maude strategies to completion procedures, illustrating their effectiveness in controlling rule application.

Findings

Successful modeling of completion procedures using Maude strategies

Enhanced understanding of strategy language capabilities

Potential for broader application in rewriting logic systems

Abstract

The two levels of data and actions on those data provided by the separation between equations and rules in rewriting logic are completed by a third level of strategies to control the application of those actions. This level is implemented on top of Maude as a strategy language, which has been successfully used in a wide range of applications. First we summarize the Maude strategy language design and review some of its applications; then, we describe a new case study, namely the description of completion procedures as transition rules + control, as proposed by Lescanne.