P-TAC is an intermediate-level language designed to capture the sharing of computation. It is a more suitable internal language for functional language compilers than the X-calculus or combinators, especially for compiler optimize, tions. Using P-TAC, a proof for the confluence of Id, a higher-order functional language augmented with I-structures? is given. Using the notion of observational congruence the correctness of some compiler optimizations is shown.

1 introduction

We present P-TAC (for P arallel Three Address Code), a simple and powerful declarative language, to study the confluence of the higher-level language Id and the correctness and confluence of the optimizations used in the Id-to-dataflowgraph compiler [16]. Id is a modern, higher-order, stronglytyped declarative language with J.-structures [I, 121, arrays whose elements get “refined’l during the course of computation [4]. I-structures have the flavor of variables in logic languages because it is possible to create an I-structure without giving a definition for each of its elemefits.(In a purely functional language a variable is given exactly one binding or definition at creation time.) All Id programs produce unique results, but a formal proof of the confluence of Id had eluded us until now.