Function getPiTerm

src/compute-engine/boxed-expression/utils.ts:281–321

(
  expr: Expression
)

  // opaque) — value-safe, and strictly better than silently corrupting.
  const binders = collectBinderNames(body);
  if (binders.size > 0) {
    for (const name of Object.keys(substitution)) {
      if (binders.has(name)) return undefined;
      for (const s of substitution[name].symbols)
        if (binders.has(s)) return undefined;
    }
  }

  return body.subs(substitution);
}

/** Every name bound by a binder anywhere within `expr` (its own bound names
 * plus those of every descendant), used to keep lambda inlining capture-safe. */
export function collectBinderNames(
  expr: Expression,
  acc: Set<string> = new Set()
): Set<string> {
  if (!isFunction(expr)) return acc;
  for (const n of boundVariableNames(expr)) acc.add(n);
  for (const op of expr.ops) collectBinderNames(op, acc);
  return acc;
}

/**
 * Inline applications of user-defined functions throughout `expr`.
 *
 * A lazy operator holds its expression operand and takes only `.canonical`,
 * which binds structure without substituting values. A call to a user-defined
 * function therefore arrived as an opaque node that the algorithm could not
 * see into: `Simplify(g(a))` returned `g(a)`, `Integrate(g(t), t)` stayed
 * inert, and — worst — `Solve(g(x) = 0, x)` returned `[]`, which by contract
 * means "proven no solutions".
 *
 * `budget` bounds the TOTAL number of beta-reductions so a self-recursive
 * definition (`fact(n) = … fact(n - 1) …`) cannot loop forever, while a finite
 * self-composition (`g(g(x))` for a non-recursive `g`) still fully expands — an
 * on-path name guard would wrongly stop the inner `g(x)`, leaving `Solve` an
 * opaque `g(x)` it reads as "no solutions". `budget` is a single object shared
 * by reference across every branch of the traversal, so it is one global cap on
 * the TOTAL number of beta-reductions in the whole tree — sibling calls
 * (`g(a) + g(b)`) draw down the same counter rather than each getting a fresh
 * budget. That shared cap is what bounds a self-recursive definition.
 */
// Generous enough that no realistic expression (a wide system of many function