The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le 03/03/2020 à 23:56, Dominique Larchey-Wendling a écrit :
> What comes first to my mind is my own experience 
> that it is generally not possible to define nested recursive
> functions such as eg MCarthy's F91
> 
> F91 x = if x > 100 then x - 10 else F91 (F91 (x+11))
> 
> w/o using dependent types because they allow you to express
> properties of the output that you can feed into the type-checker
> for termination.

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.

In a HOL setting (or plain FOL for McCarthy's F91), types are never
empty, so functions always exist and return values, whether terminating
or not. (Obviously, if they do not terminate, you will not be able to
prove anything interesting about their return value.)

In fact, your next paragraph is a good characterization of non-dependent
type systems:

> Of course if you work in a framework where termination of all
> functions is not required by the type-checker, then you won't
> have such a constraint.

> On the other hand, proving properties after defining the function
> does not work with nested calls because you need those properties
> while constructing termination certificates.

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).

Best regards,

Guillaume