Terms as DAGs

Last modified on

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:

lambda_term_1 (\x->(x,x))y Ap \x->(x,x) Lam (\x->(x,x))y->\x->(x,x) func y y (\x->(x,x))y->y arg x x \x->(x,x)->x arg (x,x) Ap \x->(x,x)->(x,x) body (x,x)->x arg (x,) Ap (x,x)->(x,) func (x,)->x arg (,) (,) (x,)->(,) func

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.