Our goal is to develop a new and highly flexible approach to program optimization. Instead of applying rote, high-level transformations, we seek to derive optimizations automatically from broad and intuitive principles. Toward that end this paper presents a new formalism for first-order, purely functional programs, then uses the formalism to give a rigorous statement of a principle of optimization. The formalism occupies three levels. At the lowest level is the trace graph, a finite, graph-like structure that describes a single terminating path of execution through a functional program. At the middle level is the trace graph set, which describes a set of paths of execution; a certain kind of trace graph set, the executable set, describes the full set of paths for a single deterministic program. At the highest level is the trace grammar, a graph grammar that generates a trace graph set. While trace graph sets may be infinite, trace grammars are finite objects with a natural, subroutine-like recursive structure. We use the formalism to give a rigorous statement of a well-known principle of optimization, namely, that programs should not make any unnecessary computations. This principle is so obvious that it is often overlooked, but it underlies many common compiler optimizations and other, more exotic program transformations. Our formal statement of the principle unifies and illuminates many optimizing transformations. Our work in progress is the construction of an optimizer that derives optimizations directly from our formal principle. This paper concludes with an overview of this optimizer and some preliminary experimental results.