 A PCF program is a closed term of ground type. We specify how programs are to be executed by defining an evaluation relation \(e \opDownarrow v\) between closed terms \(e\) and values \(v\), where the values are the constants and abstractions of the form \({\lambda x:\sigma{\, . \,}e}\). In particular, values of ground type bool are \(\texttt{tt},\texttt{ff}\), and values of the ground type num are \({0}\) and all terms of the form   \[\mathtt{n} = \underbrace{\texttt{succ}(\ldots \texttt{succ}}_{n}({0}) \ldots ) .\]   Evaluation is defined by cases according to the structure of terms, by means of inference rules for judgements of the form \(e \opDownarrow v\). These rules state how the result of the evaluation of a term depends on the result of the evaluation of other terms, the only axioms having the form \(v \opDownarrow v\) for every value \(v\). For example there is a rule  \[\frac{e \opDownarrow v}{{\texttt{succ }e} \opDownarrow  {\texttt{succ }v}}\]   that states that, if the result of the evaluation of \(e\) is \(v\), then the result of the evaluation of \({\texttt{succ }e}\) is \({\texttt{succ } v}\). Similarly we can describe the evaluation of the other constants. The evaluation of a term of the form \(e_1\ e_2\) proceeds as follows: first \(e_1\) is evaluated; if the evaluation terminates with value \(v'\), then the evaluation of \(e_1\ e_2\) proceeds with the evaluation of \(v'\ e_2\); if this terminates with value \(v\), this is the value of \(e_1\ e_2\), formally   \[\frac{e_1 \opDownarrow v' \qquad v'\ e_2 \opDownarrow v}{e_1\ e_2 \opDownarrow v}\]   For a value of the form \({\lambda x:\sigma{\, . \,}e_1}\), its application to a term \(e_2\) has the value (if any) obtained by evaluating the term \(e_1[e_2/x]\) resulting by substituting \(e_2\) to all free occurrences of \(x\) in \(e_1\):  \[\frac{e_1[e_2/x] \opDownarrow v}{({\lambda x:\sigma{\, . \,}e_1}) e_2 \opDownarrow v}.\]   These implement a call-by-name evaluation strategy: in an application, the term in function position must be evaluated completely before the term in argument position, which is then passed as actual parameter. The fixed point combinator is essential to the encoding of recursive definitions. Its evaluation is described by the rule   \[\frac{e({\mathtt{Y}(e)}) \opDownarrow v}{{\mathtt{Y}(e)} \opDownarrow v}\]   which is the only rule whose premiss involves the evaluation of a larger term than the one to be evaluated: this is why the definition of the evaluation relation cannot be reduced to structural induction.