Here is a very interesting idea I saw in one paper on AI for theorem proving - representing lambda terms (or term in any other algebra) as a DAG with leaves *representing* names.

In untyped lambda calculus, `(\x -> (x, x)) y`

might be represented as a DAG like this:

Evaluation becomes just simple graph rewriting - if you see `Ap(Lam(f,x),y)`

anywhere in your graph, rewrite every reference to `x`

in `f`

to `y`

.