Confluent Term--Graph Reduction for Computer--Aided Formal Reasoning
Maarten de Mol, M.C.J.D. van Eekelen, Rinus Plasmeijer · 2007
Abstract. Sparkle is the dedicated proof assistant for the lazy func-tional programming language Clean, which is based on term-graph rewriting. Because equational reasoning is an important proof technique, Sparkle needs to offer support for formally proving e1 = e2 in as many situations as possible. The base proof of equality is by means of reduc-tion: if e1 reduces to e2, then also e1 = e2. Therefore, the underlying reduction system of Sparkle needs to be geared towards flexibility, al-lowing reduction to take place as often as possible. In this paper, we will define a flexible term-graph reduction system for a simplified lazy functional language. Our system leaves the choice of redex free and uses single-step reduction. It is therefore more suited for formal reasoning than the well-established standard reduction systems for lazy functional languages, which usually fix a single redex and/or realize multi-step reduction only. We will show that our system is correct with respect to the standard systems, by proving that it is confluent and allows standard lazy functional evaluation as a possible reduction path. Our reduction system is used in the foundation of Sparkle. Because it is based on a simplified functional language, it can be applied to any other functional language based on term-graph rewriting as well. 1