So, how are we going to make any sense of this. Well, here comes all the theory of the semantics of functional programming languages. And the techniques most frequently used to show that certain implicitly definitions, circular definitions, do indeed define something are essentially based on the idea of turning the implicit specification which is normally something of the shape: F of x is equal to G of x, into a normalised equation which is something of this form. And at this point we have two alternatives: we have the denotational approach based on fixed-point theorems and the operational approach based on the theory of term rewriting systems. These are the two main set ways of giving semantics to functional languages. Let me just point out that the process of turning equations of the former form, that is this form, into normalised equations is essentially the problem of turning specifications into executable specifications. Of course the dream of any programming language would be just to be able to write any odd specification and by just applying some transformation turn it into an executable specification.

---