3 ms·

For some reason I thought CoC just didn’t allow programs that lack a termination proof. Oops. Ok, so the assumption I left out was, “for a turing complete lang

by drdeca 6y ago

For some reason I thought CoC just didn’t allow programs that lack a termination proof. Oops. Ok, so the assumption I left out was, “for a turing complete language” or something like that (uh, in a sense in which “takes in a description of a Turing machine, an input to it, and a maximum number of steps, and runs the tm for up to that many steps” doesn’t count as turing complete)

tom_mellior 6y ago
> For some reason I thought CoC just didn’t allow programs that lack a termination proof. Oops. I'm not sure about CoC-the-abstract-calculus-on-paper, but I guess it cannot allow programs that lack a termination proof. Coq-the-concrete-implementation-of-CoC does allow some. Or not, depending how you look at it: What it will really do is infer a termination proof behind the scenes for certain simple cases, like iterating over a list and the recursive call always being on the tail of the current list. So everything has a termination proof in Coq, it's just that in simple cases you get it for free.