Relational Treatment of Term Graphs With Bound Variables

We show how and why it makes sense to use a relational formalisation instead of the usual functional one in the treatment of term graphs. Special attention is paid to term graphs with bound variables, that have, to our knowledge, never been formalised with such a generality before. Besides the novel treatment of term graphs themselves, we present an innovative relational homomorphism concept that for the first time allows to consider terms, resp. term trees as a special case of term graphs and still have the full power of (second-order) substitution available. Keywords: Term graph rewriting, relational matching, relation calculus, #-calculus 1 Introduction Term graphs have probably been introduced into the literature by Wadsworth [43], the inventor of graph reduction, which is an important implementation technique for functional programming languages. Since then, term graphs have been used as an e#cient implementation of terms, and various flavours of term graph rewriting have been in..