370
(a) §
Let all variables be integer. Add recursive time. Using recursive construction, find a fixed-point of
skip = if i≥0 then i:= i–1. skip. i:= i+1 else ok fi Adding recursive time,
(b) §
skip = skip0 = skipn+1 = skip∞ =
if i≥0 then i:= i–1. t:= t+1. skip. i:= i+1 else ok fi
tʹ ≥ t
if i≥n then tʹ ≥ t+n+1 else if 0≤i
else tʹ=∞ fi fi
= if a≥b then t:= t+a–b. c:= Π[b+1;..a+1]/Π[1;..a–b+1] else tʹ=∞ fi
= chs∞
So chs∞ is a fixed-point. Note that for 1≤b≤a , cʹ is the number of ways of choosing b things from a things.