Cheap and Secure Web Hosting Provider : See Now

[Solved]: Lambda Calculus inductive substitution definition

, , No Comments
Problem Detail: 

I'm reading Lambda-Calculus and Combinators: An Introduction, and there's the following definition of $\lambda$-substitution:

  • $FV(P)$ stands for the set containing all free-variables from $P$.

Def

I do understand that:

  • $(a), (b)$ are the base cases for this induction.
  • $(d)$ exists per definition, as one is not allowed to substitute bound variables.
  • $(g)$ prevents a bound variable from changing to a free one. It does this by first substituting a bound variable.

My question is: If one deletes $(d)$ and allows bound variables to be substituted, is $(g)$ strong enough to handle it without messing up everything?

I'm asking this because $(d)$ seems to prevent the following $\alpha$-equivalent substitutions.

$$ [y/x] ~~ \lambda x. x \equiv \lambda y.y $$

Asked By : melchizedek

Answered By : Anton Trunov

"If one deletes $(\mathrm{d})$ and allows bound variables to be substituted..."

The problem here is that substitution of a bound variable makes little sense, since one substitutes a variable (let's forget for a moment it should be free) with a term, which may very well be an abstraction or application, but not a variable.

Let me illustrate this by example. What if we are trying to substitute a bound variable with a term, which is not a variable? Like this: $$[(y\; y)\ / \ x]\ \lambda x. x.$$ What should we do?

  • Produce $\lambda (y\; y). (y\; y)$? It is not a well-formed term, so the answer is no.

  • Another choice would be to leave the binding instance intact and make $\lambda x. (y\; y)$ a result. Let's not take into account if it makes sense, at least it is syntactically correct. This variant causes us major troubles too: it will mess up scopes and render $\beta$-reduction useless. And our end goal is to define $\beta$-reduction via substitution.

$(\mathrm{g})$ prevents a bound variable from changing to a free one. It does this by first substituting a bound variable.

It does not use substitution, it uses renaming, which is a different notion.

"...is $(\mathrm{g})$ strong enough to handle it without messing up everything?"

$(\mathrm{g})$ does not tell us anything about substitution of bound variables, since it has the condition $x \in \mathrm{FV}(P)$

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/56755

3.2K people like this

 Download Related Notes/Documents

0 comments:

Post a Comment

Let us know your responses and feedback