An algebraic approach to the compilation and operational semantics of functional languages with I-structures
Zena M. Ariola · 1992
Modern languages are too complex to be given direct operational semantics. For example, the operational semantics of functional languages has traditionally been given by translating them to the $\lambda$-calculus extended with constants. Compilers do a similar translation into an intermediate form in the process of generating code for a machine. A compiler then performs optimizations on this intermediate form before generating machine code. In this thesis we show that the intermediate form can actually be the kernel language. In fact, we may translate the kernel language into still lower-level language(s), where more machine oriented or efficiency related concerns can be expressed directly. Furthermore, compiler optimizations may be expressed as source-to-source transformations on the intermediate languages. We introduce two implicitly parallel languages, Kid (Kernel Id) and P-TAC (Parallel Three Address Code), respectively, and describe the compilation process of Id in terms of a translation of Id into Kid, and of Kid into P-TAC. In this thesis we do not describe the compilation process below the P-TAC level. However, we show that our compilation process allows the formalization of questions related to the correctness of the optimizations. We also give the operational semantics of Id indirectly by its translation into Kid and a well-defined operational semantics for Kid. Kid and P-TAC are examples of Graph Rewriting Systems (GRSs), which are introduced to capture sharing of computation precisely. Sharing of subexpressions is important both semantically (e.g., to model side-effects) and pragmatically (e.g., to reason about complexity). Our GRSs extend Barendregt's Term Graph Rewriting Systems to include cyclic graphs and cyclic rules. We present a term model for GRSs along the lines of Levy's term model for $\lambda$-calculus, and show its application to compiler optimizations. We also show that GRS reduction is a correct implementation of term rewriting.