Relational Treatment of Term Graphs with Bound Variables

Wolfram Kahl

Logic Journal of the IGPL, Vol. 6 (1998), issue 2, pp. 259-303.



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.

This work is in continuation of [Kahl-1996] and [Kahl-1995a].

Wolfram Kahl