About cookies on this site Our websites require some cookies to function properly (required). In addition, other cookies may be used with your consent to analyze site usage, improve the user experience and for advertising. For more information, please review your options. By visiting our website, you agree to our processing of information as described in IBM’sprivacy statement. To provide a smooth navigation, your cookie preferences will be shared across the IBM web domains listed here.
Publication
POPL 1984
Conference paper
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.