Correct and complete (positive) strategy annotations for OBJ

Authors

María Alpuente, Santiago Escobar, and Salvador Lucas

Abstract

Strategy annotations are used in several programming languages as replacement restrictions aimed at improving efficiency and/or reducing the risk of nontermination. Unfortunately, rewriting restrictions can have a negative impact on the ability to compute normal forms. In this paper, we first ascertain/clarify the conditions ensuring correctness and completeness (regarding normalization) of computing with strategy annotations. Then, we define a program transformation methodology for (correct and) complete evaluations which applies to OBJ-like languages.

Keywords

Declarative programming, OBJ, strategy annotations.