So first, you have to rename the bound variable first, for example to $\lambda z.xz$ and then you can safely substitute $x:=y$ to get $\lambda z.yz$. You'd get $\lambda y.yy$ which would change the meaning of the term. For example, you cannot substitute $x:=y$ into $\lambda y.xy$ because $y$ is bound under $\lambda$.
Alpha reduction in lambda calculus free#
Substitution applies only to free variables.It is better to rename bound variables ($\alpha$-conversion) to be distinct, for example to: Note that we now have $\lambda sz$ inside $\lambda sz$ which isn't very convenient (yet allowed). Where we replaced $m$ with $\lambda sz.sz$. In your case, the first reduction would be: (Capital letters likes $M$ and $N$ are used to denote terms.) The replacement $M$ is often called contractum.
It means, if you have a subterm that looks like $(\lambda x.M)N$ (called redex) you can replace it by $M$, which is $M$ with $N$ substituted for $x$. (λx.(y x) z) beta reduces to (y z) which is exactly the application of y to z, namely (y z).Lambda terms are simplified by the β-reduction rule: The motivation behind eta reduction is that the effect of an application of either of the eta expressions is the same. Any abstraction with the formįor example, λx.(y x) can be eta reduced to y. It is just mentioned here for completeness. This is a third reduction rule, which we will not need at all. Eta reduction (extensional equality of functions) If you can see this, your browser does not understand IFRAME. The reason for this is that the only time we need alpha conversion at all is to push through a beta reduction when there is capture of variable, but our implementation of beta reduction does the alpha rewrite automatically (leaving you to concentrate on more important matters)! In our implementation of reduction, we haven't made available the rewriting of a subformula by alpha conversion. So try to spot that sequence for it flags possible beta reductions. The expression, or sub-expression, which gets reduced is known as a redex (i.e. So, within the grammar we are using, an expression can be beta-reduced iff it starts with the two characters '(λ'.
HINT: Beta-reduction is always used on an application, that is, on an expression of the form ( ) and, in turn, the left expression has to be a lambda abstraction i.e. This rule can be used on sub-expressions of an expression. Beta reduction (the effect of function application):. Sometimes this is called alpha congruence.Īlpha conversion is not going to be a lot of interest to us- we need it only for ensuring that beta-reductions can take place, and more of that shortly. Normally we regard expressions with rewritten bound variables as same. λw.(w y) with the underlined pieces being re-written (question: can it be converted to λy.λy.(y y ) ? if not, why not?) The rule can also be applied to subexpressions- λy. In the simplest cases alpha conversion allows you to change, for example, λy.y into λx.x or λz.z. 9/13/19 Alpha conversion (Rewrite of bound variables):.
0 kommentar(er)
