[Solved]: Decidability of dependent typing on primitive recursive languages

Problem Detail: 

With a dependent type system in a normal functional language type checking may never halt. This is partially because dependent typing removes the isolation between types, and code. My question is this: would an implementation of dependent typing for a primitive recursive language(not Turing-complete) be guaranteed to halt? Thanks!

Asked By : Harpo Roeder

Answered By : Jake

Not only is the answer to this question yes but this is exactly the strategy that modern implementations like Coq and Agda take! To be precise the type checker has to preform evaluation when deciding definitional equality so it would, if given the right language, be possible to write an infinite loop and ask weather it was definitional equal to another expression. Because of the way we define definitional equality in most cases this demands evaluation. The calculus of constructions is actually strongly normalizing. Type checking of CoC is decidable and requires no termination checking. But to make this theory more useful we want to add inductive types and recursion over these inductive types (thus we get the calculus of inductive constructions which Coq is based on). You can view this as a means of adding terms to our language that add computational content not otherwise present. Note than many inductive types can already be represented in CoC without aide but CoC can't represent everything CoIC can. Coq and Agda both have termination checkers that except all primitive recursive functions and can both encode the Ackermann function as well. You can see more about this in a question I once asked here.

good refrences on Agda's termination checker: http://www2.tcs.ifi.lmu.de/~abel/foetus/ http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.TerminationChecker

there is also a lot of work on sized types to provide an alternative to termination checking as well as some work on abstract interpretation based solutions. Currently however checking for a generalization (see foetus) of primitive recursion is as far the state of the art in mainstream implementation (at least as far as I am aware).

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/53130

3.2K people like this

 Download Related Notes/Documents