# Capture Avoiding Substitution of multiple variables at once

In articles you often find the terminus "capture avoiding substitution" that saves the author(s) from the tedious process to re-define a recursive function -including alpha-conversion and the invention of fresh names- in the discussion of dynamic semantics. The terminus is well understood by the readers and somewhat standard.

In order to provide an easy-to-read semantics, I recently defined a group of multiple recursive functions as a map from identifiers to (lambda-) terms. Application of one of these recursive functions then requires to substitute all free occurrences of its "siblings" in its body. It seems quite natural to introduce a generalization of substitution with partial functions instead of the usual univariate meta-function.

As an example consider the following group:

let rec fac n = if n <= 1 then 1 else n * (fac (n-1))
and foo n = fac n

in let fac = 5 in foo fac


This gives a two-element partial function, where each right-hand side is mapped to the recursive group with its body:

$\sigma = \left\{(\mathtt{foo} \mapsto \lambda \mathtt{n}. \mathtt{let\ rec\ ... in\ fac\ n}), (\mathtt{fac} \mapsto \lambda \mathtt{n} . \mathtt{let\ rec ...})\right\}$

This substitution is then applied to the body of the let-rec. It should first rename the bound variable fac, since it occurs freely in the codomain of the partial function i.e.

... let fac0 = 5 in foo fac0


Then, the substitution should replace any mapped variable at once:

... let fac0 = 5 in ((let rec fac = ... and foo = ... in fac) fac0)


When I generalize this, I cannot assume that the right-hand terms are recursive definitions. Any term might occur on the codomain. In particular, they could contain free variables that are bound by the substitution itself. Therefore, the order of replacements matters: I need to ensure that a replacement is not immediately subject to substitution again. This can, of course be defined, but I'd rather just use a sentence similar to the one mentioned above.

Is there a standard definition of capture avoiding substitution of multiple variables?