DENOTATIONAL SEMANTICS AND REWRITE RULES FOR FP.

Abstract

We consider languages whose operational semantics is given by a set of rewrite rules. For such languages, it is important to be able to determine that there are enough rules to completely reduce all meaningful expressions, but not so many that the system of rules is inconsistent. We develop a formal framework in which to give a precise treatment of these soundness and completeness issues. We believe our approach to be novel in that we make heavy use of denotational semantics in our proof of completeness. The particular language for which we answer these questions is an extended version of the functional programming language FP; however the applicability of these techniques extends beyond the realm of FP rewriting systems.