Mathematics for Computer Science

13.2. Reasoning AboutWhilePrograms 393

 ifŒŒTççDT, then

hifTthenCelseD; i!hC; i;

or ifŒŒTççDF, then

hifTthenCelseD; i!hD; i:

 ifŒŒTççDT, then

hwhileTdoCod; i!hCIwhileTdoCod; i

or ifŒŒTççDF, then

hwhileTdoCod; i!hDone; i:

Nowwhileprograms are probably going to be the simplest kind of programs you
will ever see, but being condescending about them would be a mistake. It turns that
every function on nonnegative integers that can be computed by any programon
any machine whatsoever can also be computed bywhileprograms (maybe more
slowly). We can’t take the time to explain how such a sweeping claim can be
justified, but you can find out by taking a course in computability theory such as
6.045 or 6.840.

13.2.3 Denotational Semantics

The net effect of starting awhileprogram in some environment is reflected in the
final environment when the program halts. So we can think of awhileprogram,C,
aas defining a function,ŒŒCççWEnv!Env, from initial environments to environ-
ments at halting. The functionŒŒCççis called themeaningofC.
ŒŒCççof awhileprogram,Cto be a partial function from Env to Env mapping an
initial environment to the final halting environment.
We’ll need one bit of notation first. For any functionf WS!S, letf.n/be the
composition off with itselfntimes wheren 2 N. Namely,

f.0/WWDIdS

f.nC1/WWDfıf.n/;

where “ı” denotes functional composition.
The recursive definition of the meaning of a program follows the definition of
thewhileprogram recursive data type.