2
$\begingroup$

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.

Improve this question
$\endgroup$
3
$\begingroup$

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.

Improve this answer
$\endgroup$
7
  • $\begingroup$ Thanks!! Do you happen to have an opinion or value judgment about the best of these schemes? $\endgroup$ – JRC Jan 27 at 16:39
  • $\begingroup$ 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." $\endgroup$ – JRC Jan 27 at 16:56
  • $\begingroup$ Are we discussing what humans find easier to read, or what is mathematically easiest to define, or what implementors actually use? $\endgroup$ – Andrej Bauer Jan 27 at 22:12
  • $\begingroup$ I'm just realizing that the answer to these three questions don't converge :(. $\endgroup$ – JRC Jan 28 at 8:13
  • $\begingroup$ Why would they? $\endgroup$ – Andrej Bauer Jan 28 at 8:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.