diff --git a/internal/unify/dot.go b/internal/unify/dot.go
index 143fa61..a26b9da 100644
--- a/internal/unify/dot.go
+++ b/internal/unify/dot.go
@@ -96,14 +96,15 @@
 	fmt.Fprintf(enc.w, "%s -> %s [label=%q];\n", from, to, l)
 }
 
-func (enc *dotEncoder) subgraph(v *Value) (vID, cID string) {
+func (enc *dotEncoder) valueSubgraph(v *Value) {
 	enc.valLimit = maxNodes
-	cID = enc.newID("cluster_%d")
+	cID := enc.newID("cluster_%d")
 	fmt.Fprintf(enc.w, "subgraph %s {\n", cID)
 	fmt.Fprintf(enc.w, "style=invis;")
-	vID = enc.value(v)
+	vID := enc.value(v)
 	fmt.Fprintf(enc.w, "}\n")
-	return
+	// We don't need the IDs right now.
+	_, _ = cID, vID
 }
 
 func (enc *dotEncoder) value(v *Value) string {
@@ -181,3 +182,40 @@
 		return enc.node(fmt.Sprintf("Var %s", enc.idp.unique(vd.id)), "")
 	}
 }
+
+func (enc *dotEncoder) envSubgraph(e nonDetEnv) {
+	enc.valLimit = maxNodes
+	cID := enc.newID("cluster_%d")
+	fmt.Fprintf(enc.w, "subgraph %s {\n", cID)
+	fmt.Fprintf(enc.w, "style=invis;")
+	vID := enc.env(e.root)
+	fmt.Fprintf(enc.w, "}\n")
+	_, _ = cID, vID
+}
+
+func (enc *dotEncoder) env(e *envExpr) string {
+	switch e.kind {
+	default:
+		panic("bad kind")
+	case envZero:
+		return enc.node("0", "")
+	case envUnit:
+		return enc.node("1", "")
+	case envBinding:
+		node := enc.node(fmt.Sprintf("%q :", enc.idp.unique(e.id)), "")
+		enc.edge(node, enc.value(e.val), "")
+		return node
+	case envProduct:
+		node := enc.node("⨯", "")
+		for _, op := range e.operands {
+			enc.edge(node, enc.env(op), "")
+		}
+		return node
+	case envSum:
+		node := enc.node("+", "")
+		for _, op := range e.operands {
+			enc.edge(node, enc.env(op), "")
+		}
+		return node
+	}
+}
diff --git a/internal/unify/env.go b/internal/unify/env.go
index 618887c..0f45af3 100644
--- a/internal/unify/env.go
+++ b/internal/unify/env.go
@@ -8,29 +8,36 @@
 	"fmt"
 	"iter"
 	"reflect"
-	"slices"
 	"strings"
 )
 
-// A nonDetEnv is a non-deterministic mapping from [ident]s to [Value]s.
+// A nonDetEnv is an immutable set of environments, where each environment is a
+// mapping from [ident]s to [Value]s.
 //
-// Logically, this is just a set of deterministic environments, where each
-// deterministic environment is a complete mapping from each [ident]s to exactly
-// one [Value]. In particular, [ident]s are NOT necessarily independent of each
-// other. For example, an environment may have both {x: 1, y: 1} and {x: 2, y:
-// 2}, but not {x: 1, y: 2}.
+// To keep this compact, we use an algebraic representation similar to
+// relational algebra. The atoms are zero, unit, or a singular binding:
 //
-// A nonDetEnv is immutable.
+// - A singular binding is an environment set consisting of a single environment
+// that binds a single ident to a single value.
 //
-// Often [ident]s are independent of each other, so the representation optimizes
-// for this by using a cross-product of environment factors, where each factor
-// is a sum of deterministic environments. These operations obey the usual
-// distributional laws, so we can always canonicalize into this form. (It MAY be
-// worthwhile to allow more general expressions of sums and products.)
+// - Zero is the empty set.
 //
-// For example, to represent {{x: 1, y: 1}, {x: 2, y: 2}}, in which the
-// variables x and y are dependent, we need a single factor that covers x and y
-// and consists of two terms: {x: 1, y: 1} + {x: 2, y: 2}.
+// - Unit is an environment set consisting of a single, empty environment (no
+// bindings).
+//
+// From these, we build up more complex sets of environments using sums and
+// cross products:
+//
+// - A sum is simply the union of the two environment sets.
+//
+// - A cross product is the Cartesian product of the two environment sets,
+// followed by combining each pair of environments. Combining simply merges the
+// two mappings, but fails if the mappings overlap.
+//
+// For example, to represent {{x: 1, y: 1}, {x: 2, y: 2}}, we build the two
+// environments and sum them:
+//
+//	({x: 1} ⨯ {y: 1}) + ({x: 2} ⨯ {y: 2})
 //
 // If we add a third variable z that can be 1 or 2, independent of x and y, we
 // get four logical environments:
@@ -40,43 +47,59 @@
 //	{x: 1, y: 1, z: 2}
 //	{x: 2, y: 2, z: 2}
 //
-// This could be represented as a single factor that is the sum of these four
-// detEnvs, but because z is independent, it can be a separate factor. Hence,
-// the most compact representation of this environment is:
+// This could be represented as a sum of all four environments, but because z is
+// independent, we can use a more compact representation:
 //
-//	({x: 1, y: 1} + {x: 2, y: 2}) ⨯ ({z: 1} + {z: 2})
+//	(({x: 1} ⨯ {y: 1}) + ({x: 2} ⨯ {y: 2})) ⨯ ({z: 1} + {z: 2})
 //
-// That is, two factors, where each is the sum of two terms.
+// Environment sets obey commutative algebra rules:
+//
+//	e + 0 = e
+//	e ⨯ 0 = 0
+//	e ⨯ 1 =
+//	e + f = f + e
+//	e ⨯ f = f ⨯ e
 type nonDetEnv struct {
-	// factors is a list of the multiplicative factors in this environment. The
-	// set of deterministic environments is the cross-product of these factors.
-	// All factors must have disjoint variables.
-	factors []*envSum
+	root *envExpr
 }
 
-// envSum is a sum of deterministic environments, all with the same set of
-// variables.
-type envSum struct {
-	ids   []*ident // TODO: Do we ever use this as a slice? Should it be a map?
-	terms []detEnv
+type envExpr struct {
+	// TODO: A tree-based data structure for this may not be ideal, since it
+	// involves a lot of walking to find things and we often have to do deep
+	// rewrites anyway for partitioning. Would some flattened array-style
+	// representation be better, possibly combined with an index of ident uses?
+	// We could even combine that with an immutable array abstraction (ala
+	// Clojure) that could enable more efficient construction operations.
+
+	kind envExprKind
+
+	// For envBinding
+	id  *ident
+	val *Value
+
+	// For sum or product. Len must be >= 2 and none of the elements can have
+	// the same kind as this node.
+	operands []*envExpr
 }
 
-type detEnv struct {
-	vals []*Value // Indexes correspond to envSum.ids
-}
+type envExprKind byte
+
+const (
+	envZero envExprKind = iota
+	envUnit
+	envProduct
+	envSum
+	envBinding
+)
 
 var (
-	// zeroEnvFactor is the "0" value of an [envSum]. It's a a factor with no
-	// sum terms. This is easiest to think of as: an empty sum must be the
-	// additive identity, 0.
-	zeroEnvFactor = &envSum{}
+	// topEnv is the unit value (multiplicative identity) of a [nonDetEnv].
+	topEnv = nonDetEnv{envExprUnit}
+	// bottomEnv is the zero value (additive identity) of a [nonDetEnv].
+	bottomEnv = nonDetEnv{envExprZero}
 
-	// topEnv is the algebraic one value of a [nonDetEnv]. It has no factors
-	// because the product of no factors is the multiplicative identity.
-	topEnv = nonDetEnv{}
-	// bottomEnv is the algebraic zero value of a [nonDetEnv]. The product of
-	// bottomEnv with x is bottomEnv, and the sum of bottomEnv with y is y.
-	bottomEnv = nonDetEnv{factors: []*envSum{zeroEnvFactor}}
+	envExprZero = &envExpr{kind: envZero}
+	envExprUnit = &envExpr{kind: envUnit}
 )
 
 // bind binds id to each of vals in e.
@@ -90,232 +113,132 @@
 		return bottomEnv
 	}
 
-	// TODO: If any of vals are _, should we just not do anything? We're kind of
+	// TODO: If any of vals are _, should we just drop that val? We're kind of
 	// inconsistent about whether an id missing from e means id is invalid or
 	// means id is _.
 
 	// Check that id isn't present in e.
-	for _, f := range e.factors {
-		if slices.Contains(f.ids, id) {
-			panic("id " + id.name + " already present in environment")
-		}
+	for range e.root.bindings(id) {
+		panic("id " + id.name + " already present in environment")
 	}
 
-	// Create the new sum term.
-	sum := &envSum{ids: []*ident{id}}
+	// Create a sum of all the values.
+	bindings := make([]*envExpr, 0, 1)
 	for _, val := range vals {
-		sum.terms = append(sum.terms, detEnv{vals: []*Value{val}})
+		bindings = append(bindings, &envExpr{kind: envBinding, id: id, val: val})
 	}
+
 	// Multiply it in.
-	factors := append(e.factors[:len(e.factors):len(e.factors)], sum)
-	return nonDetEnv{factors}
+	return nonDetEnv{newEnvExprProduct(e.root, newEnvExprSum(bindings...))}
 }
 
 func (e nonDetEnv) isBottom() bool {
-	if len(e.factors) == 0 {
-		// This is top.
-		return false
-	}
-	return len(e.factors[0].terms) == 0
+	return e.root.kind == envZero
 }
 
-func (e nonDetEnv) vars() iter.Seq[*ident] {
-	return func(yield func(*ident) bool) {
-		for _, t := range e.factors {
-			for _, id := range t.ids {
-				if !yield(id) {
-					return
+// bindings yields all [envBinding] nodes in e with the given id. If id is nil,
+// it yields all binding nodes.
+func (e *envExpr) bindings(id *ident) iter.Seq[*envExpr] {
+	// This is just a pre-order walk and it happens this is the only thing we
+	// need a pre-order walk for.
+	return func(yield func(*envExpr) bool) {
+		var rec func(e *envExpr) bool
+		rec = func(e *envExpr) bool {
+			if e.kind == envBinding && (id == nil || e.id == id) {
+				if !yield(e) {
+					return false
 				}
 			}
-		}
-	}
-}
-
-// all enumerates all deterministic environments in e.
-//
-// The result slice is in the same order as the slice returned by
-// [nonDetEnv2.vars]. The slice is reused between iterations.
-func (e nonDetEnv) all() iter.Seq[[]*Value] {
-	return func(yield func([]*Value) bool) {
-		var vals []*Value
-		var walk func(int) bool
-		walk = func(i int) bool {
-			if i == len(e.factors) {
-				return yield(vals)
-			}
-			start := len(vals)
-			for _, term := range e.factors[i].terms {
-				vals = append(vals[:start], term.vals...)
-				if !walk(i + 1) {
+			for _, o := range e.operands {
+				if !rec(o) {
 					return false
 				}
 			}
 			return true
 		}
-		walk(0)
+		rec(e)
 	}
 }
 
-// allOrdered is like all, but idOrder controls the order of the values in the
-// resulting slice. Any [ident]s in idOrder that are missing from e are set to
-// topValue. The values of idOrder must be a bijection with [0, n).
-func (e nonDetEnv) allOrdered(idOrder map[*ident]int) iter.Seq[[]*Value] {
-	valsLen := 0
-	for _, idx := range idOrder {
-		valsLen = max(valsLen, idx+1)
+// newEnvExprProduct constructs a product node from exprs, performing
+// simplifications. It does NOT check that bindings are disjoint.
+func newEnvExprProduct(exprs ...*envExpr) *envExpr {
+	factors := make([]*envExpr, 0, 2)
+	for _, expr := range exprs {
+		switch expr.kind {
+		case envZero:
+			return envExprZero
+		case envUnit:
+			// No effect on product
+		case envProduct:
+			factors = append(factors, expr.operands...)
+		default:
+			factors = append(factors, expr)
+		}
 	}
 
-	return func(yield func([]*Value) bool) {
-		vals := make([]*Value, valsLen)
-		// e may not have all of the IDs in idOrder. Make sure any missing
-		// values are top.
-		for i := range vals {
-			vals[i] = topValue
-		}
-		var walk func(int) bool
-		walk = func(i int) bool {
-			if i == len(e.factors) {
-				return yield(vals)
-			}
-			for _, term := range e.factors[i].terms {
-				for j, id := range e.factors[i].ids {
-					vals[idOrder[id]] = term.vals[j]
-				}
-				if !walk(i + 1) {
-					return false
-				}
-			}
-			return true
-		}
-		walk(0)
+	if len(factors) == 0 {
+		return envExprUnit
+	} else if len(factors) == 1 {
+		return factors[0]
 	}
+	return &envExpr{kind: envProduct, operands: factors}
 }
 
-func crossEnvs(envs ...nonDetEnv) nonDetEnv {
-	// Combine the factors of envs
-	var factors []*envSum
-	haveIDs := map[*ident]struct{}{}
-	for _, e := range envs {
-		if e.isBottom() {
-			// The environment is bottom, so the whole product goes to
-			// bottom.
-			return bottomEnv
-		}
-		// Check that all ids are disjoint.
-		for _, f := range e.factors {
-			for _, id := range f.ids {
-				if _, ok := haveIDs[id]; ok {
-					panic("conflict on " + id.name)
+// newEnvExprSum constructs a sum node from exprs, performing simplifications.
+func newEnvExprSum(exprs ...*envExpr) *envExpr {
+	// TODO: If all of envs are products (or bindings), factor any common terms.
+	// E.g., x * y + x * z ==> x * (y + z). This is easy to do for binding
+	// terms, but harder to do for more general terms.
+
+	var have smallSet[*envExpr]
+	terms := make([]*envExpr, 0, 2)
+	for _, expr := range exprs {
+		switch expr.kind {
+		case envZero:
+			// No effect on sum
+		case envSum:
+			for _, expr1 := range expr.operands {
+				if have.Add(expr1) {
+					terms = append(terms, expr1)
 				}
-				haveIDs[id] = struct{}{}
+			}
+		default:
+			if have.Add(expr) {
+				terms = append(terms, expr)
 			}
 		}
-		// Everything checks out. Multiply the factors.
-		factors = append(factors, e.factors...)
 	}
-	return nonDetEnv{factors: factors}
+
+	if len(terms) == 0 {
+		return envExprZero
+	} else if len(terms) == 1 {
+		return terms[0]
+	}
+	return &envExpr{kind: envSum, operands: terms}
+}
+
+func crossEnvs(env1, env2 nonDetEnv) nonDetEnv {
+	// Confirm that envs have disjoint idents.
+	var ids1 smallSet[*ident]
+	for e := range env1.root.bindings(nil) {
+		ids1.Add(e.id)
+	}
+	for e := range env2.root.bindings(nil) {
+		if ids1.Has(e.id) {
+			panic(fmt.Sprintf("%s bound on both sides of cross-product", e.id.name))
+		}
+	}
+
+	return nonDetEnv{newEnvExprProduct(env1.root, env2.root)}
 }
 
 func sumEnvs(envs ...nonDetEnv) nonDetEnv {
-	// nonDetEnv is a product at the top level, so we implement summation using
-	// the distributive law. We also use associativity to keep as many top-level
-	// factors as we can, since those are what keep the environment compact.
-	//
-	// a * b * c + a * d         (where a, b, c, and d are factors)
-	//                           (combine common factors)
-	//   = a * (b * c + d)
-	//                           (expand factors into their sum terms)
-	//   = a * ((b_1 + b_2 + ...) * (c_1 + c_2 + ...) + d)
-	//                           (where b_i and c_i are deterministic environments)
-	//                           (FOIL)
-	//   = a * (b_1 * c_1 + b_1 * c_2 + b_2 * c_1 + b_2 * c2 + d)
-	//                           (all factors are now in canonical form)
-	//   = a * e
-	//
-	// The product of two deterministic environments is a deterministic
-	// environment, and the sum of deterministic environments is a factor, so
-	// this process results in the canonical product-of-sums form.
-	//
-	// TODO: This is a bit of a one-way process. We could try to factor the
-	// environment to reduce the number of sums. I'm not sure how to do this
-	// efficiently. It might be possible to guide it by gathering the
-	// distributions of each ID's bindings. E.g., if there are 12 deterministic
-	// environments in a sum and $x is bound to 4 different values, each 3
-	// times, then it *might* be possible to factor out $x into a 4-way sum of
-	// its own.
-
-	factors, toSum := commonFactors(envs)
-
-	if len(toSum) > 0 {
-		// Collect all IDs into a single order.
-		var ids []*ident
-		idOrder := make(map[*ident]int)
-		for _, e := range toSum {
-			for v := range e.vars() {
-				if _, ok := idOrder[v]; !ok {
-					idOrder[v] = len(ids)
-					ids = append(ids, v)
-				}
-			}
-		}
-
-		// Flatten out each term in the sum.
-		var summands []detEnv
-		for _, env := range toSum {
-			for vals := range env.allOrdered(idOrder) {
-				summands = append(summands, detEnv{vals: slices.Clone(vals)})
-			}
-		}
-		factors = append(factors, &envSum{ids: ids, terms: summands})
+	exprs := make([]*envExpr, len(envs))
+	for i := range envs {
+		exprs[i] = envs[i].root
 	}
-
-	return nonDetEnv{factors: factors}
-}
-
-// commonFactors finds common factors that can be factored out of a summation of
-// [nonDetEnv]s.
-func commonFactors(envs []nonDetEnv) (common []*envSum, toSum []nonDetEnv) {
-	// Drop any bottom environments. They don't contribute to the sum and they
-	// would complicate some logic below.
-	envs = slices.DeleteFunc(envs, func(e nonDetEnv) bool {
-		return e.isBottom()
-	})
-	if len(envs) == 0 {
-		return bottomEnv.factors, nil
-	}
-
-	// It's very common that the exact same factor will appear across all envs.
-	// Keep those factored out.
-	//
-	// TODO: Is it also common to have vars that are bound to the same value
-	// across all envs? If so, we could also factor those into common terms.
-	counts := map[*envSum]int{}
-	for _, e := range envs {
-		for _, f := range e.factors {
-			counts[f]++
-		}
-	}
-	for _, f := range envs[0].factors {
-		if counts[f] == len(envs) {
-			// Common factor
-			common = append(common, f)
-		}
-	}
-
-	// Any other factors need to be multiplied out.
-	for _, env := range envs {
-		var newFactors []*envSum
-		for _, f := range env.factors {
-			if counts[f] != len(envs) {
-				newFactors = append(newFactors, f)
-			}
-		}
-		if len(newFactors) > 0 {
-			toSum = append(toSum, nonDetEnv{factors: newFactors})
-		}
-	}
-
-	return common, toSum
+	return nonDetEnv{newEnvExprSum(exprs...)}
 }
 
 // envPartition is a subset of an env where id is bound to value in all
@@ -326,69 +249,125 @@
 	env   nonDetEnv
 }
 
+// partitionBy splits e by distinct bindings of id and removes id from each
+// partition.
+//
+// If there are environments in e where id is not bound, they will not be
+// reflected in any partition.
+//
+// It panics if e is bottom, since attempting to partition an empty environment
+// set almost certainly indicates a bug.
 func (e nonDetEnv) partitionBy(id *ident) []envPartition {
 	if e.isBottom() {
-		// Bottom contains all variables
-		return []envPartition{{id: id, value: bottomValue, env: e}}
+		// We could return zero partitions, but getting here at all almost
+		// certainly indicates a bug.
+		panic("cannot partition empty environment set")
 	}
 
-	// Find the factor containing id and id's index in that factor.
-	idFactor, idIndex := -1, -1
-	var newIDs []*ident
-	for factI, fact := range e.factors {
-		idI := slices.Index(fact.ids, id)
-		if idI < 0 {
-			continue
-		} else if idFactor != -1 {
-			panic("multiple factors containing id " + id.name)
-		} else {
-			idFactor, idIndex = factI, idI
-			// Drop id from this factor's IDs
-			newIDs = without(fact.ids, idI)
-		}
-	}
-	if idFactor == -1 {
-		panic("id " + id.name + " not found in environment")
-	}
-
-	// If id is the only term in its factor, then dropping it is equivalent to
-	// making the factor be the unit value, so we can just drop the factor. (And
-	// if this is the only factor, we'll arrive at [topEnv], which is exactly
-	// what we want!). In this case we can use the same nonDetEnv in all of the
-	// partitions.
-	isUnit := len(newIDs) == 0
-	var unitFactors []*envSum
-	if isUnit {
-		unitFactors = without(e.factors, idFactor)
-	}
-
-	// Create a partition for each distinct value of id.
+	// Emit a partition for each value of id.
+	var seen smallSet[*Value]
 	var parts []envPartition
-	partIndex := map[*Value]int{}
-	for _, det := range e.factors[idFactor].terms {
-		val := det.vals[idIndex]
-		i, ok := partIndex[val]
-		if !ok {
-			i = len(parts)
-			var factors []*envSum
-			if isUnit {
-				factors = unitFactors
-			} else {
-				// Copy all other factor
-				factors = slices.Clone(e.factors)
-				factors[idFactor] = &envSum{ids: newIDs}
-			}
-			parts = append(parts, envPartition{id: id, value: val, env: nonDetEnv{factors: factors}})
-			partIndex[val] = i
+	for n := range e.root.bindings(id) {
+		if !seen.Add(n.val) {
+			// Already emitted a partition for this value.
+			continue
 		}
 
-		if !isUnit {
-			factor := parts[i].env.factors[idFactor]
-			newVals := without(det.vals, idIndex)
-			factor.terms = append(factor.terms, detEnv{vals: newVals})
+		parts = append(parts, envPartition{
+			id:    id,
+			value: n.val,
+			env:   nonDetEnv{e.root.substitute(id, n.val)},
+		})
+	}
+
+	return parts
+}
+
+// substitute replaces bindings of id to val with 1 and bindings of id to any
+// other value with 0 and simplifies the result.
+func (e *envExpr) substitute(id *ident, val *Value) *envExpr {
+	switch e.kind {
+	default:
+		panic("bad kind")
+
+	case envZero, envUnit:
+		return e
+
+	case envBinding:
+		if e.id != id {
+			return e
+		} else if e.val != val {
+			return envExprZero
+		} else {
+			return envExprUnit
+		}
+
+	case envProduct, envSum:
+		// Substitute each operand. Sometimes, this won't change anything, so we
+		// build the new operands list lazily.
+		var nOperands []*envExpr
+		for i, op := range e.operands {
+			nOp := op.substitute(id, val)
+			if nOperands == nil && op != nOp {
+				// Operand diverged; initialize nOperands.
+				nOperands = make([]*envExpr, 0, len(e.operands))
+				nOperands = append(nOperands, e.operands[:i]...)
+			}
+			if nOperands != nil {
+				nOperands = append(nOperands, nOp)
+			}
+		}
+		if nOperands == nil {
+			// Nothing changed.
+			return e
+		}
+		if e.kind == envProduct {
+			return newEnvExprProduct(nOperands...)
+		} else {
+			return newEnvExprSum(nOperands...)
 		}
 	}
-	return parts
+}
+
+// A smallSet is a set optimized for stack allocation when small.
+type smallSet[T comparable] struct {
+	array [32]T
+	n     int
+
+	m map[T]struct{}
+}
+
+// Has returns whether val is in set.
+func (s *smallSet[T]) Has(val T) bool {
+	arr := s.array[:s.n]
+	for i := range arr {
+		if arr[i] == val {
+			return true
+		}
+	}
+	_, ok := s.m[val]
+	return ok
+}
+
+// Add adds val to the set and returns true if it was added (not already
+// present).
+func (s *smallSet[T]) Add(val T) bool {
+	// Test for presence.
+	if s.Has(val) {
+		return false
+	}
+
+	// Add it
+	if s.n < len(s.array) {
+		s.array[s.n] = val
+		s.n++
+	} else {
+		if s.m == nil {
+			s.m = make(map[T]struct{})
+		}
+		s.m[val] = struct{}{}
+	}
+	return true
 }
 
 type ident struct {
@@ -494,7 +473,3 @@
 	}
 	return fmt.Sprintf("[%s]", strings.Join(strs, ", "))
 }
-
-func without[Elt any](s []Elt, i int) []Elt {
-	return append(s[:i:i], s[i+1:]...)
-}
diff --git a/internal/unify/html.go b/internal/unify/html.go
index d2434fe..d59bd8f 100644
--- a/internal/unify/html.go
+++ b/internal/unify/html.go
@@ -52,7 +52,7 @@
 type htmlTracer struct {
 	w    io.Writer
 	dot  *dotEncoder
-	svgs map[*Value]string
+	svgs map[any]string
 }
 
 func (t *htmlTracer) writeTree(node *traceTree) {
@@ -91,19 +91,19 @@
 	}
 }
 
-func (t *htmlTracer) svg(v *Value) string {
-	if s, ok := t.svgs[v]; ok {
+func htmlSVG[Key comparable](t *htmlTracer, f func(Key), arg Key) string {
+	if s, ok := t.svgs[arg]; ok {
 		return s
 	}
 	var buf strings.Builder
-	t.dot.subgraph(v)
+	f(arg)
 	t.dot.writeSvg(&buf)
 	t.dot.clear()
 	svg := buf.String()
 	if t.svgs == nil {
-		t.svgs = make(map[*Value]string)
+		t.svgs = make(map[any]string)
 	}
-	t.svgs[v] = svg
+	t.svgs[arg] = svg
 	buf.Reset()
 	return svg
 }
@@ -112,79 +112,12 @@
 	fmt.Fprintf(t.w, `<div class="unify">`)
 	for i, v := range vs {
 		fmt.Fprintf(t.w, `<div class="header" style="grid-column: %d">%s</div>`, i+1, html.EscapeString(labels[i]))
-		fmt.Fprintf(t.w, `<div style="grid-area: 2 / %d">%s</div>`, i+1, t.svg(v))
+		fmt.Fprintf(t.w, `<div style="grid-area: 2 / %d">%s</div>`, i+1, htmlSVG(t, t.dot.valueSubgraph, v))
 	}
+	col := len(vs)
 
-	t.emitEnv(env, len(vs))
+	fmt.Fprintf(t.w, `<div class="header" style="grid-column: %d">in</div>`, col+1)
+	fmt.Fprintf(t.w, `<div style="grid-area: 2 / %d">%s</div>`, col+1, htmlSVG(t, t.dot.envSubgraph, env))
 
 	fmt.Fprintf(t.w, `</div>`)
 }
-
-func (t *htmlTracer) emitEnv(env nonDetEnv, colStart int) {
-	if env.isBottom() {
-		fmt.Fprintf(t.w, `<div class="header" style="grid-column: %d">_|_</div>`, colStart+1)
-		return
-	}
-
-	colLimit := 10
-	col := colStart
-	for i, f := range env.factors {
-		if i > 0 {
-			// Print * between each factor.
-			fmt.Fprintf(t.w, `<div class="header" style="grid-column: %d">&times;</div>`, col+1)
-			col++
-		}
-
-		var idCols []int
-		for i, id := range f.ids {
-			var str string
-			if i == 0 && len(f.ids) > 1 {
-				str = "("
-			}
-			if colLimit <= 0 {
-				str += "..."
-			} else {
-				str += html.EscapeString(t.dot.idp.unique(id))
-			}
-			if (i == len(f.ids)-1 || colLimit <= 0) && len(f.ids) > 1 {
-				str += ")"
-			}
-
-			fmt.Fprintf(t.w, `<div class="header" style="grid-column: %d">%s</div>`, col+1, str)
-			idCols = append(idCols, col)
-
-			col++
-			if colLimit <= 0 {
-				break
-			}
-			colLimit--
-		}
-
-		fmt.Fprintf(t.w, `<div class="envFactor" style="grid-area: 2 / %d / 3 / %d">`, idCols[0]+1, col+1)
-		rowLimit := 10
-		row := 0
-		for _, term := range f.terms {
-			// TODO: Print + between rows? With some horizontal something to
-			// make it clear what it applies across?
-
-			for i, val := range term.vals {
-				fmt.Fprintf(t.w, `<div style="grid-area: %d / %d">`, row+1, idCols[i]-idCols[0]+1)
-				if i < len(term.vals)-1 && i == len(idCols)-1 {
-					fmt.Fprintf(t.w, `...</div>`)
-					break
-				} else if rowLimit <= 0 {
-					fmt.Fprintf(t.w, `...</div>`)
-				} else {
-					fmt.Fprintf(t.w, `%s</div>`, t.svg(val))
-				}
-			}
-
-			row++
-			if rowLimit <= 0 {
-				break
-			}
-			rowLimit--
-		}
-		fmt.Fprintf(t.w, `</div>`)
-	}
-}
diff --git a/internal/unify/testdata/stress.yaml b/internal/unify/testdata/stress.yaml
new file mode 100644
index 0000000..e447853
--- /dev/null
+++ b/internal/unify/testdata/stress.yaml
@@ -0,0 +1,33 @@
+# In the original representation of environments, this caused an exponential
+# blowup in time and allocation. With that representation, this took about 20
+# seconds on my laptop and had a max RSS of ~12 GB. Big enough to be really
+# noticeable, but not so big it's likely to crash a developer machine. With the
+# better environment representation, it runs almost instantly and has an RSS of
+# ~90 MB.
+unify:
+- !sum
+  - !sum [1, 2]
+  - !sum [3, 4]
+  - !sum [5, 6]
+  - !sum [7, 8]
+  - !sum [9, 10]
+  - !sum [11, 12]
+  - !sum [13, 14]
+  - !sum [15, 16]
+  - !sum [17, 18]
+  - !sum [19, 20]
+  - !sum [21, 22]
+- !sum
+  - !sum [1, 2]
+  - !sum [3, 4]
+  - !sum [5, 6]
+  - !sum [7, 8]
+  - !sum [9, 10]
+  - !sum [11, 12]
+  - !sum [13, 14]
+  - !sum [15, 16]
+  - !sum [17, 18]
+  - !sum [19, 20]
+  - !sum [21, 22]
+all:
+  [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22]
diff --git a/internal/unify/yaml.go b/internal/unify/yaml.go
index 1b1c813..ff5115f 100644
--- a/internal/unify/yaml.go
+++ b/internal/unify/yaml.go
@@ -93,7 +93,7 @@
 }
 
 func (c *Closure) unmarshal(node *yaml.Node, opts UnmarshalOpts) error {
-	dec := &yamlDecoder{opts: opts, vars: make(map[string]*ident)}
+	dec := &yamlDecoder{opts: opts, vars: make(map[string]*ident), env: topEnv}
 	val, err := dec.value(node)
 	if err != nil {
 		return err
@@ -349,25 +349,35 @@
 }
 
 func (enc *yamlEncoder) env(e nonDetEnv) *yaml.Node {
-	var n yaml.Node
-	n.Kind = yaml.SequenceNode
-	n.Tag = "!env"
-	for _, term := range e.factors {
-		var nTerm yaml.Node
-		n.Content = append(n.Content, &nTerm)
-		nTerm.Kind = yaml.SequenceNode
-		for _, det := range term.terms {
-			var nDet yaml.Node
-			nTerm.Content = append(nTerm.Content, &nDet)
-			nDet.Kind = yaml.MappingNode
-			for i, val := range det.vals {
-				var nLabel yaml.Node
-				nLabel.SetString(enc.idp.unique(term.ids[i]))
-				nDet.Content = append(nDet.Content, &nLabel, enc.value(val))
+	var encode func(e *envExpr) *yaml.Node
+	encode = func(e *envExpr) *yaml.Node {
+		var n yaml.Node
+		switch e.kind {
+		default:
+			panic("bad kind")
+		case envZero:
+			n.SetString("0")
+		case envUnit:
+			n.SetString("1")
+		case envBinding:
+			var id yaml.Node
+			id.SetString(enc.idp.unique(e.id))
+			n.Kind = yaml.MappingNode
+			n.Content = []*yaml.Node{&id, enc.value(e.val)}
+		case envProduct, envSum:
+			n.Kind = yaml.SequenceNode
+			if e.kind == envProduct {
+				n.Tag = "!product"
+			} else {
+				n.Tag = "!sum"
+			}
+			for _, e2 := range e.operands {
+				n.Content = append(n.Content, encode(e2))
 			}
 		}
+		return &n
 	}
-	return &n
+	return encode(e.root)
 }
 
 var yamlIntRe = regexp.MustCompile(`^-?[0-9]+$`)