In the operational approach what we do is turn the symbol equality into an arrow. We view this asymmetrically. And so we give rise to what is called a substitution model of evaluation of functional programming languages whereby essentially we view this expression as a way of replacing all syntactic occurrences of the symbol x with the expanded form H of x. And we keep expanding, keep expanding, keep expanding until in the end we cannot expand any further. In general only this second approach allows for an implementation and this is essentially the way in which all functional programming languages are implemented. But why do we ever bother then to discuss the first approach, the denotational approach? Well, as it happens it is difficult to reason about term rewriting systems, but on the contrary denotationants, that is fixed points, are mathematical objects and hence they are easily amenable to rigorous reasoning. So the whole success of functional programming lies in this fact, that we have two ways of reading a functional programme. One is an operational way which admits evaluation and the other one is a denotational way in terms of fixed points which admits rigorous mathematical reasoning. So, let's have a look at fixed point theorems.

---