316 Here is a procedure applied to an argument. 〈x: int→ a:= x. b:= x〉 (a+1)
§
Suppose, by mistake, we replace both occurrences of x in the body with the argument. What do we get? What should we get? (This mistake is known as “call-by-name”.)
〈x: int→ a:= x. b:= x〉 (a+1) as directed, replace both occurrences of x
= a:= a+1. b:= a+1
= aʹ=a+1 ∧ bʹ=a+2
On page 39, Exercise 110(k) says that it is a mistake to replace the x after the composition. Here’s what we should get.
〈x: int→ a:= x. b:= x〉 (a+1) expand the two assignments
= 〈x: int→ aʹ=x ∧ bʹ=b. aʹ=a ∧ bʹ=x〉 (a+1) definition of dependent composition
= 〈x: int→ ∃aʹʹ, bʹʹ· aʹʹ=x ∧ bʹʹ=b ∧ aʹ=aʹʹ ∧ bʹ=x〉 (a+1)
= 〈x: int→ aʹ=bʹ=x〉 (a+1)
= aʹ=bʹ=a+1 OR
〈x: int→ a:= x. b:= x〉 (a+1)
= 〈x: int→ a:= x. aʹ=a ∧ bʹ=x〉 (a+1)
= 〈x: int→ aʹ=x ∧ bʹ=x〉 (a+1)
= 〈x: int→ aʹ=bʹ=x〉 (a+1)
= aʹ=bʹ=a+1
apply
expand the last assignment substitution law
apply