A Correctness Proof for Combinator Reduction with Cycles
William M. Farmer, John D. Ramsdell, Ronald J. Watro
1990
Abstract
Turner popularized a technique of Wadsworth in which a cyclic graph
rewriting rule is used to implement reduction of the fixed point
combinator Y. We examine the theoretical foundation of this approach.
Previous work has concentrated on proving that graph methods are, in a
certain sense, sound and complete implementations of term methods.
This work is inapplicable to the cyclic Y-rule, which is unsound in
this sense since graph normal forms can exist without corresponding
term normal forms. We define and prove the correctness of combinator
head reduction using the cyclic Y-rule; the correctness of normal
reduction is an immediate consequence. Our proof avoids the use of
infinite trees to explain cyclic graphs. Instead, we show how to
consider reduction with cycles as an optimization of reduction without
cycles.