Properties of a first-order functional language with sharing

AbstractA calculus and a model for a first-order functional language with sharing is presented. In most implementations of functional languages, argument subexpressions in a function application are shared to avoid their repeated evaluation. Recursive functions are typically implemented using graphs with cycles. Compilers for these languages sometimes employ non-left-linear and left-cyclic rules for optimizations. A graph rewriting system (GRS) to address these concerns is developed. It is shown that a GRS without interfering rules is confluent. Along the lines of Lévy's term model for the λ-calculus, a semantics of such a GRS is also presented. An application of the term model to compiler optimizations is discussed