2
$\begingroup$

While going through Church's text on Lambda calculus , I cam across the first set of conversion rules .

Before writing out my query I would like to put the notation that church has used for substitution which is as follow :

$\ S$ $^x_yM $ means the act of substituting $y$ in place of $x$ all through out $M$ .

(I think there should be a mention of free variables but do not know why has that been left out)

The following are the rules of conversion that he has introduced :

I. To replace any part $ M $ of a formula by $\ S$ $^x_yM $ , provided that $x$ is not a free variable of $ M $ and $y$ does not occur in N.

II. To replace any part $ ( (\lambda x M)N)$ of a formula by $\ S$ $^x_yM $ provided that the bound variables of $ M $ are distinct both from x and from the free variables of $ N $.

III. To replace any part $\ S$ $^x_yM $ of a formula by $ ( (\lambda x M)y)$ provided that $ ( (\lambda x M)N)$ is well-formed and the bound variables of $N$ are distinct both from $x$ and from the free variables of $N$ .

Now next church writes that Rule 1 may be used to transform $ab (\lambda a a)(\lambda a a) $ into $ab (\lambda b b)(\lambda a a) $

and rule III can be used to transform $ \lambda a a $ into $ \lambda a .(\lambda a a) a$ .

I tried figuring out the above usage of rule 3 but could not be sure .

So , if in $ \lambda a a $ if we think "a has been substituted in place of a" ,i.e., $\ S$ $^x_yM $ where $M$ is $ \lambda a a $ and $x$ and $y$ are both $a$ , then I can see that application of rule 3 leads to $ \lambda a .(\lambda a a) a$ .

Is this understanding of mine correct ?

$\endgroup$

Your Answer

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

Browse other questions tagged or ask your own question.