There is very general machinery, from Moschovakis 1989, called the Formal Language of Recursion, FLR. Using it a thorough exploration of recursive definitions and fixpoints is possible. The language that concerns us here, LPCR, embeds into FLR, even allowing nested clauses and parameters, something we ignored in our discussion of denotation. In FLR there is a method for converting recursive definitions into a normal form, which cannot be further reduced. That normal form has a very simple structure, consisting of a set of self-referential equations with no nesting present at all. Normal forms reveal essential evaluation structure most clearly. When working with a single structure, \(\langle\bD, \bR_1, \ldots, \bR_n\rangle\), all normal forms will be built from a common set of functionals. This makes it easy to compare normal forms. The idea is that if two formulas of LPCR, when embedded into FLR, have differing normal forms, the two formulas have different senses. Of course this must be taken with some reasonable flexibility. For instance, two sets of equations that differ only by renaming variables or switching order of equations do not differ in any fundamental way. With this understood, if two LPCR formulas, when embedded into FLR, have truly distinct normal forms, the two LPCR formulas are defined to have different senses. This meets all the informal conditions one wants a notion of sense to have. Moschovakis even proves the important theorem that equality of sense, as just defined, is decidable under natural conditions.