Language designers and implementors have avoided specifying and preserving the meaning of programs that produce errors. This is apparently because being forced to preserve error behavior limits severely the scope of program optimization, even for correct programs. However, error behavior preservation is desirable for debugging, and error behavior must be preserved in any language that permits user-generated errors (i.e., exceptions). This article presents a technique for expressing general program transformations for languages that possess a rich collection of distinguishable error values. This is accomplished by defining a higher-order function called Safe , which can be used to annotate those portions of a program that are guaranteed not to produce errors. It is shown that this facilitates the expression of very general program transformations, effectively giving program transformations in a language with many error values the same power and generality as program transformations in a language with only a single error value. Using the semantic properties of Safe , it is possible to provide some useful sufficient conditions for establishing the correctness of transformations in the presence of errors. In particular, a Substitutability theorem is proven, which can be used to justify “in-context” optimizations: transformations that alter the meanings of subexpressions without changing the meaning of the whole program. Finally, the effectiveness of the technique is demonstrated by some examples of its use in an optimizing compiler.

Language designers and implementors have avoided specifying and preserving the meaning of programs that produce errors. This is apparently because being forced to preserve error behavior severely limits the scope of program optimization, even for correct programs. However, preserving error behavior is desirable for debugging, and error behavior must be preserved in any language that permits user-generated exceptions.

This paper treats 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 be able to compute the correct meaning of all expressions, but not so many that the system of rules is inconsistent. A formal framework is developed in which to give a precise treatment of these completeness and soundness issues, which are then investigated in the context of an extended version of the functional programming language FP. The rewrite rules of FP are shown to be sound and complete with respect to three different notions of completeness. The latter half of the paper considers rewrite strategies. In order to implement a language based on rewrite rules, it does not suffice to know that there are “enough” rules in the language; a good strategy for determining the order in which to apply them is also needed. But what is “good”? Corresponding to each notion of completeness, there is a notion of a good rewrite strategy. These notions of goodness are examined and characterized, and examples of a number of natural good strategies are given. Although these results are presented in the context of FP, the techniques (some of which are nontrivial extensions of techniques first used in the context of λ-calculus) should apply well beyond the realm of FP rewriting systems.

The designers of (functional) programming languages are faced with two occasionally conflicting goals: programmer convenience and semantic simplicity. For example, it is convenient to treat I/O operations as primitive “functions” with side effects, but doing so destroys referential transparency.FL is a functional language that is designed to trade some of the semantic simplicity of a pure language for some of the convenience of a procedural language, by treating I/O operations as primitives with “side effects”, but by using a structuring technique that localizes the scope of those effects. In this way, surprisingly little of the semantic simplicity is lost, as can be seen by comparing the underlying algebraic laws of FL with those of its pure counterpart. FP.This paper describes that comparison and shows that, in fact, for programs involving I/O, the structures of the algebraic laws of the two languages are identical! It concludes by showing that this technique cannot be extended to allow assignment statements without incurring a massive loss in the expressiveness and simplicity of the underlying algebra.

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.

The development of the algebraic approach to reasoning about functional programs that was introduced by Backus in his Turing Award Lecture is furthered.Precise definitions for the foundations on which the algebra is based are given, and some new expansion theorems that broaden the class of functions for which this approach is applicable are proved.In particular, the class of "overruntolerant" forms, nonlinear forms that include some of the familiar divide-and-conquer program schemes, are defined; an expansion theorem for such forms is proved; and that theorem is used to show how to derive expansions for some programs deemed by nonlinear forms.

A bottom-up parsing technique which can make nonleftmost possible reductions in sentential forms is said to be noncanonical Nearly every existing parsing technique can be extended to a noncanonical method which operates on larger classes of grammars and languages than the original technique. Moreover, most of the resulting parsers run in time linearly proportional to the length of their input strings. Several such extensions are defined and analyzed from the points of view of both power and decidability. The results are presented in terms of a general bottom-up parsing model which yields a common decision procedure for testing membership in many of the existing and extended classes.