termination checking, need escape analysis

[jsiek]

to make sure the recursive function doesn't get called indirectly on a non-decreasing argument.

[jsiek]

Simple solution: only allow recursive function names to appear as the operator in a function call, and nowhere else.

[Temperz87]

Can you give an example of this in Deduce?