Implementing β-Reduction by Hypergraph Rewriting
Sabine Kuske · Electronic Notes in Theoretical Computer Science · 1995
The aim of this paper is to implement the β-reduction in the lambda;-calculus with a hypergraph rewriting mechanism called collapsed lambda;-tree rewriting. It turns out that collapsed lambda;-tree rewriting is sound with respect to β-reduction and complete with respect to the Gross-Knuth strategy. As a consequence, there exists a normal form for a collapsed lambda;-tree if and only if there exists a normal form for the represented λ-term. I am grateful to Renate Klempien-Hinrichs, Detlef Plump, and to the referees for their helpful comments.