How is the shifting operation reflected in substitution operation (Definition 6.2.4) and evaluation (Section 6.3) attach
Posted: Sun May 15, 2022 8:50 am
How is the shifting operation reflected in substitution
operation (Definition 6.2.4) and evaluation (Section 6.3) attached
below.
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).
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 67 times
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).