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. Key words: Term graph rewriting, relational matching, relation calculus, λ-calculus