The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

> That is kind of a circular argument: Dependent types require your
> functions to be terminating, and termination requires dependent types to
> be proved, thus dependent types are required.

Well yes that is true. But the motivation for having termination 
of all functions goes beyond having dependent types, eg consistency.

> Nested calls feel like a red herring to me. Indeed, you can always turn
> a function with nested calls into a function without nested calls, e.g.,
> using a trampoline. If your function uses dependent types, then your
> trampoline does too, and we are back to the circular argument. For F91,
> the trampoline has a trivial type (a list of single-valued elements,
> i.e., a natural number).

I'd be happy to have more details here. But I doubt you can do this
w/o modifying the computational content, ie the underlying algo. 
I should have used algo. instead of function in what I said. But 
I really meant algorithms.

Best,

Dominique