How is the shifting operation reflected in substitution operation (Definition 6.2.4) and evaluation (Section 6.3) attach

[answerhappygod]

How is the shifting operation reflected in substitution
operation (Definition 6.2.4) and evaluation (Section 6.3) attached
below.

How Is The Shifting Operation Reflected In Substitution Operation Definition 6 2 4 And Evaluation Section 6 3 Attach 1 (52.98 KiB) Viewed 66 times

6.2.4 DEFINITION (SUBSTITUTION]: The substitution of a term s for variable num- ber j in a term t, written [j- s]t, is defined as follows: = [j - s]k = ss if k = j Ik otherwise 1. [j+1 -11(s)]tı ([j -s]tı [j - s]t2) = [ js](2.ti) [j - s](ti t2) =

Evaluation To define the evaluation relation on nameless terms, the only thing we need to change (because it is the only place where variable names are mentioned) is the beta-reduction rule, which must now use our new nameless substitution operation. The only slightly subtle point is that reducing a redex “uses up” the bound variable: when we reduce ((Ax.t12) v2) to [x - V2]t12, the bound variable x disappears in the process. Thus, we will need to renumber the variables of 6.3 Evaluation 81 the result of substitution to take into account the fact that x is no longer part of the context. For example: (1.10 2) (1.0) - 0 (1.0) 1 (not 1 (1.0) 2). Similarly, we need to shift the variables in v2 up by one before substituting into t12, since t12 is defined in a larger context than V2. Taking these points into account, the beta-reduction rule looks like this: (1.t12) v2 1-1 ([0 – 11 (v2)]t12) (E-APPABS) The other rules are identical to what we had before (Figure 5-3).