Exponential space means that memory use grows like an exponential function of input size. In term unification, a substitution can allocate O(2^n) objects when n holes expand through a binary structure, so a small-looking problem can produce a huge result. section 10.2
A binary-tree blow-up
Four holes produce 16 nodes; five, six, and seven holes produce 32, 64, and 128 nodes. The resulting substitution repeats large subterms, making both space and time exponential. section 10.2
Symbol Blah(BinTerm left, BinTerm right) =>
new("Blah", left, right);
Hole W = new ("W"), X = new("X"), Y = new("Y"), Z = new("Z");
var two = new Constant(2);
var term1 = Blah(W, Blah(X, Blah(Y, Blah(Z, two))));
var term2 = Blah(Blah(Blah(Blah(two, Z), Y), X), W);
var subst = term1.Unify(term2);
foreach (var hole in subst.Keys)
Console.WriteLine($"{hole.Name} -> {subst[hole]}");
Console.WriteLine(term1.Substitute(subst));
Run the unification example to inspect each hole’s substitution and the fully expanded term that triggers the allocation blow-up. section 10.2
Deduplicating immutable terms can convert the exponential-size graph into a linear-size graph, avoiding repeated structure rather than merely processing it faster. section 10.2
