New answers tagged

2

Spurred by comments in Pierre Marie's answer, I'll add some clarification on the difference between type checking and type synthesis. Generally, type checking in a dependent type system is designed to be decidable up to normalization for fully annotated terms, that is, $\lambda x : T.t$ and $\Pi x : T. U$ for example (you need type annotations in other ...


7

There are actually two questions here. Is the Coq type system decidable? Long answer short, we hope so, as in it would be a bug if it were not. It is not a universal requirement for a type theory to have decidable type-checking, but it is considered a desirable property. When type-checking is not decidable, one has to cheat to implement the theory as a proof ...


2

It is decidable, as a consequence of the usual consistency proof, tho the exact time bound is not well understood AFAICT. You can encode really huge functions into Coq that can take long to normalize, for a nice example see Ralf Loader's famous entry in the Bignum Bakeoff contest: http://djm.cc/bignum-results.txt


Top 50 recent answers are included