How shall I understand the undesirable consequences of dynamic scoping? In Practical Foundation of Programming Languages by Harper


  8.4 Dynamic Scope
  
  Another approach, called dynamic scoping, or dynamic binding, is sometimes advocated
  as an alternative to static binding. The crucial difference is that with dynamic scoping the
  principle of identiﬁcation of abt’s up to renaming of bound variables is denied. Consequently, capture-avoiding substitution is not available. Instead, evaluation is deﬁned for
  open terms, with the bindings of free variables provided by an environment mapping variable names to (possibly open) values. The binding of a variable is determined as late as
  possible, at the point where the variable is evaluated, rather than where it is bound. If the
  environment does not provide a binding for a variable, evaluation is aborted with a run-time
  error.
  
  In the higher-order case, the equivalence of static and dynamic scope
  breaks down. For example, consider the expression

 e = (λ (x : num) λ (y : num) x + y)(42).

  
  With static scoping e evaluates to the closed value v = λ (y : num) 42 + y, which, if applied, would add 42 to its argument. It makes
  no difference how the bound variable x is chosen, the outcome will
  always be the same. With dynamic scoping, e evaluates to the open
  value v'  = λ (y : num) x + y in which the variable x occurs free.
  When this expression is evaluated, the variable x is bound to 42,
  but this is irrelevant because the binding is not needed to evaluate
  the λ-abstraction. The binding of x is not retrieved until such time
  as v' is applied to an argument, at which point the binding for x
  in force at that time is retrieved,and not the one in force at the
  point where e is evaluated. 
  
  Therein lies the difference. For example, consider the expression

e' = (λ (f : num → num) (λ (x : num) f (0))(7))(e)`.

  
  When evaluated using dynamic scope, the value of e' is 7, whereas
  its value is 42 under static scope. The discrepancy can be traced to
  the rebinding of x to 7 before the value of e, namely v', is
  applied to 0, altering the outcome.
  
  Dynamic scope violates the basic principle that variables are given
  meaning by capture-avoiding substitution as deﬁned in Chapter 1.
  Violating this principle has at least two undesirable consequences.
  
  One is that the names of bound variables matter, in contrast to static
  scope which obeys the identiﬁcation principle. For example, had the
  innermost λ-abstraction of e' bound the variable y, rather than
  x, then its value would have been 42, rather than 7. Thus, one
  component of a program may be sensitive to the names of bound
  variables chosen in another component, a clear violation of modular
  decomposition.
  
  Another problem is that dynamic scope is not, in general, type-safe.
  For example, consider the expression

e' = (λ (f : num → num) (λ (x : str) f ("zero"))(7))(e)

  
  Under dynamic scoping this expression gets stuck attempting to
  evaluate x + y with x bound to the string “zero”, and no further
  progress can be made.


What does it mean by "with dynamic scoping the
principle of identiﬁcation of abt’s up to renaming of bound variables is denied" and "consequently, capture-avoiding substitution is not available"?

Why under dynamic scoping, "had the innermost λ-abstraction of e' bound the variable y, rather than  x, then its value would have been 42, rather than 7"? How does  "static scope  obey the identiﬁcation principle" here?

How "Under dynamic scoping this expression gets stuck attempting to evaluate x + y with x bound to the string “zero”"?  Isn't it that x in e' is bound to 7?

Thanks.
I think you're right that that example is a bit confused. I believe the fix is the following, if I got my parantheses right.

e' = (λ (f : num → num) (λ (x : str) f ("zero"))(7))(e)


should instead be

e' = (λ (f : num → num) (λ (x : str) f) ("zero"))(e)(7)


If we evaluate e first we'll get:

(λ (x : num) λ (y : num) x + y)(42).

x = 42
(λ (y : num) x + y).


We've finished evaluating e, since we got to a lambda. But evaluating it in the above expression will cause the bad addition "zero" + 42, since, regardless of what we do with the environment, the x="zero" binding will be the closest. The immediate reduction of the above gives: