 Terms are built inductively according to rules that allow to infer judgements of the form \(B \vdash e : \sigma\), stating that term \(e\) is of type \(\sigma\) under the assumption that the variables occurring free in \(e\) are given unique types in a basis \(B\) of the form   \[{\{ x_1:\sigma_1,\ldots,x_k:\sigma_k \}}.\]   The rule for building PCF-terms are therefore inference rules for such judgements. In particular there are rules for typed constants, for example in any basis \(B\) there is a judgement \(B \vdash \texttt{zero?} : \texttt{num}\to \texttt{bool}\), and we have rules for typed \(\lambda\)-abstractions   \[\frac{B,x:\sigma \vdash e:\tau}{B \vdash {\lambda x:\sigma{\, . \,}e}:\sigma \to \tau}\]   and applications   \[\frac{B \vdash e_1 : \sigma \to \tau \qquad B \vdash e_2 : \sigma}{B \vdash e_1 e_2 : \tau}\]   and a rule for the fixed-point operator:   \[\frac{B \vdash e:\sigma \to \sigma} {B \vdash {\mathtt{Y}(e)}:\sigma}.\]   