well-roundedness and termination_by

Stream: new members

[rzeta0]

I'm working through Chapter 6 of MoP.

There is discussion of "well foundedness" and termination_by required to be appended to the definition of recursive functions.

I have reached the exercises at the end of the chapter but have found the explanation hasn't been enough for me to understand.

I have a vague idea that:

• simply writing a definition for a recursive function does not mean it will "behave well"
• I think there is a difference between "will terminate" and "the definition is evaluated only using previously evaluated points"
• a termination measure is one way to determine that a function will terminate
• I'm not sure if that is the same thing as "well foundedness"
• I can't see how to derive a measure from a given function definition

I'd welcome advice, help or pointers elsewhere for further (beginner-level) reading,