A Single-Step Term-Graph Reduction System for Proof Assistants

In this paper, we will define a custom term-graph reduction system for a simplified lazy functional language. Our custom system is geared towards flexibility, which is accomplished by leaving the choice of redex free and by making use of single-step reduction. It is therefore more suited for formal reasoning than the well-established standard reduction systems, which usually fix a single redex and realize multi-step reduction only. We will show that our custom 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. Sparkle is the dedicated proof assistant for Clean, a lazy functional programming language based on term-graph rewriting. An important reasoning step in Sparkle is the replacement of an expression with one of its reducts. The flexibility of our underlying reduction mechanism ensures that as many reductio...

• Type: Conference
• Year: 2007
• Where: AGTIVE
• Authors: Maarten de Mol, Marko C. J. D. van Eekelen, Rinus Plasmeijer
• Keywords: AGTIVE 2007, Custom Term-graph Reduction, Formal Languages, Lazy Functional Language, Reduction System