# Simplify the definition of substitution in Lamdba calculus

Substitution in untyped Lambda calculus is complicated by variable capture.

Can this boring technical complication be entirely avoided by some restriction on the standard formation rules? Something that prevents the dangerous symbol duplication. If so, how? Otherwise why not?

Alternatively, can the complication be avoided by uniformly alpha-converting every Lambda abstraction of the final composite, to ensure that every binding/bound variable symbol only appears locally (and therefore never as a free variable in the argument of an application term). If so, it seems that the substitution rules could be simplified.

Yes, there are several techniques, such as de Bruijn indices and explicit substitutions. Actual implementations, at least those that actually have to work efficiently, use such techniques and never implement substitution by renaming variables.

• Thanks!! Do you happen to have an opinion or value judgment about the best of these schemes?
– JRC
Jan 27 at 16:39
• I see (Hindley and Seldin): "First, there is a notation for λ-calculus that avoids bound variables completely. It was invented by N. G. de Bruijn, see [Bru72], and in it each bound variable-occurrence is replaced by a number showing its ‘distance’ from its binding λ, in a certain sense. De Bruijn’s notation has been found useful when coding λ-terms for machine manipulation; examples are in [Alt93, Hue94, KR95]. But, as remarked in [Pol93, pp. 314–315], it does not lead to a particularly simple definition of substitution, and most human workers still find the classical notation easier to read."
– JRC
Jan 27 at 16:56
• Are we discussing what humans find easier to read, or what is mathematically easiest to define, or what implementors actually use? Jan 27 at 22:12
• I'm just realizing that the answer to these three questions don't converge :(.
– JRC
Jan 28 at 8:13
• Why would they? Jan 28 at 8:44